Testing processes usually aim at high coverage, but loops severely limit coverage ambitions since the number of iterations is generally not predictable. The most common solution is extreme: it limits its aims to achieving branch coverage, which only considers loop executions that iterate the body either once or not at all. This approach misses bugs that only arise after two or more iterations. To achieve more meaningful coverage, testing strategies may unroll loops, iterating them up to n times for some n greater than one, chosen pragmatically in consideration of the available computational power. While loop unrolling is a standard part of compiler optimization techniques, its use in testing is less common. Part of the reason is that the concept, while seemingly intuitive, lacks a generally accepted and precise specification. The present article provides a formal definition and a set of formal properties of unrolling. All the properties have mechanically been proved correct (through the Isabelle proof assistant). Using this definition, we have applied an unrolling strategy to an automated testing framework. The results indicate how many bugs the usual approach misses by limiting itself to branch coverage, analyzing the benefits (in number of detected bugs) and costs of successive unrolling levels. They provide important factual information on the merits of including unrolling in testing strategies and coverage measurement.