diff --git a/src/common/util/cilfacade.ml b/src/common/util/cilfacade.ml
index 9d2f8b2d3a..09aab6088b 100644
--- a/src/common/util/cilfacade.ml
+++ b/src/common/util/cilfacade.ml
@@ -66,8 +66,34 @@ let parse fileName =
     E.s (E.error "There were parsing errors in %s" fileName_str);
   file
 
+(** Version of {!defaultCilPrinterClass} which excludes line directives and builtin signatures (in comments).
+    Used for [dbg.justcil-printer]. *)
+class cleanCilPrinterClass =
+object
+  inherit defaultCilPrinterClass as super
+
+  method! pLineDirective ?(forcefile=false) l =
+    Pretty.nil
+
+  method! pGlobal () (g: global) =
+    match g with
+    | GVarDecl (vi, l) when Hashtbl.mem builtinFunctions vi.vname -> Pretty.nil
+    | _ -> super#pGlobal () g
+end
+
+let cleanCilPrinter = new cleanCilPrinterClass
+
+let cleanDumpFile (pp: cilPrinter) (out : out_channel) (outfile: string) file =
+  Pretty.printDepth := 99999;
+  Pretty.fastMode := true;
+  iterGlobals file (fun g -> dumpGlobal pp out g);
+  flush out
+
 let print (fileAST: file) =
-  dumpFile defaultCilPrinter stdout "stdout" fileAST
+  match GobConfig.get_string "dbg.justcil-printer" with
+  | "default" -> dumpFile defaultCilPrinter stdout "stdout" fileAST
+  | "clean" -> cleanDumpFile cleanCilPrinter stdout "stdout" fileAST
+  | _ -> assert false
 
 let rmTemps fileAST =
   RmUnused.removeUnused fileAST
diff --git a/src/config/options.schema.json b/src/config/options.schema.json
index 5d69990499..14f4530a45 100644
--- a/src/config/options.schema.json
+++ b/src/config/options.schema.json
@@ -1860,6 +1860,13 @@
           "type": "string",
           "default": ""
         },
+        "justcil-printer": {
+          "title": "dbg.justcil-printer",
+          "description": "Printer to use for justcil: default, or clean (excludes line directives and builtin declarations).",
+          "type": "string",
+          "enum": ["default", "clean"],
+          "default": "default"
+        },
         "timeout": {
           "title": "dbg.timeout",
           "description":
diff --git a/src/util/loopUnrolling.ml b/src/util/loopUnrolling.ml
index 519477557b..47f42ca830 100644
--- a/src/util/loopUnrolling.ml
+++ b/src/util/loopUnrolling.ml
@@ -299,7 +299,7 @@ class arrayVisitor = object
   inherit nopCilVisitor
 
   method! vvrbl info =
-    if not @@ (hasAttribute "goblint_array_domain" info.vattr || AutoTune0.is_large_array info.vtype) then
+    if Cil.isArrayType info.vtype && not @@ (hasAttribute "goblint_array_domain" info.vattr || AutoTune0.is_large_array info.vtype) then
       info.vattr <- addAttribute (Attr ("goblint_array_domain", [AStr "unroll"]) ) info.vattr;
     DoChildren
 end
@@ -390,27 +390,13 @@ end
   Also assigns fresh names to all labels and patches gotos for labels appearing in the current
   fragment to their new name
 *)
-class copyandPatchLabelsVisitor(loopEnd,currentIterationEnd) = object
+class copyandPatchLabelsVisitor(loopEnd, currentIterationEnd, gotos) = object
   inherit nopCilVisitor
 
-  val mutable depth = 0
   val mutable loopNestingDepth = 0
 
-  val gotos = StatementHashTable.create 20
-
   method! vstmt s =
-    let after x =
-      depth <- depth-1;
-      if depth = 0 then
-        (* the labels can only be patched once the entire part of the AST we want has been transformed, and *)
-        (* we know all lables appear in the hash table *)
-        let patchLabelsVisitor = new patchLabelsGotosVisitor(StatementHashTable.find_opt gotos) in
-        let x  = visitCilStmt patchLabelsVisitor x in
-        StatementHashTable.clear gotos;
-        x
-      else
-        x
-    in
+    let after x = x in
     let rename_labels sn =
       let new_labels = List.map (function Label(str,loc,b) -> Label (Cil.freshLabel str,loc,b) | x -> x) sn.labels in
       (* this makes new physical copy*)
@@ -421,18 +407,17 @@ class copyandPatchLabelsVisitor(loopEnd,currentIterationEnd) = object
         StatementHashTable.add gotos s new_s;
       new_s
     in
-    depth <- depth+1;
     match s.skind with
     | Continue loc ->
       if loopNestingDepth = 0 then
         (* turn top-level continues into gotos to end of current unrolling *)
-        ChangeDoChildrenPost(rename_labels {s with skind = Goto (!currentIterationEnd, loc)}, after)
+        ChangeDoChildrenPost(rename_labels {s with skind = Goto (ref currentIterationEnd, loc)}, after)
       else
         ChangeDoChildrenPost(rename_labels s, after)
     | Break loc ->
       if loopNestingDepth = 0 then
         (* turn top-level breaks into gotos to end of current unrolling *)
-        ChangeDoChildrenPost(rename_labels {s with skind = Goto (loopEnd,loc)}, after)
+        ChangeDoChildrenPost(rename_labels {s with skind = Goto (ref loopEnd,loc)}, after)
       else
         ChangeDoChildrenPost(rename_labels s, after)
     | Loop _ -> loopNestingDepth <- loopNestingDepth+1;
@@ -440,37 +425,41 @@ class copyandPatchLabelsVisitor(loopEnd,currentIterationEnd) = object
     | _ -> ChangeDoChildrenPost(rename_labels s, after)
 end
 
+let copy_and_patch_labels break_target current_continue_target stmts =
+  let gotos = StatementHashTable.create 20 in
+  let patcher = new copyandPatchLabelsVisitor (break_target, current_continue_target, gotos) in
+  let stmts' = List.map (visitCilStmt patcher) stmts in
+  (* the labels can only be patched once the entire part of the AST we want has been transformed, and *)
+  (* we know all lables appear in the hash table *)
+  let patchLabelsVisitor = new patchLabelsGotosVisitor(StatementHashTable.find_opt gotos) in
+  List.map (visitCilStmt patchLabelsVisitor) stmts'
+
 class loopUnrollingVisitor(func, totalLoops) = object
   (* Labels are simply handled by giving them a fresh name. Jumps coming from outside will still always go to the original label! *)
   inherit nopCilVisitor
 
   method! vstmt s =
-    match s.skind with
-    | Loop (b,loc, loc2, break , continue) ->
-      let duplicate_and_rem_labels s =
+    let duplicate_and_rem_labels s =
+      match s.skind with
+      | Loop (b,loc, loc2, break , continue) ->
         let factor = loop_unrolling_factor s func totalLoops in
         if(factor > 0) then (
           Logs.info "unrolling loop at %a with factor %d" CilType.Location.pretty loc factor;
           annotateArrays b;
-          match s.skind with
-          | Loop (b,loc, loc2, break , continue) ->
-            (* top-level breaks should immediately go to the end of the loop, and not just break out of the current iteration *)
-            let break_target = { (Cil.mkEmptyStmt ()) with labels = [Label (Cil.freshLabel "loop_end",loc, true)]} in
-            (* continues should go to the next unrolling *)
-            let continue_target i = { (Cil.mkEmptyStmt ()) with labels = [Label (Cil.freshLabel ("loop_continue_" ^ (string_of_int i)),loc, true)]} in
-            (* passed as a reference so we can reuse the patcher for all unrollings of the current loop *)
-            let current_continue_target = ref dummyStmt in
-            let patcher = new copyandPatchLabelsVisitor (ref break_target, ref current_continue_target) in
-            let one_copy () = visitCilStmt patcher (mkStmt (Block (mkBlock b.bstmts))) in
-            let copies = List.init (factor) (fun i ->
-                current_continue_target := continue_target i;
-                mkStmt (Block (mkBlock [one_copy (); !current_continue_target])))
-            in
-            mkStmt (Block (mkBlock (copies@[s]@[break_target])))
-          | _ -> failwith "invariant broken"
+          (* top-level breaks should immediately go to the end of the loop, and not just break out of the current iteration *)
+          let break_target = { (Cil.mkEmptyStmt ()) with labels = [Label (Cil.freshLabel "loop_end",loc, false)]} in
+          let copies = List.init factor (fun i ->
+              (* continues should go to the next unrolling *)
+              let current_continue_target = { (Cil.mkEmptyStmt ()) with labels = [Label (Cil.freshLabel ("loop_continue_" ^ (string_of_int i)),loc, false)]} in
+              let one_copy_stmts = copy_and_patch_labels break_target current_continue_target b.bstmts in
+              one_copy_stmts @ [current_continue_target]
+            )
+          in
+          mkStmt (Block (mkBlock (List.flatten copies @ [s; break_target])))
         ) else s (*no change*)
-      in ChangeDoChildrenPost(s, duplicate_and_rem_labels);
-    | _ -> DoChildren
+      | _ -> s
+    in
+    ChangeDoChildrenPost(s, duplicate_and_rem_labels)
 end
 
 let unroll_loops fd totalLoops =
diff --git a/tests/regression/55-loop-unrolling/01-simple-cases.t b/tests/regression/55-loop-unrolling/01-simple-cases.t
new file mode 100644
index 0000000000..4baf3c13d4
--- /dev/null
+++ b/tests/regression/55-loop-unrolling/01-simple-cases.t
@@ -0,0 +1,1034 @@
+  $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --enable justcil --set dbg.justcil-printer clean 01-simple-cases.c
+  [Info] unrolling loop at 01-simple-cases.c:27:5-30:5 with factor 5
+  [Info] unrolling loop at 01-simple-cases.c:42:5-45:19 with factor 5
+  [Info] unrolling loop at 01-simple-cases.c:57:5-60:5 with factor 5
+  [Info] unrolling loop at 01-simple-cases.c:74:5-80:5 with factor 5
+  [Info] unrolling loop at 01-simple-cases.c:95:5-105:5 with factor 5
+  [Info] unrolling loop at 01-simple-cases.c:119:5-123:5 with factor 5
+  [Info] unrolling loop at 01-simple-cases.c:143:2-146:2 with factor 5
+  [Info] unrolling loop at 01-simple-cases.c:160:9-163:9 with factor 5
+  [Info] unrolling loop at 01-simple-cases.c:157:2-165:2 with factor 5
+  [Info] unrolling loop at 01-simple-cases.c:174:2-178:2 with factor 5
+  [Info] unrolling loop at 01-simple-cases.c:187:2-194:2 with factor 5
+  extern void __goblint_check(int exp ) ;
+  extern void __goblint_assume(int exp ) ;
+  extern void __goblint_assert(int exp ) ;
+  extern void __goblint_assume_join() ;
+  extern void __goblint_globalize(void *ptr ) ;
+  extern void __goblint_split_begin(int exp ) ;
+  extern void __goblint_split_end(int exp ) ;
+  extern void __goblint_bounded(unsigned long long exp ) ;
+  int global  ;
+  void example1(void) ;
+  void example2(void) ;
+  void example3(void) ;
+  void example4(void) ;
+  void example5(void) ;
+  void example6(void) ;
+  void example7(void) ;
+  void example8(void) ;
+  void example9(void) ;
+  void example10(void) ;
+  int main(void) 
+  { 
+  
+  
+    {
+    example1();
+    example2();
+    example3();
+    example4();
+    example5();
+    example6();
+    example7();
+    example8();
+    example9();
+    example10();
+    return (0);
+  }
+  }
+  void example1(void) 
+  { 
+    int a[5] ;
+    int i ;
+  
+    {
+    i = 0;
+    {
+    if (! (i < 5)) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_0: /* CIL Label */ ;
+    if (! (i < 5)) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_1: /* CIL Label */ ;
+    if (! (i < 5)) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_2: /* CIL Label */ ;
+    if (! (i < 5)) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_3: /* CIL Label */ ;
+    if (! (i < 5)) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_4: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue: /* CIL Label */ ;
+      if (! (i < 5)) {
+        goto while_break;
+      }
+      a[i] = i;
+      i ++;
+    }
+    while_break: /* CIL Label */ ;
+    }
+    loop_end: /* CIL Label */ ;
+    }
+    __goblint_check(a[0] == 0);
+    __goblint_check(a[3] == 3);
+    return;
+  }
+  }
+  void example2(void) 
+  { 
+    int a[5] ;
+    int i ;
+  
+    {
+    i = 0;
+    {
+    a[i] = i;
+    i ++;
+    if (! (i <= 5)) {
+      goto loop_end;
+    }
+    loop_continue_0: /* CIL Label */ ;
+    a[i] = i;
+    i ++;
+    if (! (i <= 5)) {
+      goto loop_end;
+    }
+    loop_continue_1: /* CIL Label */ ;
+    a[i] = i;
+    i ++;
+    if (! (i <= 5)) {
+      goto loop_end;
+    }
+    loop_continue_2: /* CIL Label */ ;
+    a[i] = i;
+    i ++;
+    if (! (i <= 5)) {
+      goto loop_end;
+    }
+    loop_continue_3: /* CIL Label */ ;
+    a[i] = i;
+    i ++;
+    if (! (i <= 5)) {
+      goto loop_end;
+    }
+    loop_continue_4: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue: /* CIL Label */ ;
+      a[i] = i;
+      i ++;
+      if (! (i <= 5)) {
+        goto while_break;
+      }
+    }
+    while_break: /* CIL Label */ ;
+    }
+    loop_end: /* CIL Label */ ;
+    }
+    __goblint_check(a[0] == 0);
+    __goblint_check(a[3] == 3);
+    return;
+  }
+  }
+  void example3(void) 
+  { 
+    int a[10] ;
+    int i ;
+  
+    {
+    i = 0;
+    {
+    if (! (i < 5)) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_0: /* CIL Label */ ;
+    if (! (i < 5)) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_1: /* CIL Label */ ;
+    if (! (i < 5)) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_2: /* CIL Label */ ;
+    if (! (i < 5)) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_3: /* CIL Label */ ;
+    if (! (i < 5)) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_4: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue: /* CIL Label */ ;
+      if (! (i < 5)) {
+        goto while_break;
+      }
+      a[i] = i;
+      i ++;
+    }
+    while_break: /* CIL Label */ ;
+    }
+    loop_end: /* CIL Label */ ;
+    }
+    __goblint_check(a[0] == 0);
+    __goblint_check(a[3] == 0);
+    __goblint_check(a[7] == 0);
+    return;
+  }
+  }
+  void example4(void) 
+  { 
+    int a[10] ;
+    int i ;
+    int first_iteration ;
+  
+    {
+    i = 0;
+    first_iteration = 1;
+    {
+    if (! (i < 10)) {
+      goto loop_end;
+    }
+    if (first_iteration == 1) {
+      __goblint_check(i == 0);
+    } else
+    if (i > 5) {
+      __goblint_check(i == 6);
+    }
+    first_iteration = 0;
+    a[i] = 0;
+    i ++;
+    loop_continue_0: /* CIL Label */ ;
+    if (! (i < 10)) {
+      goto loop_end;
+    }
+    if (first_iteration == 1) {
+      __goblint_check(i == 0);
+    } else
+    if (i > 5) {
+      __goblint_check(i == 6);
+    }
+    first_iteration = 0;
+    a[i] = 0;
+    i ++;
+    loop_continue_1: /* CIL Label */ ;
+    if (! (i < 10)) {
+      goto loop_end;
+    }
+    if (first_iteration == 1) {
+      __goblint_check(i == 0);
+    } else
+    if (i > 5) {
+      __goblint_check(i == 6);
+    }
+    first_iteration = 0;
+    a[i] = 0;
+    i ++;
+    loop_continue_2: /* CIL Label */ ;
+    if (! (i < 10)) {
+      goto loop_end;
+    }
+    if (first_iteration == 1) {
+      __goblint_check(i == 0);
+    } else
+    if (i > 5) {
+      __goblint_check(i == 6);
+    }
+    first_iteration = 0;
+    a[i] = 0;
+    i ++;
+    loop_continue_3: /* CIL Label */ ;
+    if (! (i < 10)) {
+      goto loop_end;
+    }
+    if (first_iteration == 1) {
+      __goblint_check(i == 0);
+    } else
+    if (i > 5) {
+      __goblint_check(i == 6);
+    }
+    first_iteration = 0;
+    a[i] = 0;
+    i ++;
+    loop_continue_4: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue: /* CIL Label */ ;
+      if (! (i < 10)) {
+        goto while_break;
+      }
+      if (first_iteration == 1) {
+        __goblint_check(i == 0);
+      } else
+      if (i > 5) {
+        __goblint_check(i == 6);
+      }
+      first_iteration = 0;
+      a[i] = 0;
+      i ++;
+    }
+    while_break: /* CIL Label */ ;
+    }
+    loop_end: /* CIL Label */ ;
+    }
+    __goblint_check(a[0] == 0);
+    __goblint_check(first_iteration == 0);
+    return;
+  }
+  }
+  void example5(void) 
+  { 
+    int a[4] ;
+    int i ;
+    int top ;
+  
+    {
+    i = 0;
+    top = 0;
+    {
+    if (! (i < 4)) {
+      goto loop_end;
+    }
+    a[i] = 0;
+    top += i;
+    if (i == 2) {
+      __goblint_check(top == 3);
+    } else {
+      __goblint_check(top == 3);
+    }
+    i ++;
+    loop_continue_0: /* CIL Label */ ;
+    if (! (i < 4)) {
+      goto loop_end;
+    }
+    a[i] = 0;
+    top += i;
+    if (i == 2) {
+      __goblint_check(top == 3);
+    } else {
+      __goblint_check(top == 3);
+    }
+    i ++;
+    loop_continue_1: /* CIL Label */ ;
+    if (! (i < 4)) {
+      goto loop_end;
+    }
+    a[i] = 0;
+    top += i;
+    if (i == 2) {
+      __goblint_check(top == 3);
+    } else {
+      __goblint_check(top == 3);
+    }
+    i ++;
+    loop_continue_2: /* CIL Label */ ;
+    if (! (i < 4)) {
+      goto loop_end;
+    }
+    a[i] = 0;
+    top += i;
+    if (i == 2) {
+      __goblint_check(top == 3);
+    } else {
+      __goblint_check(top == 3);
+    }
+    i ++;
+    loop_continue_3: /* CIL Label */ ;
+    if (! (i < 4)) {
+      goto loop_end;
+    }
+    a[i] = 0;
+    top += i;
+    if (i == 2) {
+      __goblint_check(top == 3);
+    } else {
+      __goblint_check(top == 3);
+    }
+    i ++;
+    loop_continue_4: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue: /* CIL Label */ ;
+      if (! (i < 4)) {
+        goto while_break;
+      }
+      a[i] = 0;
+      top += i;
+      if (i == 2) {
+        __goblint_check(top == 3);
+      } else {
+        __goblint_check(top == 3);
+      }
+      i ++;
+    }
+    while_break: /* CIL Label */ ;
+    }
+    loop_end: /* CIL Label */ ;
+    }
+    __goblint_check(a[0] == 0);
+    __goblint_check(a[3] == 0);
+    __goblint_check(top == 6);
+    return;
+  }
+  }
+  void example6(void) 
+  { 
+    int a[5] ;
+    int i ;
+    int top ;
+  
+    {
+    i = 0;
+    top = 0;
+    {
+    if (! (i < 3)) {
+      goto loop_end;
+    }
+    a[i] = 0;
+    __goblint_check(a[0] == 0);
+    i ++;
+    loop_continue_0: /* CIL Label */ ;
+    if (! (i < 3)) {
+      goto loop_end;
+    }
+    a[i] = 0;
+    __goblint_check(a[0] == 0);
+    i ++;
+    loop_continue_1: /* CIL Label */ ;
+    if (! (i < 3)) {
+      goto loop_end;
+    }
+    a[i] = 0;
+    __goblint_check(a[0] == 0);
+    i ++;
+    loop_continue_2: /* CIL Label */ ;
+    if (! (i < 3)) {
+      goto loop_end;
+    }
+    a[i] = 0;
+    __goblint_check(a[0] == 0);
+    i ++;
+    loop_continue_3: /* CIL Label */ ;
+    if (! (i < 3)) {
+      goto loop_end;
+    }
+    a[i] = 0;
+    __goblint_check(a[0] == 0);
+    i ++;
+    loop_continue_4: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue: /* CIL Label */ ;
+      if (! (i < 3)) {
+        goto while_break;
+      }
+      a[i] = 0;
+      __goblint_check(a[0] == 0);
+      i ++;
+    }
+    while_break: /* CIL Label */ ;
+    }
+    loop_end: /* CIL Label */ ;
+    }
+    __goblint_check(a[0] == 0);
+    __goblint_check(a[3] == 0);
+    __goblint_check(top == 6);
+    return;
+  }
+  }
+  int update(int i ) 
+  { 
+  
+  
+    {
+    if (i > 5) {
+      return (0);
+    } else {
+      return (1);
+    }
+  }
+  }
+  void example7(void) 
+  { 
+    int a[10] ;
+    int i ;
+    int tmp ;
+  
+    {
+    i = 0;
+    {
+    tmp = update(i);
+    if (! tmp) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_0: /* CIL Label */ ;
+    tmp = update(i);
+    if (! tmp) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_1: /* CIL Label */ ;
+    tmp = update(i);
+    if (! tmp) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_2: /* CIL Label */ ;
+    tmp = update(i);
+    if (! tmp) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_3: /* CIL Label */ ;
+    tmp = update(i);
+    if (! tmp) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_4: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue: /* CIL Label */ ;
+      tmp = update(i);
+      if (! tmp) {
+        goto while_break;
+      }
+      a[i] = i;
+      i ++;
+    }
+    while_break: /* CIL Label */ ;
+    }
+    loop_end: /* CIL Label */ ;
+    }
+    __goblint_check(a[0] == 0);
+    __goblint_check(a[6] == 0);
+    return;
+  }
+  }
+  void example8(void) 
+  { 
+    int a[5] ;
+    int b[5] ;
+    int i ;
+    int j ;
+  
+    {
+    b[0] = 0;
+    b[1] = 0;
+    b[2] = 0;
+    b[3] = 0;
+    b[4] = 0;
+    i = 0;
+    {
+    if (! (i < 5)) {
+      goto loop_end___0;
+    }
+    a[i] = i;
+    j = 0;
+    {
+    if (! (j < 5)) {
+      goto loop_end___1;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_0___1: /* CIL Label */ ;
+    if (! (j < 5)) {
+      goto loop_end___1;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_1___0: /* CIL Label */ ;
+    if (! (j < 5)) {
+      goto loop_end___1;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_2___0: /* CIL Label */ ;
+    if (! (j < 5)) {
+      goto loop_end___1;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_3___0: /* CIL Label */ ;
+    if (! (j < 5)) {
+      goto loop_end___1;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_4___0: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue: /* CIL Label */ ;
+      if (! (j < 5)) {
+        goto while_break;
+      }
+      b[j] += a[i];
+      j ++;
+    }
+    while_break: /* CIL Label */ ;
+    }
+    loop_end___1: /* CIL Label */ ;
+    }
+    i ++;
+    loop_continue_0___0: /* CIL Label */ ;
+    if (! (i < 5)) {
+      goto loop_end___0;
+    }
+    a[i] = i;
+    j = 0;
+    {
+    if (! (j < 5)) {
+      goto loop_end___2;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_0___2: /* CIL Label */ ;
+    if (! (j < 5)) {
+      goto loop_end___2;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_1___2: /* CIL Label */ ;
+    if (! (j < 5)) {
+      goto loop_end___2;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_2___1: /* CIL Label */ ;
+    if (! (j < 5)) {
+      goto loop_end___2;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_3___1: /* CIL Label */ ;
+    if (! (j < 5)) {
+      goto loop_end___2;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_4___1: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue___0: /* CIL Label */ ;
+      if (! (j < 5)) {
+        goto while_break___0;
+      }
+      b[j] += a[i];
+      j ++;
+    }
+    while_break___0: /* CIL Label */ ;
+    }
+    loop_end___2: /* CIL Label */ ;
+    }
+    i ++;
+    loop_continue_1___1: /* CIL Label */ ;
+    if (! (i < 5)) {
+      goto loop_end___0;
+    }
+    a[i] = i;
+    j = 0;
+    {
+    if (! (j < 5)) {
+      goto loop_end___3;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_0___3: /* CIL Label */ ;
+    if (! (j < 5)) {
+      goto loop_end___3;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_1___3: /* CIL Label */ ;
+    if (! (j < 5)) {
+      goto loop_end___3;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_2___3: /* CIL Label */ ;
+    if (! (j < 5)) {
+      goto loop_end___3;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_3___2: /* CIL Label */ ;
+    if (! (j < 5)) {
+      goto loop_end___3;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_4___2: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue___1: /* CIL Label */ ;
+      if (! (j < 5)) {
+        goto while_break___1;
+      }
+      b[j] += a[i];
+      j ++;
+    }
+    while_break___1: /* CIL Label */ ;
+    }
+    loop_end___3: /* CIL Label */ ;
+    }
+    i ++;
+    loop_continue_2___2: /* CIL Label */ ;
+    if (! (i < 5)) {
+      goto loop_end___0;
+    }
+    a[i] = i;
+    j = 0;
+    {
+    if (! (j < 5)) {
+      goto loop_end___4;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_0___4: /* CIL Label */ ;
+    if (! (j < 5)) {
+      goto loop_end___4;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_1___4: /* CIL Label */ ;
+    if (! (j < 5)) {
+      goto loop_end___4;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_2___4: /* CIL Label */ ;
+    if (! (j < 5)) {
+      goto loop_end___4;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_3___4: /* CIL Label */ ;
+    if (! (j < 5)) {
+      goto loop_end___4;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_4___3: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue___2: /* CIL Label */ ;
+      if (! (j < 5)) {
+        goto while_break___2;
+      }
+      b[j] += a[i];
+      j ++;
+    }
+    while_break___2: /* CIL Label */ ;
+    }
+    loop_end___4: /* CIL Label */ ;
+    }
+    i ++;
+    loop_continue_3___3: /* CIL Label */ ;
+    if (! (i < 5)) {
+      goto loop_end___0;
+    }
+    a[i] = i;
+    j = 0;
+    {
+    if (! (j < 5)) {
+      goto loop_end___5;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_0___5: /* CIL Label */ ;
+    if (! (j < 5)) {
+      goto loop_end___5;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_1___5: /* CIL Label */ ;
+    if (! (j < 5)) {
+      goto loop_end___5;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_2___5: /* CIL Label */ ;
+    if (! (j < 5)) {
+      goto loop_end___5;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_3___5: /* CIL Label */ ;
+    if (! (j < 5)) {
+      goto loop_end___5;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_4___5: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue___3: /* CIL Label */ ;
+      if (! (j < 5)) {
+        goto while_break___3;
+      }
+      b[j] += a[i];
+      j ++;
+    }
+    while_break___3: /* CIL Label */ ;
+    }
+    loop_end___5: /* CIL Label */ ;
+    }
+    i ++;
+    loop_continue_4___4: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue___4: /* CIL Label */ ;
+      if (! (i < 5)) {
+        goto while_break___4;
+      }
+      a[i] = i;
+      j = 0;
+      {
+      if (! (j < 5)) {
+        goto loop_end;
+      }
+      b[j] += a[i];
+      j ++;
+      loop_continue_0: /* CIL Label */ ;
+      if (! (j < 5)) {
+        goto loop_end;
+      }
+      b[j] += a[i];
+      j ++;
+      loop_continue_1: /* CIL Label */ ;
+      if (! (j < 5)) {
+        goto loop_end;
+      }
+      b[j] += a[i];
+      j ++;
+      loop_continue_2: /* CIL Label */ ;
+      if (! (j < 5)) {
+        goto loop_end;
+      }
+      b[j] += a[i];
+      j ++;
+      loop_continue_3: /* CIL Label */ ;
+      if (! (j < 5)) {
+        goto loop_end;
+      }
+      b[j] += a[i];
+      j ++;
+      loop_continue_4: /* CIL Label */ ;
+      {
+      while (1) {
+        while_continue___5: /* CIL Label */ ;
+        if (! (j < 5)) {
+          goto while_break___5;
+        }
+        b[j] += a[i];
+        j ++;
+      }
+      while_break___5: /* CIL Label */ ;
+      }
+      loop_end: /* CIL Label */ ;
+      }
+      i ++;
+    }
+    while_break___4: /* CIL Label */ ;
+    }
+    loop_end___0: /* CIL Label */ ;
+    }
+    return;
+  }
+  }
+  void example9(void) 
+  { 
+    int a[5] ;
+    int i ;
+  
+    {
+    i = 0;
+    {
+    if (! 1) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    if (i == 5) {
+      goto loop_end;
+    }
+    loop_continue_0: /* CIL Label */ ;
+    if (! 1) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    if (i == 5) {
+      goto loop_end;
+    }
+    loop_continue_1: /* CIL Label */ ;
+    if (! 1) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    if (i == 5) {
+      goto loop_end;
+    }
+    loop_continue_2: /* CIL Label */ ;
+    if (! 1) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    if (i == 5) {
+      goto loop_end;
+    }
+    loop_continue_3: /* CIL Label */ ;
+    if (! 1) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    if (i == 5) {
+      goto loop_end;
+    }
+    loop_continue_4: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue: /* CIL Label */ ;
+      if (! 1) {
+        goto while_break;
+      }
+      a[i] = i;
+      i ++;
+      if (i == 5) {
+        goto while_break;
+      }
+    }
+    while_break: /* CIL Label */ ;
+    }
+    loop_end: /* CIL Label */ ;
+    }
+    return;
+  }
+  }
+  void example10(void) 
+  { 
+    int a[5] ;
+    int i ;
+  
+    {
+    i = 0;
+    {
+    if (! (i < 5)) {
+      goto loop_end;
+    }
+    if (i == 3) {
+      i ++;
+      goto loop_continue_0;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_0: /* CIL Label */ ;
+    if (! (i < 5)) {
+      goto loop_end;
+    }
+    if (i == 3) {
+      i ++;
+      goto loop_continue_1;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_1: /* CIL Label */ ;
+    if (! (i < 5)) {
+      goto loop_end;
+    }
+    if (i == 3) {
+      i ++;
+      goto loop_continue_2;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_2: /* CIL Label */ ;
+    if (! (i < 5)) {
+      goto loop_end;
+    }
+    if (i == 3) {
+      i ++;
+      goto loop_continue_3;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_3: /* CIL Label */ ;
+    if (! (i < 5)) {
+      goto loop_end;
+    }
+    if (i == 3) {
+      i ++;
+      goto loop_continue_4;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_4: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue: /* CIL Label */ ;
+      if (! (i < 5)) {
+        goto while_break;
+      }
+      if (i == 3) {
+        i ++;
+        goto while_continue;
+      }
+      a[i] = i;
+      i ++;
+    }
+    while_break: /* CIL Label */ ;
+    }
+    loop_end: /* CIL Label */ ;
+    }
+    return;
+  }
+  }
diff --git a/tests/regression/55-loop-unrolling/02-break.t b/tests/regression/55-loop-unrolling/02-break.t
new file mode 100644
index 0000000000..cd94f32d6e
--- /dev/null
+++ b/tests/regression/55-loop-unrolling/02-break.t
@@ -0,0 +1,156 @@
+  $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --enable justcil --set dbg.justcil-printer clean 02-break.c
+  [Info] unrolling loop at 02-break.c:6:5-15:2 with factor 5
+  extern void __goblint_check(int exp ) ;
+  extern void __goblint_assume(int exp ) ;
+  extern void __goblint_assert(int exp ) ;
+  extern void __goblint_assume_join() ;
+  extern void __goblint_globalize(void *ptr ) ;
+  extern void __goblint_split_begin(int exp ) ;
+  extern void __goblint_split_end(int exp ) ;
+  extern void __goblint_bounded(unsigned long long exp ) ;
+  int main(void) 
+  { 
+    int r ;
+    int i ;
+  
+    {
+    r = 5;
+    i = 0;
+    {
+    if (! (i < 2)) {
+      goto loop_end;
+    }
+    {
+    if (i == 0) {
+      goto case_0___4;
+    }
+    if (i == 1) {
+      goto case_1___4;
+    }
+    goto switch_break;
+    case_0: /* CIL Label */ 
+    goto loop_end;
+    case_1: /* CIL Label */ 
+    r = 8;
+    switch_break: /* CIL Label */ ;
+    }
+    r = 17;
+    goto loop_end;
+    i ++;
+    loop_continue_0: /* CIL Label */ ;
+    if (! (i < 2)) {
+      goto loop_end;
+    }
+    {
+    if (i == 0) {
+      goto case_0___4;
+    }
+    if (i == 1) {
+      goto case_1___4;
+    }
+    goto switch_break___0;
+    case_0___0: /* CIL Label */ 
+    goto loop_end;
+    case_1___0: /* CIL Label */ 
+    r = 8;
+    switch_break___0: /* CIL Label */ ;
+    }
+    r = 17;
+    goto loop_end;
+    i ++;
+    loop_continue_1: /* CIL Label */ ;
+    if (! (i < 2)) {
+      goto loop_end;
+    }
+    {
+    if (i == 0) {
+      goto case_0___4;
+    }
+    if (i == 1) {
+      goto case_1___4;
+    }
+    goto switch_break___1;
+    case_0___1: /* CIL Label */ 
+    goto loop_end;
+    case_1___1: /* CIL Label */ 
+    r = 8;
+    switch_break___1: /* CIL Label */ ;
+    }
+    r = 17;
+    goto loop_end;
+    i ++;
+    loop_continue_2: /* CIL Label */ ;
+    if (! (i < 2)) {
+      goto loop_end;
+    }
+    {
+    if (i == 0) {
+      goto case_0___4;
+    }
+    if (i == 1) {
+      goto case_1___4;
+    }
+    goto switch_break___2;
+    case_0___2: /* CIL Label */ 
+    goto loop_end;
+    case_1___2: /* CIL Label */ 
+    r = 8;
+    switch_break___2: /* CIL Label */ ;
+    }
+    r = 17;
+    goto loop_end;
+    i ++;
+    loop_continue_3: /* CIL Label */ ;
+    if (! (i < 2)) {
+      goto loop_end;
+    }
+    {
+    if (i == 0) {
+      goto case_0___4;
+    }
+    if (i == 1) {
+      goto case_1___4;
+    }
+    goto switch_break___3;
+    case_0___3: /* CIL Label */ 
+    goto loop_end;
+    case_1___3: /* CIL Label */ 
+    r = 8;
+    switch_break___3: /* CIL Label */ ;
+    }
+    r = 17;
+    goto loop_end;
+    i ++;
+    loop_continue_4: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue: /* CIL Label */ ;
+      if (! (i < 2)) {
+        goto while_break;
+      }
+      {
+      if (i == 0) {
+        goto case_0___4;
+      }
+      if (i == 1) {
+        goto case_1___4;
+      }
+      goto switch_break___4;
+      case_0___4: /* CIL Label */ 
+      goto switch_break___4;
+      case_1___4: /* CIL Label */ 
+      r = 8;
+      switch_break___4: /* CIL Label */ ;
+      }
+      r = 17;
+      goto while_break;
+      i ++;
+    }
+    while_break: /* CIL Label */ ;
+    }
+    loop_end: /* CIL Label */ ;
+    }
+    __goblint_check(r == 17);
+    return (0);
+  }
+  }
diff --git a/tests/regression/55-loop-unrolling/03-break-right-place.t b/tests/regression/55-loop-unrolling/03-break-right-place.t
new file mode 100644
index 0000000000..e4d15ae90e
--- /dev/null
+++ b/tests/regression/55-loop-unrolling/03-break-right-place.t
@@ -0,0 +1,84 @@
+  $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --enable justcil --set dbg.justcil-printer clean 03-break-right-place.c
+  [Info] unrolling loop at 03-break-right-place.c:8:5-15:5 with factor 5
+  extern void __goblint_check(int exp ) ;
+  extern void __goblint_assume(int exp ) ;
+  extern void __goblint_assert(int exp ) ;
+  extern void __goblint_assume_join() ;
+  extern void __goblint_globalize(void *ptr ) ;
+  extern void __goblint_split_begin(int exp ) ;
+  extern void __goblint_split_end(int exp ) ;
+  extern void __goblint_bounded(unsigned long long exp ) ;
+  int main(void) 
+  { 
+    int i ;
+    int j ;
+  
+    {
+    i = 0;
+    j = 0;
+    {
+    if (! (i < 17)) {
+      goto loop_end;
+    }
+    if (j == 0) {
+      j = 1;
+      goto loop_end;
+    }
+    i ++;
+    loop_continue_0: /* CIL Label */ ;
+    if (! (i < 17)) {
+      goto loop_end;
+    }
+    if (j == 0) {
+      j = 1;
+      goto loop_end;
+    }
+    i ++;
+    loop_continue_1: /* CIL Label */ ;
+    if (! (i < 17)) {
+      goto loop_end;
+    }
+    if (j == 0) {
+      j = 1;
+      goto loop_end;
+    }
+    i ++;
+    loop_continue_2: /* CIL Label */ ;
+    if (! (i < 17)) {
+      goto loop_end;
+    }
+    if (j == 0) {
+      j = 1;
+      goto loop_end;
+    }
+    i ++;
+    loop_continue_3: /* CIL Label */ ;
+    if (! (i < 17)) {
+      goto loop_end;
+    }
+    if (j == 0) {
+      j = 1;
+      goto loop_end;
+    }
+    i ++;
+    loop_continue_4: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue: /* CIL Label */ ;
+      if (! (i < 17)) {
+        goto while_break;
+      }
+      if (j == 0) {
+        j = 1;
+        goto while_break;
+      }
+      i ++;
+    }
+    while_break: /* CIL Label */ ;
+    }
+    loop_end: /* CIL Label */ ;
+    }
+    __goblint_check(i == 0);
+    return (0);
+  }
+  }
diff --git a/tests/regression/55-loop-unrolling/04-simple.t b/tests/regression/55-loop-unrolling/04-simple.t
new file mode 100644
index 0000000000..da38fd7b13
--- /dev/null
+++ b/tests/regression/55-loop-unrolling/04-simple.t
@@ -0,0 +1,66 @@
+  $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --set ana.base.arrays.domain unroll --set ana.base.arrays.unrolling-factor 5 --enable justcil --set dbg.justcil-printer clean 04-simple.c
+  [Info] unrolling loop at 04-simple.c:10:5-13:5 with factor 5
+  extern void __goblint_check(int exp ) ;
+  extern void __goblint_assume(int exp ) ;
+  extern void __goblint_assert(int exp ) ;
+  extern void __goblint_assume_join() ;
+  extern void __goblint_globalize(void *ptr ) ;
+  extern void __goblint_split_begin(int exp ) ;
+  extern void __goblint_split_end(int exp ) ;
+  extern void __goblint_bounded(unsigned long long exp ) ;
+  void main(void) 
+  { 
+    int a[5]  __attribute__((__goblint_array_domain__("unroll"))) ;
+    int i ;
+  
+    {
+    i = 0;
+    {
+    if (! (i < 5)) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_0: /* CIL Label */ ;
+    if (! (i < 5)) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_1: /* CIL Label */ ;
+    if (! (i < 5)) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_2: /* CIL Label */ ;
+    if (! (i < 5)) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_3: /* CIL Label */ ;
+    if (! (i < 5)) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_4: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue: /* CIL Label */ ;
+      if (! (i < 5)) {
+        goto while_break;
+      }
+      a[i] = i;
+      i ++;
+    }
+    while_break: /* CIL Label */ ;
+    }
+    loop_end: /* CIL Label */ ;
+    }
+    __goblint_check(a[0] == 0);
+    __goblint_check(a[3] == 3);
+    return;
+  }
+  }
diff --git a/tests/regression/55-loop-unrolling/05-continue.t b/tests/regression/55-loop-unrolling/05-continue.t
new file mode 100644
index 0000000000..16731ad4e6
--- /dev/null
+++ b/tests/regression/55-loop-unrolling/05-continue.t
@@ -0,0 +1,108 @@
+  $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --enable justcil --set dbg.justcil-printer clean 05-continue.c
+  [Info] unrolling loop at 05-continue.c:9:5-17:5 with factor 5
+  extern void __goblint_check(int exp ) ;
+  extern void __goblint_assume(int exp ) ;
+  extern void __goblint_assert(int exp ) ;
+  extern void __goblint_assume_join() ;
+  extern void __goblint_globalize(void *ptr ) ;
+  extern void __goblint_split_begin(int exp ) ;
+  extern void __goblint_split_end(int exp ) ;
+  extern void __goblint_bounded(unsigned long long exp ) ;
+  void main(void) 
+  { 
+    int j ;
+    int i ;
+  
+    {
+    j = 0;
+    i = 0;
+    {
+    if (! (i < 50)) {
+      goto loop_end;
+    }
+    if (i < 2) {
+      goto __Cont___0;
+    }
+    if (i > 4) {
+      goto loop_end;
+    }
+    j ++;
+    __Cont___0: /* CIL Label */ 
+    i ++;
+    loop_continue_0: /* CIL Label */ ;
+    if (! (i < 50)) {
+      goto loop_end;
+    }
+    if (i < 2) {
+      goto __Cont___1;
+    }
+    if (i > 4) {
+      goto loop_end;
+    }
+    j ++;
+    __Cont___1: /* CIL Label */ 
+    i ++;
+    loop_continue_1: /* CIL Label */ ;
+    if (! (i < 50)) {
+      goto loop_end;
+    }
+    if (i < 2) {
+      goto __Cont___2;
+    }
+    if (i > 4) {
+      goto loop_end;
+    }
+    j ++;
+    __Cont___2: /* CIL Label */ 
+    i ++;
+    loop_continue_2: /* CIL Label */ ;
+    if (! (i < 50)) {
+      goto loop_end;
+    }
+    if (i < 2) {
+      goto __Cont___3;
+    }
+    if (i > 4) {
+      goto loop_end;
+    }
+    j ++;
+    __Cont___3: /* CIL Label */ 
+    i ++;
+    loop_continue_3: /* CIL Label */ ;
+    if (! (i < 50)) {
+      goto loop_end;
+    }
+    if (i < 2) {
+      goto __Cont___4;
+    }
+    if (i > 4) {
+      goto loop_end;
+    }
+    j ++;
+    __Cont___4: /* CIL Label */ 
+    i ++;
+    loop_continue_4: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue: /* CIL Label */ ;
+      if (! (i < 50)) {
+        goto while_break;
+      }
+      if (i < 2) {
+        goto __Cont;
+      }
+      if (i > 4) {
+        goto while_break;
+      }
+      j ++;
+      __Cont: /* CIL Label */ 
+      i ++;
+    }
+    while_break: /* CIL Label */ ;
+    }
+    loop_end: /* CIL Label */ ;
+    }
+    __goblint_check(j == 3);
+    return;
+  }
+  }
diff --git a/tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t b/tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t
new file mode 100644
index 0000000000..52fd7d868b
--- /dev/null
+++ b/tests/regression/55-loop-unrolling/06-simple-cases-unrolled.t
@@ -0,0 +1,1034 @@
+  $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --set ana.base.arrays.domain unroll --set ana.base.arrays.unrolling-factor 5 --enable justcil --set dbg.justcil-printer clean 06-simple-cases-unrolled.c
+  [Info] unrolling loop at 06-simple-cases-unrolled.c:27:5-30:5 with factor 5
+  [Info] unrolling loop at 06-simple-cases-unrolled.c:42:5-45:19 with factor 5
+  [Info] unrolling loop at 06-simple-cases-unrolled.c:57:5-60:5 with factor 5
+  [Info] unrolling loop at 06-simple-cases-unrolled.c:74:5-80:5 with factor 5
+  [Info] unrolling loop at 06-simple-cases-unrolled.c:95:5-105:5 with factor 5
+  [Info] unrolling loop at 06-simple-cases-unrolled.c:119:5-123:5 with factor 5
+  [Info] unrolling loop at 06-simple-cases-unrolled.c:143:2-146:2 with factor 5
+  [Info] unrolling loop at 06-simple-cases-unrolled.c:160:9-163:9 with factor 5
+  [Info] unrolling loop at 06-simple-cases-unrolled.c:157:2-165:2 with factor 5
+  [Info] unrolling loop at 06-simple-cases-unrolled.c:174:2-178:2 with factor 5
+  [Info] unrolling loop at 06-simple-cases-unrolled.c:187:2-194:2 with factor 5
+  extern void __goblint_check(int exp ) ;
+  extern void __goblint_assume(int exp ) ;
+  extern void __goblint_assert(int exp ) ;
+  extern void __goblint_assume_join() ;
+  extern void __goblint_globalize(void *ptr ) ;
+  extern void __goblint_split_begin(int exp ) ;
+  extern void __goblint_split_end(int exp ) ;
+  extern void __goblint_bounded(unsigned long long exp ) ;
+  int global  ;
+  void example1(void) ;
+  void example2(void) ;
+  void example3(void) ;
+  void example4(void) ;
+  void example5(void) ;
+  void example6(void) ;
+  void example7(void) ;
+  void example8(void) ;
+  void example9(void) ;
+  void example10(void) ;
+  int main(void) 
+  { 
+  
+  
+    {
+    example1();
+    example2();
+    example3();
+    example4();
+    example5();
+    example6();
+    example7();
+    example8();
+    example9();
+    example10();
+    return (0);
+  }
+  }
+  void example1(void) 
+  { 
+    int a[5]  __attribute__((__goblint_array_domain__("unroll"))) ;
+    int i ;
+  
+    {
+    i = 0;
+    {
+    if (! (i < 5)) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_0: /* CIL Label */ ;
+    if (! (i < 5)) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_1: /* CIL Label */ ;
+    if (! (i < 5)) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_2: /* CIL Label */ ;
+    if (! (i < 5)) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_3: /* CIL Label */ ;
+    if (! (i < 5)) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_4: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue: /* CIL Label */ ;
+      if (! (i < 5)) {
+        goto while_break;
+      }
+      a[i] = i;
+      i ++;
+    }
+    while_break: /* CIL Label */ ;
+    }
+    loop_end: /* CIL Label */ ;
+    }
+    __goblint_check(a[0] == 0);
+    __goblint_check(a[3] == 3);
+    return;
+  }
+  }
+  void example2(void) 
+  { 
+    int a[5]  __attribute__((__goblint_array_domain__("unroll"))) ;
+    int i ;
+  
+    {
+    i = 0;
+    {
+    a[i] = i;
+    i ++;
+    if (! (i <= 5)) {
+      goto loop_end;
+    }
+    loop_continue_0: /* CIL Label */ ;
+    a[i] = i;
+    i ++;
+    if (! (i <= 5)) {
+      goto loop_end;
+    }
+    loop_continue_1: /* CIL Label */ ;
+    a[i] = i;
+    i ++;
+    if (! (i <= 5)) {
+      goto loop_end;
+    }
+    loop_continue_2: /* CIL Label */ ;
+    a[i] = i;
+    i ++;
+    if (! (i <= 5)) {
+      goto loop_end;
+    }
+    loop_continue_3: /* CIL Label */ ;
+    a[i] = i;
+    i ++;
+    if (! (i <= 5)) {
+      goto loop_end;
+    }
+    loop_continue_4: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue: /* CIL Label */ ;
+      a[i] = i;
+      i ++;
+      if (! (i <= 5)) {
+        goto while_break;
+      }
+    }
+    while_break: /* CIL Label */ ;
+    }
+    loop_end: /* CIL Label */ ;
+    }
+    __goblint_check(a[0] == 0);
+    __goblint_check(a[3] == 3);
+    return;
+  }
+  }
+  void example3(void) 
+  { 
+    int a[10]  __attribute__((__goblint_array_domain__("unroll"))) ;
+    int i ;
+  
+    {
+    i = 0;
+    {
+    if (! (i < 5)) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_0: /* CIL Label */ ;
+    if (! (i < 5)) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_1: /* CIL Label */ ;
+    if (! (i < 5)) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_2: /* CIL Label */ ;
+    if (! (i < 5)) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_3: /* CIL Label */ ;
+    if (! (i < 5)) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_4: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue: /* CIL Label */ ;
+      if (! (i < 5)) {
+        goto while_break;
+      }
+      a[i] = i;
+      i ++;
+    }
+    while_break: /* CIL Label */ ;
+    }
+    loop_end: /* CIL Label */ ;
+    }
+    __goblint_check(a[0] == 0);
+    __goblint_check(a[3] == 0);
+    __goblint_check(a[7] == 0);
+    return;
+  }
+  }
+  void example4(void) 
+  { 
+    int a[10]  __attribute__((__goblint_array_domain__("unroll"))) ;
+    int i ;
+    int first_iteration ;
+  
+    {
+    i = 0;
+    first_iteration = 1;
+    {
+    if (! (i < 10)) {
+      goto loop_end;
+    }
+    if (first_iteration == 1) {
+      __goblint_check(i == 0);
+    } else
+    if (i > 5) {
+      __goblint_check(i == 6);
+    }
+    first_iteration = 0;
+    a[i] = 0;
+    i ++;
+    loop_continue_0: /* CIL Label */ ;
+    if (! (i < 10)) {
+      goto loop_end;
+    }
+    if (first_iteration == 1) {
+      __goblint_check(i == 0);
+    } else
+    if (i > 5) {
+      __goblint_check(i == 6);
+    }
+    first_iteration = 0;
+    a[i] = 0;
+    i ++;
+    loop_continue_1: /* CIL Label */ ;
+    if (! (i < 10)) {
+      goto loop_end;
+    }
+    if (first_iteration == 1) {
+      __goblint_check(i == 0);
+    } else
+    if (i > 5) {
+      __goblint_check(i == 6);
+    }
+    first_iteration = 0;
+    a[i] = 0;
+    i ++;
+    loop_continue_2: /* CIL Label */ ;
+    if (! (i < 10)) {
+      goto loop_end;
+    }
+    if (first_iteration == 1) {
+      __goblint_check(i == 0);
+    } else
+    if (i > 5) {
+      __goblint_check(i == 6);
+    }
+    first_iteration = 0;
+    a[i] = 0;
+    i ++;
+    loop_continue_3: /* CIL Label */ ;
+    if (! (i < 10)) {
+      goto loop_end;
+    }
+    if (first_iteration == 1) {
+      __goblint_check(i == 0);
+    } else
+    if (i > 5) {
+      __goblint_check(i == 6);
+    }
+    first_iteration = 0;
+    a[i] = 0;
+    i ++;
+    loop_continue_4: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue: /* CIL Label */ ;
+      if (! (i < 10)) {
+        goto while_break;
+      }
+      if (first_iteration == 1) {
+        __goblint_check(i == 0);
+      } else
+      if (i > 5) {
+        __goblint_check(i == 6);
+      }
+      first_iteration = 0;
+      a[i] = 0;
+      i ++;
+    }
+    while_break: /* CIL Label */ ;
+    }
+    loop_end: /* CIL Label */ ;
+    }
+    __goblint_check(a[0] == 0);
+    __goblint_check(first_iteration == 0);
+    return;
+  }
+  }
+  void example5(void) 
+  { 
+    int a[4]  __attribute__((__goblint_array_domain__("unroll"))) ;
+    int i ;
+    int top ;
+  
+    {
+    i = 0;
+    top = 0;
+    {
+    if (! (i < 4)) {
+      goto loop_end;
+    }
+    a[i] = 0;
+    top += i;
+    if (i == 2) {
+      __goblint_check(top == 3);
+    } else {
+      __goblint_check(top == 3);
+    }
+    i ++;
+    loop_continue_0: /* CIL Label */ ;
+    if (! (i < 4)) {
+      goto loop_end;
+    }
+    a[i] = 0;
+    top += i;
+    if (i == 2) {
+      __goblint_check(top == 3);
+    } else {
+      __goblint_check(top == 3);
+    }
+    i ++;
+    loop_continue_1: /* CIL Label */ ;
+    if (! (i < 4)) {
+      goto loop_end;
+    }
+    a[i] = 0;
+    top += i;
+    if (i == 2) {
+      __goblint_check(top == 3);
+    } else {
+      __goblint_check(top == 3);
+    }
+    i ++;
+    loop_continue_2: /* CIL Label */ ;
+    if (! (i < 4)) {
+      goto loop_end;
+    }
+    a[i] = 0;
+    top += i;
+    if (i == 2) {
+      __goblint_check(top == 3);
+    } else {
+      __goblint_check(top == 3);
+    }
+    i ++;
+    loop_continue_3: /* CIL Label */ ;
+    if (! (i < 4)) {
+      goto loop_end;
+    }
+    a[i] = 0;
+    top += i;
+    if (i == 2) {
+      __goblint_check(top == 3);
+    } else {
+      __goblint_check(top == 3);
+    }
+    i ++;
+    loop_continue_4: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue: /* CIL Label */ ;
+      if (! (i < 4)) {
+        goto while_break;
+      }
+      a[i] = 0;
+      top += i;
+      if (i == 2) {
+        __goblint_check(top == 3);
+      } else {
+        __goblint_check(top == 3);
+      }
+      i ++;
+    }
+    while_break: /* CIL Label */ ;
+    }
+    loop_end: /* CIL Label */ ;
+    }
+    __goblint_check(a[0] == 0);
+    __goblint_check(a[3] == 0);
+    __goblint_check(top == 6);
+    return;
+  }
+  }
+  void example6(void) 
+  { 
+    int a[5]  __attribute__((__goblint_array_domain__("unroll"))) ;
+    int i ;
+    int top ;
+  
+    {
+    i = 0;
+    top = 0;
+    {
+    if (! (i < 3)) {
+      goto loop_end;
+    }
+    a[i] = 0;
+    __goblint_check(a[0] == 0);
+    i ++;
+    loop_continue_0: /* CIL Label */ ;
+    if (! (i < 3)) {
+      goto loop_end;
+    }
+    a[i] = 0;
+    __goblint_check(a[0] == 0);
+    i ++;
+    loop_continue_1: /* CIL Label */ ;
+    if (! (i < 3)) {
+      goto loop_end;
+    }
+    a[i] = 0;
+    __goblint_check(a[0] == 0);
+    i ++;
+    loop_continue_2: /* CIL Label */ ;
+    if (! (i < 3)) {
+      goto loop_end;
+    }
+    a[i] = 0;
+    __goblint_check(a[0] == 0);
+    i ++;
+    loop_continue_3: /* CIL Label */ ;
+    if (! (i < 3)) {
+      goto loop_end;
+    }
+    a[i] = 0;
+    __goblint_check(a[0] == 0);
+    i ++;
+    loop_continue_4: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue: /* CIL Label */ ;
+      if (! (i < 3)) {
+        goto while_break;
+      }
+      a[i] = 0;
+      __goblint_check(a[0] == 0);
+      i ++;
+    }
+    while_break: /* CIL Label */ ;
+    }
+    loop_end: /* CIL Label */ ;
+    }
+    __goblint_check(a[0] == 0);
+    __goblint_check(a[3] == 0);
+    __goblint_check(top == 6);
+    return;
+  }
+  }
+  int update(int i ) 
+  { 
+  
+  
+    {
+    if (i > 5) {
+      return (0);
+    } else {
+      return (1);
+    }
+  }
+  }
+  void example7(void) 
+  { 
+    int a[10]  __attribute__((__goblint_array_domain__("unroll"))) ;
+    int i ;
+    int tmp ;
+  
+    {
+    i = 0;
+    {
+    tmp = update(i);
+    if (! tmp) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_0: /* CIL Label */ ;
+    tmp = update(i);
+    if (! tmp) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_1: /* CIL Label */ ;
+    tmp = update(i);
+    if (! tmp) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_2: /* CIL Label */ ;
+    tmp = update(i);
+    if (! tmp) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_3: /* CIL Label */ ;
+    tmp = update(i);
+    if (! tmp) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_4: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue: /* CIL Label */ ;
+      tmp = update(i);
+      if (! tmp) {
+        goto while_break;
+      }
+      a[i] = i;
+      i ++;
+    }
+    while_break: /* CIL Label */ ;
+    }
+    loop_end: /* CIL Label */ ;
+    }
+    __goblint_check(a[0] == 0);
+    __goblint_check(a[6] == 0);
+    return;
+  }
+  }
+  void example8(void) 
+  { 
+    int a[5]  __attribute__((__goblint_array_domain__("unroll"))) ;
+    int b[5]  __attribute__((__goblint_array_domain__("unroll"))) ;
+    int i ;
+    int j ;
+  
+    {
+    b[0] = 0;
+    b[1] = 0;
+    b[2] = 0;
+    b[3] = 0;
+    b[4] = 0;
+    i = 0;
+    {
+    if (! (i < 5)) {
+      goto loop_end___0;
+    }
+    a[i] = i;
+    j = 0;
+    {
+    if (! (j < 5)) {
+      goto loop_end___1;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_0___1: /* CIL Label */ ;
+    if (! (j < 5)) {
+      goto loop_end___1;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_1___0: /* CIL Label */ ;
+    if (! (j < 5)) {
+      goto loop_end___1;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_2___0: /* CIL Label */ ;
+    if (! (j < 5)) {
+      goto loop_end___1;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_3___0: /* CIL Label */ ;
+    if (! (j < 5)) {
+      goto loop_end___1;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_4___0: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue: /* CIL Label */ ;
+      if (! (j < 5)) {
+        goto while_break;
+      }
+      b[j] += a[i];
+      j ++;
+    }
+    while_break: /* CIL Label */ ;
+    }
+    loop_end___1: /* CIL Label */ ;
+    }
+    i ++;
+    loop_continue_0___0: /* CIL Label */ ;
+    if (! (i < 5)) {
+      goto loop_end___0;
+    }
+    a[i] = i;
+    j = 0;
+    {
+    if (! (j < 5)) {
+      goto loop_end___2;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_0___2: /* CIL Label */ ;
+    if (! (j < 5)) {
+      goto loop_end___2;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_1___2: /* CIL Label */ ;
+    if (! (j < 5)) {
+      goto loop_end___2;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_2___1: /* CIL Label */ ;
+    if (! (j < 5)) {
+      goto loop_end___2;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_3___1: /* CIL Label */ ;
+    if (! (j < 5)) {
+      goto loop_end___2;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_4___1: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue___0: /* CIL Label */ ;
+      if (! (j < 5)) {
+        goto while_break___0;
+      }
+      b[j] += a[i];
+      j ++;
+    }
+    while_break___0: /* CIL Label */ ;
+    }
+    loop_end___2: /* CIL Label */ ;
+    }
+    i ++;
+    loop_continue_1___1: /* CIL Label */ ;
+    if (! (i < 5)) {
+      goto loop_end___0;
+    }
+    a[i] = i;
+    j = 0;
+    {
+    if (! (j < 5)) {
+      goto loop_end___3;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_0___3: /* CIL Label */ ;
+    if (! (j < 5)) {
+      goto loop_end___3;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_1___3: /* CIL Label */ ;
+    if (! (j < 5)) {
+      goto loop_end___3;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_2___3: /* CIL Label */ ;
+    if (! (j < 5)) {
+      goto loop_end___3;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_3___2: /* CIL Label */ ;
+    if (! (j < 5)) {
+      goto loop_end___3;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_4___2: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue___1: /* CIL Label */ ;
+      if (! (j < 5)) {
+        goto while_break___1;
+      }
+      b[j] += a[i];
+      j ++;
+    }
+    while_break___1: /* CIL Label */ ;
+    }
+    loop_end___3: /* CIL Label */ ;
+    }
+    i ++;
+    loop_continue_2___2: /* CIL Label */ ;
+    if (! (i < 5)) {
+      goto loop_end___0;
+    }
+    a[i] = i;
+    j = 0;
+    {
+    if (! (j < 5)) {
+      goto loop_end___4;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_0___4: /* CIL Label */ ;
+    if (! (j < 5)) {
+      goto loop_end___4;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_1___4: /* CIL Label */ ;
+    if (! (j < 5)) {
+      goto loop_end___4;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_2___4: /* CIL Label */ ;
+    if (! (j < 5)) {
+      goto loop_end___4;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_3___4: /* CIL Label */ ;
+    if (! (j < 5)) {
+      goto loop_end___4;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_4___3: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue___2: /* CIL Label */ ;
+      if (! (j < 5)) {
+        goto while_break___2;
+      }
+      b[j] += a[i];
+      j ++;
+    }
+    while_break___2: /* CIL Label */ ;
+    }
+    loop_end___4: /* CIL Label */ ;
+    }
+    i ++;
+    loop_continue_3___3: /* CIL Label */ ;
+    if (! (i < 5)) {
+      goto loop_end___0;
+    }
+    a[i] = i;
+    j = 0;
+    {
+    if (! (j < 5)) {
+      goto loop_end___5;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_0___5: /* CIL Label */ ;
+    if (! (j < 5)) {
+      goto loop_end___5;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_1___5: /* CIL Label */ ;
+    if (! (j < 5)) {
+      goto loop_end___5;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_2___5: /* CIL Label */ ;
+    if (! (j < 5)) {
+      goto loop_end___5;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_3___5: /* CIL Label */ ;
+    if (! (j < 5)) {
+      goto loop_end___5;
+    }
+    b[j] += a[i];
+    j ++;
+    loop_continue_4___5: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue___3: /* CIL Label */ ;
+      if (! (j < 5)) {
+        goto while_break___3;
+      }
+      b[j] += a[i];
+      j ++;
+    }
+    while_break___3: /* CIL Label */ ;
+    }
+    loop_end___5: /* CIL Label */ ;
+    }
+    i ++;
+    loop_continue_4___4: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue___4: /* CIL Label */ ;
+      if (! (i < 5)) {
+        goto while_break___4;
+      }
+      a[i] = i;
+      j = 0;
+      {
+      if (! (j < 5)) {
+        goto loop_end;
+      }
+      b[j] += a[i];
+      j ++;
+      loop_continue_0: /* CIL Label */ ;
+      if (! (j < 5)) {
+        goto loop_end;
+      }
+      b[j] += a[i];
+      j ++;
+      loop_continue_1: /* CIL Label */ ;
+      if (! (j < 5)) {
+        goto loop_end;
+      }
+      b[j] += a[i];
+      j ++;
+      loop_continue_2: /* CIL Label */ ;
+      if (! (j < 5)) {
+        goto loop_end;
+      }
+      b[j] += a[i];
+      j ++;
+      loop_continue_3: /* CIL Label */ ;
+      if (! (j < 5)) {
+        goto loop_end;
+      }
+      b[j] += a[i];
+      j ++;
+      loop_continue_4: /* CIL Label */ ;
+      {
+      while (1) {
+        while_continue___5: /* CIL Label */ ;
+        if (! (j < 5)) {
+          goto while_break___5;
+        }
+        b[j] += a[i];
+        j ++;
+      }
+      while_break___5: /* CIL Label */ ;
+      }
+      loop_end: /* CIL Label */ ;
+      }
+      i ++;
+    }
+    while_break___4: /* CIL Label */ ;
+    }
+    loop_end___0: /* CIL Label */ ;
+    }
+    return;
+  }
+  }
+  void example9(void) 
+  { 
+    int a[5]  __attribute__((__goblint_array_domain__("unroll"))) ;
+    int i ;
+  
+    {
+    i = 0;
+    {
+    if (! 1) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    if (i == 5) {
+      goto loop_end;
+    }
+    loop_continue_0: /* CIL Label */ ;
+    if (! 1) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    if (i == 5) {
+      goto loop_end;
+    }
+    loop_continue_1: /* CIL Label */ ;
+    if (! 1) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    if (i == 5) {
+      goto loop_end;
+    }
+    loop_continue_2: /* CIL Label */ ;
+    if (! 1) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    if (i == 5) {
+      goto loop_end;
+    }
+    loop_continue_3: /* CIL Label */ ;
+    if (! 1) {
+      goto loop_end;
+    }
+    a[i] = i;
+    i ++;
+    if (i == 5) {
+      goto loop_end;
+    }
+    loop_continue_4: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue: /* CIL Label */ ;
+      if (! 1) {
+        goto while_break;
+      }
+      a[i] = i;
+      i ++;
+      if (i == 5) {
+        goto while_break;
+      }
+    }
+    while_break: /* CIL Label */ ;
+    }
+    loop_end: /* CIL Label */ ;
+    }
+    return;
+  }
+  }
+  void example10(void) 
+  { 
+    int a[5]  __attribute__((__goblint_array_domain__("unroll"))) ;
+    int i ;
+  
+    {
+    i = 0;
+    {
+    if (! (i < 5)) {
+      goto loop_end;
+    }
+    if (i == 3) {
+      i ++;
+      goto loop_continue_0;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_0: /* CIL Label */ ;
+    if (! (i < 5)) {
+      goto loop_end;
+    }
+    if (i == 3) {
+      i ++;
+      goto loop_continue_1;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_1: /* CIL Label */ ;
+    if (! (i < 5)) {
+      goto loop_end;
+    }
+    if (i == 3) {
+      i ++;
+      goto loop_continue_2;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_2: /* CIL Label */ ;
+    if (! (i < 5)) {
+      goto loop_end;
+    }
+    if (i == 3) {
+      i ++;
+      goto loop_continue_3;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_3: /* CIL Label */ ;
+    if (! (i < 5)) {
+      goto loop_end;
+    }
+    if (i == 3) {
+      i ++;
+      goto loop_continue_4;
+    }
+    a[i] = i;
+    i ++;
+    loop_continue_4: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue: /* CIL Label */ ;
+      if (! (i < 5)) {
+        goto while_break;
+      }
+      if (i == 3) {
+        i ++;
+        goto while_continue;
+      }
+      a[i] = i;
+      i ++;
+    }
+    while_break: /* CIL Label */ ;
+    }
+    loop_end: /* CIL Label */ ;
+    }
+    return;
+  }
+  }
diff --git a/tests/regression/55-loop-unrolling/07-nested-unroll.t b/tests/regression/55-loop-unrolling/07-nested-unroll.t
new file mode 100644
index 0000000000..03455b7c8d
--- /dev/null
+++ b/tests/regression/55-loop-unrolling/07-nested-unroll.t
@@ -0,0 +1,643 @@
+  $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 5 --set ana.base.arrays.domain unroll --set ana.base.arrays.unrolling-factor 5 --enable justcil --set dbg.justcil-printer clean 07-nested-unroll.c
+  [Info] unrolling loop at 07-nested-unroll.c:7:9-9:9 with factor 5
+  [Info] unrolling loop at 07-nested-unroll.c:6:5-10:5 with factor 5
+  [Info] unrolling loop at 07-nested-unroll.c:13:9-15:9 with factor 5
+  [Info] unrolling loop at 07-nested-unroll.c:12:5-16:5 with factor 5
+  extern void __goblint_check(int exp ) ;
+  extern void __goblint_assume(int exp ) ;
+  extern void __goblint_assert(int exp ) ;
+  extern void __goblint_assume_join() ;
+  extern void __goblint_globalize(void *ptr ) ;
+  extern void __goblint_split_begin(int exp ) ;
+  extern void __goblint_split_end(int exp ) ;
+  extern void __goblint_bounded(unsigned long long exp ) ;
+  int main(void) 
+  { 
+    int arr[10][10]  __attribute__((__goblint_array_domain__("unroll"))) ;
+    int i ;
+    int j ;
+    int i___0 ;
+    int j___0 ;
+  
+    {
+    i = 0;
+    {
+    if (! (i < 10)) {
+      goto loop_end___0;
+    }
+    j = 0;
+    {
+    if (! (j < 10)) {
+      goto loop_end___1;
+    }
+    arr[i][j] = i + j;
+    j ++;
+    loop_continue_0___1: /* CIL Label */ ;
+    if (! (j < 10)) {
+      goto loop_end___1;
+    }
+    arr[i][j] = i + j;
+    j ++;
+    loop_continue_1___0: /* CIL Label */ ;
+    if (! (j < 10)) {
+      goto loop_end___1;
+    }
+    arr[i][j] = i + j;
+    j ++;
+    loop_continue_2___0: /* CIL Label */ ;
+    if (! (j < 10)) {
+      goto loop_end___1;
+    }
+    arr[i][j] = i + j;
+    j ++;
+    loop_continue_3___0: /* CIL Label */ ;
+    if (! (j < 10)) {
+      goto loop_end___1;
+    }
+    arr[i][j] = i + j;
+    j ++;
+    loop_continue_4___0: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue: /* CIL Label */ ;
+      if (! (j < 10)) {
+        goto while_break;
+      }
+      arr[i][j] = i + j;
+      j ++;
+    }
+    while_break: /* CIL Label */ ;
+    }
+    loop_end___1: /* CIL Label */ ;
+    }
+    i ++;
+    loop_continue_0___0: /* CIL Label */ ;
+    if (! (i < 10)) {
+      goto loop_end___0;
+    }
+    j = 0;
+    {
+    if (! (j < 10)) {
+      goto loop_end___2;
+    }
+    arr[i][j] = i + j;
+    j ++;
+    loop_continue_0___2: /* CIL Label */ ;
+    if (! (j < 10)) {
+      goto loop_end___2;
+    }
+    arr[i][j] = i + j;
+    j ++;
+    loop_continue_1___2: /* CIL Label */ ;
+    if (! (j < 10)) {
+      goto loop_end___2;
+    }
+    arr[i][j] = i + j;
+    j ++;
+    loop_continue_2___1: /* CIL Label */ ;
+    if (! (j < 10)) {
+      goto loop_end___2;
+    }
+    arr[i][j] = i + j;
+    j ++;
+    loop_continue_3___1: /* CIL Label */ ;
+    if (! (j < 10)) {
+      goto loop_end___2;
+    }
+    arr[i][j] = i + j;
+    j ++;
+    loop_continue_4___1: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue___0: /* CIL Label */ ;
+      if (! (j < 10)) {
+        goto while_break___0;
+      }
+      arr[i][j] = i + j;
+      j ++;
+    }
+    while_break___0: /* CIL Label */ ;
+    }
+    loop_end___2: /* CIL Label */ ;
+    }
+    i ++;
+    loop_continue_1___1: /* CIL Label */ ;
+    if (! (i < 10)) {
+      goto loop_end___0;
+    }
+    j = 0;
+    {
+    if (! (j < 10)) {
+      goto loop_end___3;
+    }
+    arr[i][j] = i + j;
+    j ++;
+    loop_continue_0___3: /* CIL Label */ ;
+    if (! (j < 10)) {
+      goto loop_end___3;
+    }
+    arr[i][j] = i + j;
+    j ++;
+    loop_continue_1___3: /* CIL Label */ ;
+    if (! (j < 10)) {
+      goto loop_end___3;
+    }
+    arr[i][j] = i + j;
+    j ++;
+    loop_continue_2___3: /* CIL Label */ ;
+    if (! (j < 10)) {
+      goto loop_end___3;
+    }
+    arr[i][j] = i + j;
+    j ++;
+    loop_continue_3___2: /* CIL Label */ ;
+    if (! (j < 10)) {
+      goto loop_end___3;
+    }
+    arr[i][j] = i + j;
+    j ++;
+    loop_continue_4___2: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue___1: /* CIL Label */ ;
+      if (! (j < 10)) {
+        goto while_break___1;
+      }
+      arr[i][j] = i + j;
+      j ++;
+    }
+    while_break___1: /* CIL Label */ ;
+    }
+    loop_end___3: /* CIL Label */ ;
+    }
+    i ++;
+    loop_continue_2___2: /* CIL Label */ ;
+    if (! (i < 10)) {
+      goto loop_end___0;
+    }
+    j = 0;
+    {
+    if (! (j < 10)) {
+      goto loop_end___4;
+    }
+    arr[i][j] = i + j;
+    j ++;
+    loop_continue_0___4: /* CIL Label */ ;
+    if (! (j < 10)) {
+      goto loop_end___4;
+    }
+    arr[i][j] = i + j;
+    j ++;
+    loop_continue_1___4: /* CIL Label */ ;
+    if (! (j < 10)) {
+      goto loop_end___4;
+    }
+    arr[i][j] = i + j;
+    j ++;
+    loop_continue_2___4: /* CIL Label */ ;
+    if (! (j < 10)) {
+      goto loop_end___4;
+    }
+    arr[i][j] = i + j;
+    j ++;
+    loop_continue_3___4: /* CIL Label */ ;
+    if (! (j < 10)) {
+      goto loop_end___4;
+    }
+    arr[i][j] = i + j;
+    j ++;
+    loop_continue_4___3: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue___2: /* CIL Label */ ;
+      if (! (j < 10)) {
+        goto while_break___2;
+      }
+      arr[i][j] = i + j;
+      j ++;
+    }
+    while_break___2: /* CIL Label */ ;
+    }
+    loop_end___4: /* CIL Label */ ;
+    }
+    i ++;
+    loop_continue_3___3: /* CIL Label */ ;
+    if (! (i < 10)) {
+      goto loop_end___0;
+    }
+    j = 0;
+    {
+    if (! (j < 10)) {
+      goto loop_end___5;
+    }
+    arr[i][j] = i + j;
+    j ++;
+    loop_continue_0___5: /* CIL Label */ ;
+    if (! (j < 10)) {
+      goto loop_end___5;
+    }
+    arr[i][j] = i + j;
+    j ++;
+    loop_continue_1___5: /* CIL Label */ ;
+    if (! (j < 10)) {
+      goto loop_end___5;
+    }
+    arr[i][j] = i + j;
+    j ++;
+    loop_continue_2___5: /* CIL Label */ ;
+    if (! (j < 10)) {
+      goto loop_end___5;
+    }
+    arr[i][j] = i + j;
+    j ++;
+    loop_continue_3___5: /* CIL Label */ ;
+    if (! (j < 10)) {
+      goto loop_end___5;
+    }
+    arr[i][j] = i + j;
+    j ++;
+    loop_continue_4___5: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue___3: /* CIL Label */ ;
+      if (! (j < 10)) {
+        goto while_break___3;
+      }
+      arr[i][j] = i + j;
+      j ++;
+    }
+    while_break___3: /* CIL Label */ ;
+    }
+    loop_end___5: /* CIL Label */ ;
+    }
+    i ++;
+    loop_continue_4___4: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue___4: /* CIL Label */ ;
+      if (! (i < 10)) {
+        goto while_break___4;
+      }
+      j = 0;
+      {
+      if (! (j < 10)) {
+        goto loop_end;
+      }
+      arr[i][j] = i + j;
+      j ++;
+      loop_continue_0: /* CIL Label */ ;
+      if (! (j < 10)) {
+        goto loop_end;
+      }
+      arr[i][j] = i + j;
+      j ++;
+      loop_continue_1: /* CIL Label */ ;
+      if (! (j < 10)) {
+        goto loop_end;
+      }
+      arr[i][j] = i + j;
+      j ++;
+      loop_continue_2: /* CIL Label */ ;
+      if (! (j < 10)) {
+        goto loop_end;
+      }
+      arr[i][j] = i + j;
+      j ++;
+      loop_continue_3: /* CIL Label */ ;
+      if (! (j < 10)) {
+        goto loop_end;
+      }
+      arr[i][j] = i + j;
+      j ++;
+      loop_continue_4: /* CIL Label */ ;
+      {
+      while (1) {
+        while_continue___5: /* CIL Label */ ;
+        if (! (j < 10)) {
+          goto while_break___5;
+        }
+        arr[i][j] = i + j;
+        j ++;
+      }
+      while_break___5: /* CIL Label */ ;
+      }
+      loop_end: /* CIL Label */ ;
+      }
+      i ++;
+    }
+    while_break___4: /* CIL Label */ ;
+    }
+    loop_end___0: /* CIL Label */ ;
+    }
+    i___0 = 0;
+    {
+    if (! (i___0 < 5)) {
+      goto loop_end___7;
+    }
+    j___0 = 0;
+    {
+    if (! (j___0 < 5)) {
+      goto loop_end___8;
+    }
+    __goblint_check(arr[i___0][j___0] == i___0 + j___0);
+    j___0 ++;
+    loop_continue_0___8: /* CIL Label */ ;
+    if (! (j___0 < 5)) {
+      goto loop_end___8;
+    }
+    __goblint_check(arr[i___0][j___0] == i___0 + j___0);
+    j___0 ++;
+    loop_continue_1___7: /* CIL Label */ ;
+    if (! (j___0 < 5)) {
+      goto loop_end___8;
+    }
+    __goblint_check(arr[i___0][j___0] == i___0 + j___0);
+    j___0 ++;
+    loop_continue_2___7: /* CIL Label */ ;
+    if (! (j___0 < 5)) {
+      goto loop_end___8;
+    }
+    __goblint_check(arr[i___0][j___0] == i___0 + j___0);
+    j___0 ++;
+    loop_continue_3___7: /* CIL Label */ ;
+    if (! (j___0 < 5)) {
+      goto loop_end___8;
+    }
+    __goblint_check(arr[i___0][j___0] == i___0 + j___0);
+    j___0 ++;
+    loop_continue_4___7: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue___6: /* CIL Label */ ;
+      if (! (j___0 < 5)) {
+        goto while_break___6;
+      }
+      __goblint_check(arr[i___0][j___0] == i___0 + j___0);
+      j___0 ++;
+    }
+    while_break___6: /* CIL Label */ ;
+    }
+    loop_end___8: /* CIL Label */ ;
+    }
+    i___0 ++;
+    loop_continue_0___7: /* CIL Label */ ;
+    if (! (i___0 < 5)) {
+      goto loop_end___7;
+    }
+    j___0 = 0;
+    {
+    if (! (j___0 < 5)) {
+      goto loop_end___9;
+    }
+    __goblint_check(arr[i___0][j___0] == i___0 + j___0);
+    j___0 ++;
+    loop_continue_0___9: /* CIL Label */ ;
+    if (! (j___0 < 5)) {
+      goto loop_end___9;
+    }
+    __goblint_check(arr[i___0][j___0] == i___0 + j___0);
+    j___0 ++;
+    loop_continue_1___9: /* CIL Label */ ;
+    if (! (j___0 < 5)) {
+      goto loop_end___9;
+    }
+    __goblint_check(arr[i___0][j___0] == i___0 + j___0);
+    j___0 ++;
+    loop_continue_2___8: /* CIL Label */ ;
+    if (! (j___0 < 5)) {
+      goto loop_end___9;
+    }
+    __goblint_check(arr[i___0][j___0] == i___0 + j___0);
+    j___0 ++;
+    loop_continue_3___8: /* CIL Label */ ;
+    if (! (j___0 < 5)) {
+      goto loop_end___9;
+    }
+    __goblint_check(arr[i___0][j___0] == i___0 + j___0);
+    j___0 ++;
+    loop_continue_4___8: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue___7: /* CIL Label */ ;
+      if (! (j___0 < 5)) {
+        goto while_break___7;
+      }
+      __goblint_check(arr[i___0][j___0] == i___0 + j___0);
+      j___0 ++;
+    }
+    while_break___7: /* CIL Label */ ;
+    }
+    loop_end___9: /* CIL Label */ ;
+    }
+    i___0 ++;
+    loop_continue_1___8: /* CIL Label */ ;
+    if (! (i___0 < 5)) {
+      goto loop_end___7;
+    }
+    j___0 = 0;
+    {
+    if (! (j___0 < 5)) {
+      goto loop_end___10;
+    }
+    __goblint_check(arr[i___0][j___0] == i___0 + j___0);
+    j___0 ++;
+    loop_continue_0___10: /* CIL Label */ ;
+    if (! (j___0 < 5)) {
+      goto loop_end___10;
+    }
+    __goblint_check(arr[i___0][j___0] == i___0 + j___0);
+    j___0 ++;
+    loop_continue_1___10: /* CIL Label */ ;
+    if (! (j___0 < 5)) {
+      goto loop_end___10;
+    }
+    __goblint_check(arr[i___0][j___0] == i___0 + j___0);
+    j___0 ++;
+    loop_continue_2___10: /* CIL Label */ ;
+    if (! (j___0 < 5)) {
+      goto loop_end___10;
+    }
+    __goblint_check(arr[i___0][j___0] == i___0 + j___0);
+    j___0 ++;
+    loop_continue_3___9: /* CIL Label */ ;
+    if (! (j___0 < 5)) {
+      goto loop_end___10;
+    }
+    __goblint_check(arr[i___0][j___0] == i___0 + j___0);
+    j___0 ++;
+    loop_continue_4___9: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue___8: /* CIL Label */ ;
+      if (! (j___0 < 5)) {
+        goto while_break___8;
+      }
+      __goblint_check(arr[i___0][j___0] == i___0 + j___0);
+      j___0 ++;
+    }
+    while_break___8: /* CIL Label */ ;
+    }
+    loop_end___10: /* CIL Label */ ;
+    }
+    i___0 ++;
+    loop_continue_2___9: /* CIL Label */ ;
+    if (! (i___0 < 5)) {
+      goto loop_end___7;
+    }
+    j___0 = 0;
+    {
+    if (! (j___0 < 5)) {
+      goto loop_end___11;
+    }
+    __goblint_check(arr[i___0][j___0] == i___0 + j___0);
+    j___0 ++;
+    loop_continue_0___11: /* CIL Label */ ;
+    if (! (j___0 < 5)) {
+      goto loop_end___11;
+    }
+    __goblint_check(arr[i___0][j___0] == i___0 + j___0);
+    j___0 ++;
+    loop_continue_1___11: /* CIL Label */ ;
+    if (! (j___0 < 5)) {
+      goto loop_end___11;
+    }
+    __goblint_check(arr[i___0][j___0] == i___0 + j___0);
+    j___0 ++;
+    loop_continue_2___11: /* CIL Label */ ;
+    if (! (j___0 < 5)) {
+      goto loop_end___11;
+    }
+    __goblint_check(arr[i___0][j___0] == i___0 + j___0);
+    j___0 ++;
+    loop_continue_3___11: /* CIL Label */ ;
+    if (! (j___0 < 5)) {
+      goto loop_end___11;
+    }
+    __goblint_check(arr[i___0][j___0] == i___0 + j___0);
+    j___0 ++;
+    loop_continue_4___10: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue___9: /* CIL Label */ ;
+      if (! (j___0 < 5)) {
+        goto while_break___9;
+      }
+      __goblint_check(arr[i___0][j___0] == i___0 + j___0);
+      j___0 ++;
+    }
+    while_break___9: /* CIL Label */ ;
+    }
+    loop_end___11: /* CIL Label */ ;
+    }
+    i___0 ++;
+    loop_continue_3___10: /* CIL Label */ ;
+    if (! (i___0 < 5)) {
+      goto loop_end___7;
+    }
+    j___0 = 0;
+    {
+    if (! (j___0 < 5)) {
+      goto loop_end___12;
+    }
+    __goblint_check(arr[i___0][j___0] == i___0 + j___0);
+    j___0 ++;
+    loop_continue_0___12: /* CIL Label */ ;
+    if (! (j___0 < 5)) {
+      goto loop_end___12;
+    }
+    __goblint_check(arr[i___0][j___0] == i___0 + j___0);
+    j___0 ++;
+    loop_continue_1___12: /* CIL Label */ ;
+    if (! (j___0 < 5)) {
+      goto loop_end___12;
+    }
+    __goblint_check(arr[i___0][j___0] == i___0 + j___0);
+    j___0 ++;
+    loop_continue_2___12: /* CIL Label */ ;
+    if (! (j___0 < 5)) {
+      goto loop_end___12;
+    }
+    __goblint_check(arr[i___0][j___0] == i___0 + j___0);
+    j___0 ++;
+    loop_continue_3___12: /* CIL Label */ ;
+    if (! (j___0 < 5)) {
+      goto loop_end___12;
+    }
+    __goblint_check(arr[i___0][j___0] == i___0 + j___0);
+    j___0 ++;
+    loop_continue_4___12: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue___10: /* CIL Label */ ;
+      if (! (j___0 < 5)) {
+        goto while_break___10;
+      }
+      __goblint_check(arr[i___0][j___0] == i___0 + j___0);
+      j___0 ++;
+    }
+    while_break___10: /* CIL Label */ ;
+    }
+    loop_end___12: /* CIL Label */ ;
+    }
+    i___0 ++;
+    loop_continue_4___11: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue___11: /* CIL Label */ ;
+      if (! (i___0 < 5)) {
+        goto while_break___11;
+      }
+      j___0 = 0;
+      {
+      if (! (j___0 < 5)) {
+        goto loop_end___6;
+      }
+      __goblint_check(arr[i___0][j___0] == i___0 + j___0);
+      j___0 ++;
+      loop_continue_0___6: /* CIL Label */ ;
+      if (! (j___0 < 5)) {
+        goto loop_end___6;
+      }
+      __goblint_check(arr[i___0][j___0] == i___0 + j___0);
+      j___0 ++;
+      loop_continue_1___6: /* CIL Label */ ;
+      if (! (j___0 < 5)) {
+        goto loop_end___6;
+      }
+      __goblint_check(arr[i___0][j___0] == i___0 + j___0);
+      j___0 ++;
+      loop_continue_2___6: /* CIL Label */ ;
+      if (! (j___0 < 5)) {
+        goto loop_end___6;
+      }
+      __goblint_check(arr[i___0][j___0] == i___0 + j___0);
+      j___0 ++;
+      loop_continue_3___6: /* CIL Label */ ;
+      if (! (j___0 < 5)) {
+        goto loop_end___6;
+      }
+      __goblint_check(arr[i___0][j___0] == i___0 + j___0);
+      j___0 ++;
+      loop_continue_4___6: /* CIL Label */ ;
+      {
+      while (1) {
+        while_continue___12: /* CIL Label */ ;
+        if (! (j___0 < 5)) {
+          goto while_break___12;
+        }
+        __goblint_check(arr[i___0][j___0] == i___0 + j___0);
+        j___0 ++;
+      }
+      while_break___12: /* CIL Label */ ;
+      }
+      loop_end___6: /* CIL Label */ ;
+      }
+      i___0 ++;
+    }
+    while_break___11: /* CIL Label */ ;
+    }
+    loop_end___7: /* CIL Label */ ;
+    }
+    return (0);
+  }
+  }
diff --git a/tests/regression/55-loop-unrolling/08-bad.t b/tests/regression/55-loop-unrolling/08-bad.t
new file mode 100644
index 0000000000..11cded728f
--- /dev/null
+++ b/tests/regression/55-loop-unrolling/08-bad.t
@@ -0,0 +1,50 @@
+  $ goblint --set lib.activated '[]' --set exp.unrolling-factor 1 --enable justcil --set dbg.justcil-printer clean 08-bad.c
+  [Info] unrolling loop at 08-bad.c:8:7-8:23 with factor 1
+  [Info] unrolling loop at 08-bad.c:14:8-14:24 with factor 1
+  int main(void) 
+  { 
+    int m ;
+  
+    {
+    {
+    goto switch_default;
+    {
+    if (! 0) {
+      goto loop_end;
+    }
+    loop_continue_0: /* CIL Label */ ;
+    switch_default: /* CIL Label */ 
+    {
+    while (1) {
+      while_continue: /* CIL Label */ ;
+      if (! 0) {
+        goto while_break;
+      }
+    }
+    while_break: /* CIL Label */ ;
+    }
+    loop_end: /* CIL Label */ ;
+    }
+    switch_break: /* CIL Label */ ;
+    }
+    goto lab;
+    {
+    if (! 0) {
+      goto loop_end___0;
+    }
+    loop_continue_0___0: /* CIL Label */ ;
+    lab: 
+    {
+    while (1) {
+      while_continue___0: /* CIL Label */ ;
+      if (! 0) {
+        goto while_break___0;
+      }
+    }
+    while_break___0: /* CIL Label */ ;
+    }
+    loop_end___0: /* CIL Label */ ;
+    }
+    return (0);
+  }
+  }
diff --git a/tests/regression/55-loop-unrolling/09-weird.t b/tests/regression/55-loop-unrolling/09-weird.t
new file mode 100644
index 0000000000..502847c46e
--- /dev/null
+++ b/tests/regression/55-loop-unrolling/09-weird.t
@@ -0,0 +1,54 @@
+  $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 2 --enable justcil --set dbg.justcil-printer clean 09-weird.c
+  [Info] unrolling loop at 09-weird.c:8:5-11:5 with factor 2
+  extern void __goblint_check(int exp ) ;
+  extern void __goblint_assume(int exp ) ;
+  extern void __goblint_assert(int exp ) ;
+  extern void __goblint_assume_join() ;
+  extern void __goblint_globalize(void *ptr ) ;
+  extern void __goblint_split_begin(int exp ) ;
+  extern void __goblint_split_end(int exp ) ;
+  extern void __goblint_bounded(unsigned long long exp ) ;
+  void main(void) 
+  { 
+    int j ;
+    int i ;
+  
+    {
+    j = 0;
+    i = 0;
+    {
+    if (! (i < 50)) {
+      goto loop_end;
+    }
+    goto somelab___0;
+    somelab___0: 
+    j = 8;
+    i ++;
+    loop_continue_0: /* CIL Label */ ;
+    if (! (i < 50)) {
+      goto loop_end;
+    }
+    goto somelab___1;
+    somelab___1: 
+    j = 8;
+    i ++;
+    loop_continue_1: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue: /* CIL Label */ ;
+      if (! (i < 50)) {
+        goto while_break;
+      }
+      goto somelab;
+      somelab: 
+      j = 8;
+      i ++;
+    }
+    while_break: /* CIL Label */ ;
+    }
+    loop_end: /* CIL Label */ ;
+    }
+    __goblint_check(j == 8);
+    return;
+  }
+  }
diff --git a/tests/regression/55-loop-unrolling/10-continue-right-place.c b/tests/regression/55-loop-unrolling/10-continue-right-place.c
new file mode 100644
index 0000000000..dd31a704c2
--- /dev/null
+++ b/tests/regression/55-loop-unrolling/10-continue-right-place.c
@@ -0,0 +1,17 @@
+// PARAM: --set lib.activated '["goblint"]' --exp.unrolling-factor 11
+#include <goblint.h>
+
+int main() {
+  int i = 0;
+  int j = 10;
+  while (i <= 10) {
+    if (i == 5) {
+      i = 7;
+      j = 3;
+      continue; // the continue should jump to the following iteration, not all the way to the unrolled loop
+    }
+    __goblint_check(i + j == 10);
+    i++; j--;
+  }
+  return 0;
+}
diff --git a/tests/regression/55-loop-unrolling/10-continue-right-place.t b/tests/regression/55-loop-unrolling/10-continue-right-place.t
new file mode 100644
index 0000000000..1daab03c52
--- /dev/null
+++ b/tests/regression/55-loop-unrolling/10-continue-right-place.t
@@ -0,0 +1,173 @@
+  $ goblint --set lib.activated '["goblint"]' --set exp.unrolling-factor 11 --enable justcil --set dbg.justcil-printer clean 10-continue-right-place.c
+  [Info] unrolling loop at 10-continue-right-place.c:7:3-15:3 with factor 11
+  extern void __goblint_check(int exp ) ;
+  extern void __goblint_assume(int exp ) ;
+  extern void __goblint_assert(int exp ) ;
+  extern void __goblint_assume_join() ;
+  extern void __goblint_globalize(void *ptr ) ;
+  extern void __goblint_split_begin(int exp ) ;
+  extern void __goblint_split_end(int exp ) ;
+  extern void __goblint_bounded(unsigned long long exp ) ;
+  int main(void) 
+  { 
+    int i ;
+    int j ;
+  
+    {
+    i = 0;
+    j = 10;
+    {
+    if (! (i <= 10)) {
+      goto loop_end;
+    }
+    if (i == 5) {
+      i = 7;
+      j = 3;
+      goto loop_continue_0;
+    }
+    __goblint_check(i + j == 10);
+    i ++;
+    j --;
+    loop_continue_0: /* CIL Label */ ;
+    if (! (i <= 10)) {
+      goto loop_end;
+    }
+    if (i == 5) {
+      i = 7;
+      j = 3;
+      goto loop_continue_1;
+    }
+    __goblint_check(i + j == 10);
+    i ++;
+    j --;
+    loop_continue_1: /* CIL Label */ ;
+    if (! (i <= 10)) {
+      goto loop_end;
+    }
+    if (i == 5) {
+      i = 7;
+      j = 3;
+      goto loop_continue_2;
+    }
+    __goblint_check(i + j == 10);
+    i ++;
+    j --;
+    loop_continue_2: /* CIL Label */ ;
+    if (! (i <= 10)) {
+      goto loop_end;
+    }
+    if (i == 5) {
+      i = 7;
+      j = 3;
+      goto loop_continue_3;
+    }
+    __goblint_check(i + j == 10);
+    i ++;
+    j --;
+    loop_continue_3: /* CIL Label */ ;
+    if (! (i <= 10)) {
+      goto loop_end;
+    }
+    if (i == 5) {
+      i = 7;
+      j = 3;
+      goto loop_continue_4;
+    }
+    __goblint_check(i + j == 10);
+    i ++;
+    j --;
+    loop_continue_4: /* CIL Label */ ;
+    if (! (i <= 10)) {
+      goto loop_end;
+    }
+    if (i == 5) {
+      i = 7;
+      j = 3;
+      goto loop_continue_5;
+    }
+    __goblint_check(i + j == 10);
+    i ++;
+    j --;
+    loop_continue_5: /* CIL Label */ ;
+    if (! (i <= 10)) {
+      goto loop_end;
+    }
+    if (i == 5) {
+      i = 7;
+      j = 3;
+      goto loop_continue_6;
+    }
+    __goblint_check(i + j == 10);
+    i ++;
+    j --;
+    loop_continue_6: /* CIL Label */ ;
+    if (! (i <= 10)) {
+      goto loop_end;
+    }
+    if (i == 5) {
+      i = 7;
+      j = 3;
+      goto loop_continue_7;
+    }
+    __goblint_check(i + j == 10);
+    i ++;
+    j --;
+    loop_continue_7: /* CIL Label */ ;
+    if (! (i <= 10)) {
+      goto loop_end;
+    }
+    if (i == 5) {
+      i = 7;
+      j = 3;
+      goto loop_continue_8;
+    }
+    __goblint_check(i + j == 10);
+    i ++;
+    j --;
+    loop_continue_8: /* CIL Label */ ;
+    if (! (i <= 10)) {
+      goto loop_end;
+    }
+    if (i == 5) {
+      i = 7;
+      j = 3;
+      goto loop_continue_9;
+    }
+    __goblint_check(i + j == 10);
+    i ++;
+    j --;
+    loop_continue_9: /* CIL Label */ ;
+    if (! (i <= 10)) {
+      goto loop_end;
+    }
+    if (i == 5) {
+      i = 7;
+      j = 3;
+      goto loop_continue_10;
+    }
+    __goblint_check(i + j == 10);
+    i ++;
+    j --;
+    loop_continue_10: /* CIL Label */ ;
+    {
+    while (1) {
+      while_continue: /* CIL Label */ ;
+      if (! (i <= 10)) {
+        goto while_break;
+      }
+      if (i == 5) {
+        i = 7;
+        j = 3;
+        goto while_continue;
+      }
+      __goblint_check(i + j == 10);
+      i ++;
+      j --;
+    }
+    while_break: /* CIL Label */ ;
+    }
+    loop_end: /* CIL Label */ ;
+    }
+    return (0);
+  }
+  }
diff --git a/tests/regression/55-loop-unrolling/dune b/tests/regression/55-loop-unrolling/dune
new file mode 100644
index 0000000000..23c0dd3290
--- /dev/null
+++ b/tests/regression/55-loop-unrolling/dune
@@ -0,0 +1,2 @@
+(cram
+ (deps (glob_files *.c)))