diff --git a/src/plugins/variadic/tests/defined/oracle/sum_with_unspecified_sequence.res.oracle b/src/plugins/variadic/tests/defined/oracle/sum_with_unspecified_sequence.res.oracle
index 6efec9870ea80f65d22584419bd259c372760eae..ec0cd665edef6bc4a3c6c325ef178fb1f9df928d 100644
--- a/src/plugins/variadic/tests/defined/oracle/sum_with_unspecified_sequence.res.oracle
+++ b/src/plugins/variadic/tests/defined/oracle/sum_with_unspecified_sequence.res.oracle
@@ -7,12 +7,12 @@
   out of bounds read. assert \valid_read((int *)*list);
 [eva:alarm] sum_with_unspecified_sequence.c:14: Warning: 
   signed overflow.
-  assert -2147483648 ≤ ret + tmp_unroll_5;
-  (tmp_unroll_5 from vararg)
+  assert -2147483648 ≤ ret + tmp_unfold_5;
+  (tmp_unfold_5 from vararg)
 [eva:alarm] sum_with_unspecified_sequence.c:14: Warning: 
   signed overflow.
-  assert ret + tmp_unroll_5 ≤ 2147483647;
-  (tmp_unroll_5 from vararg)
+  assert ret + tmp_unfold_5 ≤ 2147483647;
+  (tmp_unfold_5 from vararg)
 [eva:alarm] sum_with_unspecified_sequence.c:14: Warning: 
   out of bounds read. assert \valid_read(list);
 [eva:alarm] sum_with_unspecified_sequence.c:14: Warning: 
@@ -43,20 +43,20 @@ int sum(int n, void * const *__va_params)
   int ret = 0;
   list = __va_params;
   i = 0;
-  if (! (i < n)) goto unrolling_2_loop;
+  if (! (i < n)) goto unfolding_2_loop;
   {
-    int tmp_unroll_5;
+    int tmp_unfold_5;
     /*@ assert Eva: mem_access: \valid_read(list); */
     /*@ assert Eva: mem_access: \valid_read((int *)*list); */
-    tmp_unroll_5 = *((int *)*list);
+    tmp_unfold_5 = *((int *)*list);
     list ++;
-    /*@ assert Eva: signed_overflow: -2147483648 ≤ ret + tmp_unroll_5; */
-    /*@ assert Eva: signed_overflow: ret + tmp_unroll_5 ≤ 2147483647; */
-    ret += tmp_unroll_5;
+    /*@ assert Eva: signed_overflow: -2147483648 ≤ ret + tmp_unfold_5; */
+    /*@ assert Eva: signed_overflow: ret + tmp_unfold_5 ≤ 2147483647; */
+    ret += tmp_unfold_5;
   }
   i ++;
-  unrolling_3_loop: ;
-  /*@ loop pragma UNROLL "done", 1; */
+  unfolding_3_loop: ;
+  /*@ loop unfold "done", 1; */
   while (i < n) {
     {
       int tmp;
@@ -70,7 +70,7 @@ int sum(int n, void * const *__va_params)
     }
     i ++;
   }
-  unrolling_2_loop: ;
+  unfolding_2_loop: ;
   return ret;
 }
 
diff --git a/src/plugins/wp/tests/wp_plugin/doomed_unroll.i b/src/plugins/wp/tests/wp_plugin/doomed_unroll.i
index dd025d4817a97adde1279711cbce88670b0e1f58..bfcaec734b26c6420e7a17b56fbf50a7bad36a1c 100644
--- a/src/plugins/wp/tests/wp_plugin/doomed_unroll.i
+++ b/src/plugins/wp/tests/wp_plugin/doomed_unroll.i
@@ -10,7 +10,7 @@ void foo(void)
 {
   int n = 3 ;
   /*@
-    loop pragma UNROLL "completely", 4 ;
+    loop unfold "completely", 4 ;
   */
   while (n>0) n--;
 }
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/doomed_unroll.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/doomed_unroll.res.oracle
index 43b1f1173ae426387f7cac5252f94d1e3e2a3dc3..116eea855dee981d0162fc96b0eed3fac3e6f375 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/doomed_unroll.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/doomed_unroll.res.oracle
@@ -45,24 +45,24 @@ Prove: true.
 void foo(void)
 {
   int n = 3;
-  if (! (n > 0)) goto unrolling_2_loop;
+  if (! (n > 0)) goto unfolding_2_loop;
   n --;
-  unrolling_6_loop: ;
-  if (! (n > 0)) goto unrolling_2_loop;
+  unfolding_6_loop: ;
+  if (! (n > 0)) goto unfolding_2_loop;
   n --;
-  unrolling_5_loop: ;
-  if (! (n > 0)) goto unrolling_2_loop;
+  unfolding_5_loop: ;
+  if (! (n > 0)) goto unfolding_2_loop;
   n --;
-  unrolling_4_loop: ;
-  if (! (n > 0)) goto unrolling_2_loop;
+  unfolding_4_loop: ;
+  if (! (n > 0)) goto unfolding_2_loop;
   n --;
-  unrolling_3_loop: ;
+  unfolding_3_loop: ;
   /*@ loop invariant \false;
-      loop pragma UNROLL "completely", 4;
-      loop pragma UNROLL "done", 4;
+      loop unfold "completely", 4;
+      loop unfold "done", 4;
   */
   while (n > 0) n --;
-  unrolling_2_loop: ;
+  unfolding_2_loop: ;
   return;
 }
 
diff --git a/src/plugins/wp/tests/wp_plugin/repeat.c b/src/plugins/wp/tests/wp_plugin/repeat.c
index a060cc7c0ab55e49e68776f029670c66126ca8a7..cd53430a6b83885db09a8996ab2897ce01020138 100644
--- a/src/plugins/wp/tests/wp_plugin/repeat.c
+++ b/src/plugins/wp/tests/wp_plugin/repeat.c
@@ -43,7 +43,7 @@ void master(void)
 */
 void unroll(void)
 {
-  /*@ loop pragma UNROLL "completely", U; */
+  /*@ loop unfold "completely", U; */
   for (int i = 0; i < N; i++)
     { f(); g(); }
   return;
@@ -57,7 +57,7 @@ void unroll(void)
 */
 void induction(int n)
 {
-  /*@ 
+  /*@
     loop invariant 0 <= i <= n;
     loop invariant CALL == [| F , G |] *^ i;
     loop assigns i,calls;
@@ -77,8 +77,8 @@ void induction(int n)
 void shifted(int n)
 {
   f();
-  
-  /*@ 
+
+  /*@
     loop invariant 0 <= i <= n;
     loop invariant CALL == ([| F , G |] *^ i ^ [| F |]);
     loop assigns i,calls;
diff --git a/src/plugins/wp/tests/wp_plugin/unroll.i b/src/plugins/wp/tests/wp_plugin/unroll.i
index f6feda1b587b987794cc4103c1e4e3ea853c7af4..54a94e25d7bf95a639bdea492a9113593b170982 100644
--- a/src/plugins/wp/tests/wp_plugin/unroll.i
+++ b/src/plugins/wp/tests/wp_plugin/unroll.i
@@ -17,6 +17,6 @@ enum {Max = 16};
   @ ensures zero: zeroed(t,0,Max-1);
  */
 void unrolled_loop(unsigned *t){
-  //@ loop pragma UNROLL "completely", Max+1;
+  //@ loop unfold "completely", Max+1;
   for (unsigned i=0; i<Max; i++) t[i] = 0;
 }
diff --git a/tests/cil/comments.c b/tests/cil/comments.c
index ed0252e15d2097202b8de8897ba5d035f0a5b774..0c0e9d3efd8115687494a5daeaa72a8febc93414 100644
--- a/tests/cil/comments.c
+++ b/tests/cil/comments.c
@@ -19,7 +19,7 @@ int bts_2176() {
      1 */
   r = /* comment 2 */ 1;
 
-  //@ loop pragma UNROLL 10;
+  //@ loop unfold 10;
   for(i=0; i<10; i++) {
     r += 1;
   }
diff --git a/tests/cil/oracle/comments.res.oracle b/tests/cil/oracle/comments.res.oracle
index fd7b14f4298869cf6f9b582765cbae96ae941a3a..479418c36083c669ce17c0711d3dbf87a31e0963 100644
--- a/tests/cil/oracle/comments.res.oracle
+++ b/tests/cil/oracle/comments.res.oracle
@@ -30,53 +30,53 @@ int bts_2176(void)
   // comment 2 
   r = 1;
   i = 0;
-  if (! (i < 10)) goto unrolling_2_loop;
+  if (! (i < 10)) goto unfolding_2_loop;
   r ++;
   i ++;
-  unrolling_12_loop: ;
-  if (! (i < 10)) goto unrolling_2_loop;
+  unfolding_12_loop: ;
+  if (! (i < 10)) goto unfolding_2_loop;
   r ++;
   i ++;
-  unrolling_11_loop: ;
-  if (! (i < 10)) goto unrolling_2_loop;
+  unfolding_11_loop: ;
+  if (! (i < 10)) goto unfolding_2_loop;
   r ++;
   i ++;
-  unrolling_10_loop: ;
-  if (! (i < 10)) goto unrolling_2_loop;
+  unfolding_10_loop: ;
+  if (! (i < 10)) goto unfolding_2_loop;
   r ++;
   i ++;
-  unrolling_9_loop: ;
-  if (! (i < 10)) goto unrolling_2_loop;
+  unfolding_9_loop: ;
+  if (! (i < 10)) goto unfolding_2_loop;
   r ++;
   i ++;
-  unrolling_8_loop: ;
-  if (! (i < 10)) goto unrolling_2_loop;
+  unfolding_8_loop: ;
+  if (! (i < 10)) goto unfolding_2_loop;
   r ++;
   i ++;
-  unrolling_7_loop: ;
-  if (! (i < 10)) goto unrolling_2_loop;
+  unfolding_7_loop: ;
+  if (! (i < 10)) goto unfolding_2_loop;
   r ++;
   i ++;
-  unrolling_6_loop: ;
-  if (! (i < 10)) goto unrolling_2_loop;
+  unfolding_6_loop: ;
+  if (! (i < 10)) goto unfolding_2_loop;
   r ++;
   i ++;
-  unrolling_5_loop: ;
-  if (! (i < 10)) goto unrolling_2_loop;
+  unfolding_5_loop: ;
+  if (! (i < 10)) goto unfolding_2_loop;
   r ++;
   i ++;
-  unrolling_4_loop: ;
-  if (! (i < 10)) goto unrolling_2_loop;
+  unfolding_4_loop: ;
+  if (! (i < 10)) goto unfolding_2_loop;
   r ++;
   i ++;
-  unrolling_3_loop: ;
-  /*@ loop pragma UNROLL 10;
-      loop pragma UNROLL "done", 10; */
+  unfolding_3_loop: ;
+  /*@ loop unfold 10;
+      loop unfold "done", 10; */
   while (i < 10) {
     r ++;
     i ++;
   }
-  unrolling_2_loop: ;
+  unfolding_2_loop: ;
   // comment 3 
   return r;
 }
diff --git a/tests/float/round10d.i b/tests/float/round10d.i
index 4dfa2710f349811eb8a9063e035a7a5041fee846..30b33d4d7f5f5a7a7b0b9f3637e6c9481f1db014 100644
--- a/tests/float/round10d.i
+++ b/tests/float/round10d.i
@@ -7,12 +7,12 @@ int main()
    double t=0.0;
    int i;
    Frama_C_show_each_dixieme(0.1);
-   //@ loop pragma UNROLL 10;
-   for(i=0;i<10;i++) 
-     { 
+   //@ loop unfold 10;
+   for(i=0;i<10;i++)
+     {
        t = t + 0.1;
        Frama_C_show_each_t(t);
-     }    
+     }
    //@ assert t>=1.0;
    return 0;
 }
diff --git a/tests/idct/ieee_1180_1990.c b/tests/idct/ieee_1180_1990.c
index 90bc2edd2edd91cf7500e146ca51c0e12603245a..a7083537cbc36424e79c3b63d55ddddaa65ab29e 100644
--- a/tests/idct/ieee_1180_1990.c
+++ b/tests/idct/ieee_1180_1990.c
@@ -173,7 +173,7 @@ int main()
   long i, j, k, m1[8][8], m2[8][8], m3[8][8], m4[8][8], succ, omse, ome, err;
 
   succ = 1;
-/*@ loop pragma UNROLL 7; */
+/*@ loop unfold 7; */
   for(i = 0; i < 6; i++)
     for(j = 0; j < 8; j++)
       for(k = 0; k < 8; k++)
@@ -198,7 +198,7 @@ int main()
     }
   /*fprintf(stderr, "------------------------------------------------->\n");*/
 
-/* loop pragma UNROLL 0 */
+/* loop unfold 0 */
   for(i = 0; i < 10000; i++)
     {
     if((i + 1) % 200 == 0)
diff --git a/tests/metrics/cabs.i b/tests/metrics/cabs.i
index 0d86a7db0f7fdebb32f0b437cb5eeda624530b5b..e910d23f0dfe3852b537c10803c1ce52eb683abe 100644
--- a/tests/metrics/cabs.i
+++ b/tests/metrics/cabs.i
@@ -4,7 +4,7 @@
 
 void main() {
   int j = 1;
-  //@ loop pragma UNROLL 6;
+  //@ loop unfold 6;
   for (int i=0; i<6; i++) {
     j += 2;
   }
diff --git a/tests/misc/oracle/bts1135_ulevel.res.oracle b/tests/misc/oracle/bts1135_ulevel.res.oracle
index bb6bb5dec9af88ecf46b59b0cb968ef27a89db6e..22da8c05b0c9c9d81797a6ac1ac96773eeb594c7 100644
--- a/tests/misc/oracle/bts1135_ulevel.res.oracle
+++ b/tests/misc/oracle/bts1135_ulevel.res.oracle
@@ -4,23 +4,23 @@ int X;
 void main(int c)
 {
   int i = 0;
-  if (! (i < 10)) goto unrolling_2_loop;
+  if (! (i < 10)) goto unfolding_2_loop;
   if (c) 
     /*@ ensures \false; */
-    goto there_unrolling_6_loop;
+    goto there_unfolding_6_loop;
   X ++;
-  there_unrolling_6_loop: i ++;
-  /*@ assert c ≡ 0 ⇒ \at(X,there_unrolling_6_loop) ≡ i + 1; */ ;
-  unrolling_5_loop: ;
-  if (! (i < 10)) goto unrolling_2_loop;
+  there_unfolding_6_loop: i ++;
+  /*@ assert c ≡ 0 ⇒ \at(X,there_unfolding_6_loop) ≡ i + 1; */ ;
+  unfolding_5_loop: ;
+  if (! (i < 10)) goto unfolding_2_loop;
   if (c) 
     /*@ ensures \false; */
-    goto there_unrolling_4_loop;
+    goto there_unfolding_4_loop;
   X ++;
-  there_unrolling_4_loop: i ++;
-  /*@ assert c ≡ 0 ⇒ \at(X,there_unrolling_4_loop) ≡ i + 1; */ ;
-  unrolling_3_loop: ;
-  /*@ loop pragma UNROLL "done", 2; */
+  there_unfolding_4_loop: i ++;
+  /*@ assert c ≡ 0 ⇒ \at(X,there_unfolding_4_loop) ≡ i + 1; */ ;
+  unfolding_3_loop: ;
+  /*@ loop unfold "done", 2; */
   while (i < 10) {
     if (c) 
       /*@ ensures \false; */
@@ -29,7 +29,7 @@ void main(int c)
     there: i ++;
     /*@ assert c ≡ 0 ⇒ \at(X,there) ≡ i + 1; */ ;
   }
-  unrolling_2_loop: ;
+  unfolding_2_loop: ;
   return;
 }
 
diff --git a/tests/misc/ulevel.i b/tests/misc/ulevel.i
index dbfc67d7c9082ea9ccc854eab15ae0d2e7743a6e..d18729eb2637afa1611d8b065d735d6a746497d3 100644
--- a/tests/misc/ulevel.i
+++ b/tests/misc/ulevel.i
@@ -8,7 +8,7 @@
 
 void main(void) {
   int i, j;
-  /*@ loop pragma UNROLL 1; */
+  /*@ loop unfold 1; */
   for(i = 0; i < 4; i++)
     for(j = 0; j < 3; j++)
       ;
diff --git a/tests/slicing/oracle/adpcm.res.oracle b/tests/slicing/oracle/adpcm.res.oracle
index d064224755afa3c264138d1ff4795db2f1dc9feb..e11347f6b738faa43180943c3f74d12bf725a745 100644
--- a/tests/slicing/oracle/adpcm.res.oracle
+++ b/tests/slicing/oracle/adpcm.res.oracle
@@ -1531,6 +1531,12 @@ Slicing project worklist [default] =
 [pdg] computing for function logscl
 [pdg] done for function logscl
 [slicing] applying actions: 3/3...
+[slicing] tests/test/adpcm.c:277: Warning: Dropping unsupported ACSL annotation
+[slicing] tests/test/adpcm.c:288: Warning: Dropping unsupported ACSL annotation
+[slicing] tests/test/adpcm.c:418: Warning: Dropping unsupported ACSL annotation
+[slicing] tests/test/adpcm.c:453: Warning: Dropping unsupported ACSL annotation
+[slicing] tests/test/adpcm.c:506: Warning: Dropping unsupported ACSL annotation
+[slicing] tests/test/adpcm.c:512: Warning: Dropping unsupported ACSL annotation
 [slicing] tests/test/adpcm.c:607: Warning: Dropping unsupported ACSL annotation
 [sparecode] remove unused global declarations from project 'Sliced code tmp'
 [sparecode] removed unused global declarations in new project 'Sliced code'
@@ -1822,7 +1828,6 @@ void encode_slice_1(int xin1, int xin2)
   h_ptr ++;
   xb = (long)*tmp_1 * (long)*tmp_2;
   i = 0;
-  /*@ loop pragma UNROLL 11; */
   while (i < 10) {
     {
       int *tmp_3;
@@ -1851,7 +1856,6 @@ void encode_slice_1(int xin1, int xin2)
   xb += (long)*tqmf_ptr * (long)*tmp_9;
   tqmf_ptr1 = tqmf_ptr - 2;
   i = 0;
-  /*@ loop pragma UNROLL 23; */
   while (i < 22) {
     int *tmp_10;
     int *tmp_11;
@@ -1921,7 +1925,6 @@ int filtez_slice_1(int *bpl, int *dlt_0)
   dlt_0 ++;
   zl = (long)*tmp * (long)*tmp_0;
   i = 1;
-  /*@ loop pragma UNROLL 7; */
   while (i < 6) {
     int *tmp_1;
     int *tmp_2;
@@ -1958,7 +1961,6 @@ int quantl_slice_1(int el_0, int detl_0)
   wd = (long)abs_slice_1(el_0);
   mil = 0;
   decis = (long)decis_levl[mil] * (long)detl_0 >> 15L;
-  /*@ loop pragma UNROLL 30; */
   while (1) {
     if (wd <= decis) {
       if (! (mil < 29)) break;
@@ -2001,7 +2003,6 @@ void upzero_slice_1(int dlt_0, int *dlti, int *bli)
   int wd3;
   if (dlt_0 == 0) {
     i = 0;
-    /*@ loop pragma UNROLL 7; */
     while (i < 6) {
       *(bli + i) = (int)(255L * (long)*(bli + i) >> 8L);
       i ++;
@@ -2009,7 +2010,6 @@ void upzero_slice_1(int dlt_0, int *dlti, int *bli)
   }
   else {
     i = 0;
-    /*@ loop pragma UNROLL 7; */
     while (i < 6) {
       if ((long)dlt_0 * (long)*(dlti + i) >= (long)0) wd2 = 128;
       else wd2 = -128;
@@ -2071,7 +2071,6 @@ void main(void)
 {
   int i;
   i = 0;
-  /*@ loop pragma UNROLL 11; */
   while (i < 10) {
     encode_slice_1(test_data[i],test_data[i + 1]);
     i += 2;
diff --git a/tests/slicing/oracle/bts1768.res.oracle b/tests/slicing/oracle/bts1768.res.oracle
index 9fd462bcb24a07984cbe4e86e1297a9fd5df86cd..d6c24f06c67449fb82f0c84c046be674c40fb4aa 100644
--- a/tests/slicing/oracle/bts1768.res.oracle
+++ b/tests/slicing/oracle/bts1768.res.oracle
@@ -163,6 +163,7 @@
 [slicing] exporting project to 'Slicing export'...
 [slicing] applying all slicing requests...
 [slicing] applying 0 actions...
+[slicing] bts1768.i:44: Warning: Dropping unsupported ACSL annotation
 [sparecode] remove unused global declarations from project 'Slicing export tmp'
 [sparecode] removed unused global declarations in new project 'Slicing export'
 /* Generated by Frama-C */
@@ -226,7 +227,6 @@ void main(void)
   lecture_slice_1();
   fsm_transition_slice_1();
   step ++;
-  /*@ loop pragma UNROLL "done", 10; */
   while (1) {
     lecture_slice_1();
     fsm_transition_slice_1();
diff --git a/tests/spec/breaks_continues_unroll.i b/tests/spec/breaks_continues_unroll.i
index fed8f02091708994c1d2897d15f0ed8264547130..e5f7bf977dfc3bdb42c074ed39fc9a176c846c5b 100644
--- a/tests/spec/breaks_continues_unroll.i
+++ b/tests/spec/breaks_continues_unroll.i
@@ -3,13 +3,13 @@
 // Semantics of unrolling
 int unroll (int c) {
   int x = 0;
-  //@ loop pragma UNROLL 1;
+  //@ loop unfold 1;
   while (1) {
     /*@ breaks \false;
         continues x == \old(x) + 1; */
     switch (x) {
       /*@ breaks x == 13; */
-      { 
+      {
       case 11: x++; continue;
       case 12: x++;
       case 13: break;
@@ -24,4 +24,4 @@ int unroll (int c) {
     }
   }
   return x;
-}	
+}
diff --git a/tests/spec/loop_labels_unroll.i b/tests/spec/loop_labels_unroll.i
index cec4e93183fa944c5ac2ff6e2c929177fb1d8287..30df6b4f1be74c2a71f2213239cddb26ad91dca5 100644
--- a/tests/spec/loop_labels_unroll.i
+++ b/tests/spec/loop_labels_unroll.i
@@ -2,8 +2,8 @@ int main () {
 
   int x = 0;
 
-  /*@ 
-    loop pragma UNROLL 4;
+  /*@
+    loop unfold 4;
     loop invariant \at(x,LoopEntry) == 0;
     loop invariant \at(x,LoopCurrent) <= 15;
   */
diff --git a/tests/spec/oracle/breaks_continues_unroll.res.oracle b/tests/spec/oracle/breaks_continues_unroll.res.oracle
index 245cc34841f9d3bcf3bad7daa9ca820a8614bd41..cdb607de3549603aab89e51163d10e4093c7bb8a 100644
--- a/tests/spec/oracle/breaks_continues_unroll.res.oracle
+++ b/tests/spec/oracle/breaks_continues_unroll.res.oracle
@@ -7,7 +7,7 @@ int unroll(int c)
     /*@ breaks x ≡ 13; */
     {
       case 11: x ++;
-      goto unrolling_3_loop;
+      goto unfolding_3_loop;
       case 12: x ++;
       case 13: break;
       default: ;
@@ -15,12 +15,12 @@ int unroll(int c)
   }
   if (x < c) {
     x ++;
-    goto unrolling_3_loop;
+    goto unfolding_3_loop;
   }
-  goto unrolling_2_loop;
-  unrolling_3_loop: ;
-  /*@ loop pragma UNROLL 1;
-      loop pragma UNROLL "done", 1; */
+  goto unfolding_2_loop;
+  unfolding_3_loop: ;
+  /*@ loop unfold 1;
+      loop unfold "done", 1; */
   while (1) {
     /*@ breaks \false;
         continues x ≡ \old(x) + 1; */
@@ -44,7 +44,7 @@ int unroll(int c)
       break;
     }
   }
-  unrolling_2_loop: ;
+  unfolding_2_loop: ;
   return x;
 }
 
diff --git a/tests/spec/oracle/loop_labels_unroll.res.oracle b/tests/spec/oracle/loop_labels_unroll.res.oracle
index 84a3ca289907e1062d26b481dbadf834211b3eec..998a9bb7d2336ed96da0c577700868acad763250 100644
--- a/tests/spec/oracle/loop_labels_unroll.res.oracle
+++ b/tests/spec/oracle/loop_labels_unroll.res.oracle
@@ -4,63 +4,63 @@ int main(void)
 {
   int __retres;
   int x = 0;
-  unrolling_7_loop: ;
-  if (! (x < 15)) goto unrolling_2_loop;
+  unfolding_7_loop: ;
+  if (! (x < 15)) goto unfolding_2_loop;
   {
     x ++;
-    /*@ assert x ≡ \at(x,unrolling_7_loop) + 1; */ ;
-    int i_unroll_32 = 0;
-    /*@ loop invariant \at(i_unroll_32,LoopEntry) ≡ 0; */
-    while (i_unroll_32 < 4) {
-      i_unroll_32 ++;
-      /*@ assert \at(i_unroll_32,LoopCurrent) ≡ i_unroll_32 - 1; */ ;
+    /*@ assert x ≡ \at(x,unfolding_7_loop) + 1; */ ;
+    int i_unfold_32 = 0;
+    /*@ loop invariant \at(i_unfold_32,LoopEntry) ≡ 0; */
+    while (i_unfold_32 < 4) {
+      i_unfold_32 ++;
+      /*@ assert \at(i_unfold_32,LoopCurrent) ≡ i_unfold_32 - 1; */ ;
     }
-    /*@ assert i_unroll_32 > 0; */ ;
+    /*@ assert i_unfold_32 > 0; */ ;
   }
-  unrolling_6_loop: ;
-  if (! (x < 15)) goto unrolling_2_loop;
+  unfolding_6_loop: ;
+  if (! (x < 15)) goto unfolding_2_loop;
   {
     x ++;
-    /*@ assert x ≡ \at(x,unrolling_6_loop) + 1; */ ;
-    int i_unroll_24 = 0;
-    /*@ loop invariant \at(i_unroll_24,LoopEntry) ≡ 0; */
-    while (i_unroll_24 < 4) {
-      i_unroll_24 ++;
-      /*@ assert \at(i_unroll_24,LoopCurrent) ≡ i_unroll_24 - 1; */ ;
+    /*@ assert x ≡ \at(x,unfolding_6_loop) + 1; */ ;
+    int i_unfold_24 = 0;
+    /*@ loop invariant \at(i_unfold_24,LoopEntry) ≡ 0; */
+    while (i_unfold_24 < 4) {
+      i_unfold_24 ++;
+      /*@ assert \at(i_unfold_24,LoopCurrent) ≡ i_unfold_24 - 1; */ ;
     }
-    /*@ assert i_unroll_24 > 0; */ ;
+    /*@ assert i_unfold_24 > 0; */ ;
   }
-  unrolling_5_loop: ;
-  if (! (x < 15)) goto unrolling_2_loop;
+  unfolding_5_loop: ;
+  if (! (x < 15)) goto unfolding_2_loop;
   {
     x ++;
-    /*@ assert x ≡ \at(x,unrolling_5_loop) + 1; */ ;
-    int i_unroll_16 = 0;
-    /*@ loop invariant \at(i_unroll_16,LoopEntry) ≡ 0; */
-    while (i_unroll_16 < 4) {
-      i_unroll_16 ++;
-      /*@ assert \at(i_unroll_16,LoopCurrent) ≡ i_unroll_16 - 1; */ ;
+    /*@ assert x ≡ \at(x,unfolding_5_loop) + 1; */ ;
+    int i_unfold_16 = 0;
+    /*@ loop invariant \at(i_unfold_16,LoopEntry) ≡ 0; */
+    while (i_unfold_16 < 4) {
+      i_unfold_16 ++;
+      /*@ assert \at(i_unfold_16,LoopCurrent) ≡ i_unfold_16 - 1; */ ;
     }
-    /*@ assert i_unroll_16 > 0; */ ;
+    /*@ assert i_unfold_16 > 0; */ ;
   }
-  unrolling_4_loop: ;
-  if (! (x < 15)) goto unrolling_2_loop;
+  unfolding_4_loop: ;
+  if (! (x < 15)) goto unfolding_2_loop;
   {
     x ++;
-    /*@ assert x ≡ \at(x,unrolling_4_loop) + 1; */ ;
-    int i_unroll_8 = 0;
-    /*@ loop invariant \at(i_unroll_8,LoopEntry) ≡ 0; */
-    while (i_unroll_8 < 4) {
-      i_unroll_8 ++;
-      /*@ assert \at(i_unroll_8,LoopCurrent) ≡ i_unroll_8 - 1; */ ;
+    /*@ assert x ≡ \at(x,unfolding_4_loop) + 1; */ ;
+    int i_unfold_8 = 0;
+    /*@ loop invariant \at(i_unfold_8,LoopEntry) ≡ 0; */
+    while (i_unfold_8 < 4) {
+      i_unfold_8 ++;
+      /*@ assert \at(i_unfold_8,LoopCurrent) ≡ i_unfold_8 - 1; */ ;
     }
-    /*@ assert i_unroll_8 > 0; */ ;
+    /*@ assert i_unfold_8 > 0; */ ;
   }
-  unrolling_3_loop: ;
+  unfolding_3_loop: ;
   /*@ loop invariant \at(x,LoopEntry) ≡ 0;
       loop invariant \at(x,LoopCurrent) ≤ 15;
-      loop pragma UNROLL 4;
-      loop pragma UNROLL "done", 4;
+      loop unfold 4;
+      loop unfold "done", 4;
   */
   while (x < 15) {
     x ++;
@@ -73,7 +73,7 @@ int main(void)
     }
     /*@ assert i > 0; */ ;
   }
-  unrolling_2_loop: ;
+  unfolding_2_loop: ;
   __retres = 0;
   return __retres;
 }
diff --git a/tests/syntax/oracle/loop-case-switch-for-unroll.1.res.oracle b/tests/syntax/oracle/loop-case-switch-for-unroll.1.res.oracle
index b621427cab8dac8e73a195e76afd3ecc0c369df9..9e7552621ea4658d179135a9ccc80236d75d9088 100644
--- a/tests/syntax/oracle/loop-case-switch-for-unroll.1.res.oracle
+++ b/tests/syntax/oracle/loop-case-switch-for-unroll.1.res.oracle
@@ -174,61 +174,61 @@ void main(void)
     tmp_0 = gen_nondet(68);
     if (tmp_0) goto L1;
     {
-      int tmp_1_unroll_41;
-      case 1: tmp_1_unroll_41 = gen_nondet(71);
-      if (tmp_1_unroll_41) goto L1_unrolling_11_loop;
-      L_unrolling_8_loop: x = y;
+      int tmp_1_unfold_41;
+      case 1: tmp_1_unfold_41 = gen_nondet(71);
+      if (tmp_1_unfold_41) goto L1_unfolding_11_loop;
+      L_unfolding_8_loop: x = y;
       case 2:
       {
-        int j_unroll_40;
-        int i_unroll_40 = 0;
-        if (! (i_unroll_40 < 4)) goto unrolling_2_loop_unrolling_12_loop;
+        int j_unfold_40;
+        int i_unfold_40 = 0;
+        if (! (i_unfold_40 < 4)) goto unfolding_2_loop_unfolding_12_loop;
         {
-          int tmp_2_unroll_12_unroll_26;
-          int tmp_3_unroll_12_unroll_26;
-          int tmp_4_unroll_12_unroll_26;
-          int tmp_5_unroll_12_unroll_26;
-          L1_unrolling_4_loop_unrolling_9_loop: j_unroll_40 = gen_nondet(76);
-          tmp_2_unroll_12_unroll_26 = gen_nondet(77);
-          if (tmp_2_unroll_12_unroll_26 > 10) i_unroll_40 = 10;
-          else i_unroll_40 = 0;
-          Frama_C_show_each_i_(i_unroll_40);
-          tmp_3_unroll_12_unroll_26 = gen_nondet(79);
-          if (tmp_3_unroll_12_unroll_26) goto L_unrolling_8_loop;
-          tmp_4_unroll_12_unroll_26 = gen_nondet(80);
-          if (tmp_4_unroll_12_unroll_26) goto L0;
-          tmp_5_unroll_12_unroll_26 = gen_nondet(81);
-          if (tmp_5_unroll_12_unroll_26) goto L3;
+          int tmp_2_unfold_12_unfold_26;
+          int tmp_3_unfold_12_unfold_26;
+          int tmp_4_unfold_12_unfold_26;
+          int tmp_5_unfold_12_unfold_26;
+          L1_unfolding_4_loop_unfolding_9_loop: j_unfold_40 = gen_nondet(76);
+          tmp_2_unfold_12_unfold_26 = gen_nondet(77);
+          if (tmp_2_unfold_12_unfold_26 > 10) i_unfold_40 = 10;
+          else i_unfold_40 = 0;
+          Frama_C_show_each_i_(i_unfold_40);
+          tmp_3_unfold_12_unfold_26 = gen_nondet(79);
+          if (tmp_3_unfold_12_unfold_26) goto L_unfolding_8_loop;
+          tmp_4_unfold_12_unfold_26 = gen_nondet(80);
+          if (tmp_4_unfold_12_unfold_26) goto L0;
+          tmp_5_unfold_12_unfold_26 = gen_nondet(81);
+          if (tmp_5_unfold_12_unfold_26) goto L3;
         }
-        i_unroll_40 ++;
-        unrolling_3_loop_unrolling_10_loop: ;
-        /*@ loop pragma UNROLL "done", 1; */
-        while (i_unroll_40 < 4) {
+        i_unfold_40 ++;
+        unfolding_3_loop_unfolding_10_loop: ;
+        /*@ loop unfold "done", 1; */
+        while (i_unfold_40 < 4) {
           {
-            int tmp_2_unroll_37;
-            int tmp_3_unroll_37;
-            int tmp_4_unroll_37;
-            int tmp_5_unroll_37;
-            L1_unrolling_11_loop: j_unroll_40 = gen_nondet(76);
-            tmp_2_unroll_37 = gen_nondet(77);
-            if (tmp_2_unroll_37 > 10) i_unroll_40 = 10; else i_unroll_40 = 0;
-            Frama_C_show_each_i_(i_unroll_40);
-            tmp_3_unroll_37 = gen_nondet(79);
-            if (tmp_3_unroll_37) goto L_unrolling_8_loop;
-            tmp_4_unroll_37 = gen_nondet(80);
-            if (tmp_4_unroll_37) goto L0;
-            tmp_5_unroll_37 = gen_nondet(81);
-            if (tmp_5_unroll_37) goto L3;
+            int tmp_2_unfold_37;
+            int tmp_3_unfold_37;
+            int tmp_4_unfold_37;
+            int tmp_5_unfold_37;
+            L1_unfolding_11_loop: j_unfold_40 = gen_nondet(76);
+            tmp_2_unfold_37 = gen_nondet(77);
+            if (tmp_2_unfold_37 > 10) i_unfold_40 = 10; else i_unfold_40 = 0;
+            Frama_C_show_each_i_(i_unfold_40);
+            tmp_3_unfold_37 = gen_nondet(79);
+            if (tmp_3_unfold_37) goto L_unfolding_8_loop;
+            tmp_4_unfold_37 = gen_nondet(80);
+            if (tmp_4_unfold_37) goto L0;
+            tmp_5_unfold_37 = gen_nondet(81);
+            if (tmp_5_unfold_37) goto L3;
           }
-          i_unroll_40 ++;
+          i_unfold_40 ++;
         }
-        unrolling_2_loop_unrolling_12_loop: ;
+        unfolding_2_loop_unfolding_12_loop: ;
       }
     }
     n --;
-    if (! (n > 0)) goto unrolling_6_loop;
-    unrolling_7_loop: ;
-    /*@ loop pragma UNROLL "done", 1; */
+    if (! (n > 0)) goto unfolding_6_loop;
+    unfolding_7_loop: ;
+    /*@ loop unfold "done", 1; */
     while (1) {
       {
         int tmp_1;
@@ -238,26 +238,26 @@ void main(void)
         {
           int j;
           int i = 0;
-          if (! (i < 4)) goto unrolling_2_loop;
+          if (! (i < 4)) goto unfolding_2_loop;
           {
-            int tmp_2_unroll_12;
-            int tmp_3_unroll_12;
-            int tmp_4_unroll_12;
-            int tmp_5_unroll_12;
-            L1_unrolling_4_loop: j = gen_nondet(76);
-            tmp_2_unroll_12 = gen_nondet(77);
-            if (tmp_2_unroll_12 > 10) i = 10; else i = 0;
+            int tmp_2_unfold_12;
+            int tmp_3_unfold_12;
+            int tmp_4_unfold_12;
+            int tmp_5_unfold_12;
+            L1_unfolding_4_loop: j = gen_nondet(76);
+            tmp_2_unfold_12 = gen_nondet(77);
+            if (tmp_2_unfold_12 > 10) i = 10; else i = 0;
             Frama_C_show_each_i_(i);
-            tmp_3_unroll_12 = gen_nondet(79);
-            if (tmp_3_unroll_12) goto L;
-            tmp_4_unroll_12 = gen_nondet(80);
-            if (tmp_4_unroll_12) goto L0;
-            tmp_5_unroll_12 = gen_nondet(81);
-            if (tmp_5_unroll_12) goto L3;
+            tmp_3_unfold_12 = gen_nondet(79);
+            if (tmp_3_unfold_12) goto L;
+            tmp_4_unfold_12 = gen_nondet(80);
+            if (tmp_4_unfold_12) goto L0;
+            tmp_5_unfold_12 = gen_nondet(81);
+            if (tmp_5_unfold_12) goto L3;
           }
           i ++;
-          unrolling_3_loop: ;
-          /*@ loop pragma UNROLL "done", 1; */
+          unfolding_3_loop: ;
+          /*@ loop unfold "done", 1; */
           while (i < 4) {
             {
               int tmp_2;
@@ -277,13 +277,13 @@ void main(void)
             }
             i ++;
           }
-          unrolling_2_loop: ;
+          unfolding_2_loop: ;
         }
       }
       n --;
       if (! (n > 0)) break;
     }
-    unrolling_6_loop: ;
+    unfolding_6_loop: ;
     Frama_C_show_each_y_(y);
     Frama_C_show_each_x_(x);
   }
diff --git a/tests/syntax/oracle/loop-case-switch-for-unroll.2.res.oracle b/tests/syntax/oracle/loop-case-switch-for-unroll.2.res.oracle
index 85a47d4d093e1f69a954b43b88513bd9b84e05c6..d19de9df259672fab55369c3409b3c4ac24876ff 100644
--- a/tests/syntax/oracle/loop-case-switch-for-unroll.2.res.oracle
+++ b/tests/syntax/oracle/loop-case-switch-for-unroll.2.res.oracle
@@ -174,160 +174,160 @@ void main(void)
     tmp_0 = gen_nondet(68);
     if (tmp_0) goto L1;
     {
-      int tmp_1_unroll_106;
-      case 1: tmp_1_unroll_106 = gen_nondet(71);
-      if (tmp_1_unroll_106) goto L1_unrolling_23_loop;
-      L_unrolling_18_loop: x = y;
+      int tmp_1_unfold_106;
+      case 1: tmp_1_unfold_106 = gen_nondet(71);
+      if (tmp_1_unfold_106) goto L1_unfolding_23_loop;
+      L_unfolding_18_loop: x = y;
       case 2:
       {
-        int j_unroll_105;
-        int i_unroll_105 = 0;
-        if (! (i_unroll_105 < 4)) goto unrolling_2_loop_unrolling_24_loop;
+        int j_unfold_105;
+        int i_unfold_105 = 0;
+        if (! (i_unfold_105 < 4)) goto unfolding_2_loop_unfolding_24_loop;
         {
-          int tmp_2_unroll_24_unroll_80;
-          int tmp_3_unroll_24_unroll_80;
-          int tmp_4_unroll_24_unroll_80;
-          int tmp_5_unroll_24_unroll_80;
-          L1_unrolling_6_loop_unrolling_19_loop:
-          j_unroll_105 = gen_nondet(76);
-          tmp_2_unroll_24_unroll_80 = gen_nondet(77);
-          if (tmp_2_unroll_24_unroll_80 > 10) i_unroll_105 = 10;
-          else i_unroll_105 = 0;
-          Frama_C_show_each_i_(i_unroll_105);
-          tmp_3_unroll_24_unroll_80 = gen_nondet(79);
-          if (tmp_3_unroll_24_unroll_80) goto L_unrolling_18_loop;
-          tmp_4_unroll_24_unroll_80 = gen_nondet(80);
-          if (tmp_4_unroll_24_unroll_80) goto L0;
-          tmp_5_unroll_24_unroll_80 = gen_nondet(81);
-          if (tmp_5_unroll_24_unroll_80) goto L3;
+          int tmp_2_unfold_24_unfold_80;
+          int tmp_3_unfold_24_unfold_80;
+          int tmp_4_unfold_24_unfold_80;
+          int tmp_5_unfold_24_unfold_80;
+          L1_unfolding_6_loop_unfolding_19_loop:
+          j_unfold_105 = gen_nondet(76);
+          tmp_2_unfold_24_unfold_80 = gen_nondet(77);
+          if (tmp_2_unfold_24_unfold_80 > 10) i_unfold_105 = 10;
+          else i_unfold_105 = 0;
+          Frama_C_show_each_i_(i_unfold_105);
+          tmp_3_unfold_24_unfold_80 = gen_nondet(79);
+          if (tmp_3_unfold_24_unfold_80) goto L_unfolding_18_loop;
+          tmp_4_unfold_24_unfold_80 = gen_nondet(80);
+          if (tmp_4_unfold_24_unfold_80) goto L0;
+          tmp_5_unfold_24_unfold_80 = gen_nondet(81);
+          if (tmp_5_unfold_24_unfold_80) goto L3;
         }
-        i_unroll_105 ++;
-        unrolling_5_loop_unrolling_20_loop: ;
-        if (! (i_unroll_105 < 4)) goto unrolling_2_loop_unrolling_24_loop;
+        i_unfold_105 ++;
+        unfolding_5_loop_unfolding_20_loop: ;
+        if (! (i_unfold_105 < 4)) goto unfolding_2_loop_unfolding_24_loop;
         {
-          int tmp_2_unroll_12_unroll_91;
-          int tmp_3_unroll_12_unroll_91;
-          int tmp_4_unroll_12_unroll_91;
-          int tmp_5_unroll_12_unroll_91;
-          L1_unrolling_4_loop_unrolling_21_loop:
-          j_unroll_105 = gen_nondet(76);
-          tmp_2_unroll_12_unroll_91 = gen_nondet(77);
-          if (tmp_2_unroll_12_unroll_91 > 10) i_unroll_105 = 10;
-          else i_unroll_105 = 0;
-          Frama_C_show_each_i_(i_unroll_105);
-          tmp_3_unroll_12_unroll_91 = gen_nondet(79);
-          if (tmp_3_unroll_12_unroll_91) goto L_unrolling_18_loop;
-          tmp_4_unroll_12_unroll_91 = gen_nondet(80);
-          if (tmp_4_unroll_12_unroll_91) goto L0;
-          tmp_5_unroll_12_unroll_91 = gen_nondet(81);
-          if (tmp_5_unroll_12_unroll_91) goto L3;
+          int tmp_2_unfold_12_unfold_91;
+          int tmp_3_unfold_12_unfold_91;
+          int tmp_4_unfold_12_unfold_91;
+          int tmp_5_unfold_12_unfold_91;
+          L1_unfolding_4_loop_unfolding_21_loop:
+          j_unfold_105 = gen_nondet(76);
+          tmp_2_unfold_12_unfold_91 = gen_nondet(77);
+          if (tmp_2_unfold_12_unfold_91 > 10) i_unfold_105 = 10;
+          else i_unfold_105 = 0;
+          Frama_C_show_each_i_(i_unfold_105);
+          tmp_3_unfold_12_unfold_91 = gen_nondet(79);
+          if (tmp_3_unfold_12_unfold_91) goto L_unfolding_18_loop;
+          tmp_4_unfold_12_unfold_91 = gen_nondet(80);
+          if (tmp_4_unfold_12_unfold_91) goto L0;
+          tmp_5_unfold_12_unfold_91 = gen_nondet(81);
+          if (tmp_5_unfold_12_unfold_91) goto L3;
         }
-        i_unroll_105 ++;
-        unrolling_3_loop_unrolling_22_loop: ;
-        /*@ loop pragma UNROLL "done", 2; */
-        while (i_unroll_105 < 4) {
+        i_unfold_105 ++;
+        unfolding_3_loop_unfolding_22_loop: ;
+        /*@ loop unfold "done", 2; */
+        while (i_unfold_105 < 4) {
           {
-            int tmp_2_unroll_102;
-            int tmp_3_unroll_102;
-            int tmp_4_unroll_102;
-            int tmp_5_unroll_102;
-            L1_unrolling_23_loop: j_unroll_105 = gen_nondet(76);
-            tmp_2_unroll_102 = gen_nondet(77);
-            if (tmp_2_unroll_102 > 10) i_unroll_105 = 10;
-            else i_unroll_105 = 0;
-            Frama_C_show_each_i_(i_unroll_105);
-            tmp_3_unroll_102 = gen_nondet(79);
-            if (tmp_3_unroll_102) goto L_unrolling_18_loop;
-            tmp_4_unroll_102 = gen_nondet(80);
-            if (tmp_4_unroll_102) goto L0;
-            tmp_5_unroll_102 = gen_nondet(81);
-            if (tmp_5_unroll_102) goto L3;
+            int tmp_2_unfold_102;
+            int tmp_3_unfold_102;
+            int tmp_4_unfold_102;
+            int tmp_5_unfold_102;
+            L1_unfolding_23_loop: j_unfold_105 = gen_nondet(76);
+            tmp_2_unfold_102 = gen_nondet(77);
+            if (tmp_2_unfold_102 > 10) i_unfold_105 = 10;
+            else i_unfold_105 = 0;
+            Frama_C_show_each_i_(i_unfold_105);
+            tmp_3_unfold_102 = gen_nondet(79);
+            if (tmp_3_unfold_102) goto L_unfolding_18_loop;
+            tmp_4_unfold_102 = gen_nondet(80);
+            if (tmp_4_unfold_102) goto L0;
+            tmp_5_unfold_102 = gen_nondet(81);
+            if (tmp_5_unfold_102) goto L3;
           }
-          i_unroll_105 ++;
+          i_unfold_105 ++;
         }
-        unrolling_2_loop_unrolling_24_loop: ;
+        unfolding_2_loop_unfolding_24_loop: ;
       }
     }
     n --;
-    if (! (n > 0)) goto unrolling_8_loop;
-    unrolling_17_loop: ;
+    if (! (n > 0)) goto unfolding_8_loop;
+    unfolding_17_loop: ;
     {
-      int tmp_1_unroll_64;
-      tmp_1_unroll_64 = gen_nondet(71);
-      if (tmp_1_unroll_64) goto L1_unrolling_15_loop;
-      L_unrolling_10_loop: x = y;
+      int tmp_1_unfold_64;
+      tmp_1_unfold_64 = gen_nondet(71);
+      if (tmp_1_unfold_64) goto L1_unfolding_15_loop;
+      L_unfolding_10_loop: x = y;
       {
-        int j_unroll_63;
-        int i_unroll_63 = 0;
-        if (! (i_unroll_63 < 4)) goto unrolling_2_loop_unrolling_16_loop;
+        int j_unfold_63;
+        int i_unfold_63 = 0;
+        if (! (i_unfold_63 < 4)) goto unfolding_2_loop_unfolding_16_loop;
         {
-          int tmp_2_unroll_24_unroll_38;
-          int tmp_3_unroll_24_unroll_38;
-          int tmp_4_unroll_24_unroll_38;
-          int tmp_5_unroll_24_unroll_38;
-          L1_unrolling_6_loop_unrolling_11_loop:
-          j_unroll_63 = gen_nondet(76);
-          tmp_2_unroll_24_unroll_38 = gen_nondet(77);
-          if (tmp_2_unroll_24_unroll_38 > 10) i_unroll_63 = 10;
-          else i_unroll_63 = 0;
-          Frama_C_show_each_i_(i_unroll_63);
-          tmp_3_unroll_24_unroll_38 = gen_nondet(79);
-          if (tmp_3_unroll_24_unroll_38) goto L_unrolling_10_loop;
-          tmp_4_unroll_24_unroll_38 = gen_nondet(80);
-          if (tmp_4_unroll_24_unroll_38) goto L0;
-          tmp_5_unroll_24_unroll_38 = gen_nondet(81);
-          if (tmp_5_unroll_24_unroll_38) goto L3;
+          int tmp_2_unfold_24_unfold_38;
+          int tmp_3_unfold_24_unfold_38;
+          int tmp_4_unfold_24_unfold_38;
+          int tmp_5_unfold_24_unfold_38;
+          L1_unfolding_6_loop_unfolding_11_loop:
+          j_unfold_63 = gen_nondet(76);
+          tmp_2_unfold_24_unfold_38 = gen_nondet(77);
+          if (tmp_2_unfold_24_unfold_38 > 10) i_unfold_63 = 10;
+          else i_unfold_63 = 0;
+          Frama_C_show_each_i_(i_unfold_63);
+          tmp_3_unfold_24_unfold_38 = gen_nondet(79);
+          if (tmp_3_unfold_24_unfold_38) goto L_unfolding_10_loop;
+          tmp_4_unfold_24_unfold_38 = gen_nondet(80);
+          if (tmp_4_unfold_24_unfold_38) goto L0;
+          tmp_5_unfold_24_unfold_38 = gen_nondet(81);
+          if (tmp_5_unfold_24_unfold_38) goto L3;
         }
-        i_unroll_63 ++;
-        unrolling_5_loop_unrolling_12_loop: ;
-        if (! (i_unroll_63 < 4)) goto unrolling_2_loop_unrolling_16_loop;
+        i_unfold_63 ++;
+        unfolding_5_loop_unfolding_12_loop: ;
+        if (! (i_unfold_63 < 4)) goto unfolding_2_loop_unfolding_16_loop;
         {
-          int tmp_2_unroll_12_unroll_49;
-          int tmp_3_unroll_12_unroll_49;
-          int tmp_4_unroll_12_unroll_49;
-          int tmp_5_unroll_12_unroll_49;
-          L1_unrolling_4_loop_unrolling_13_loop:
-          j_unroll_63 = gen_nondet(76);
-          tmp_2_unroll_12_unroll_49 = gen_nondet(77);
-          if (tmp_2_unroll_12_unroll_49 > 10) i_unroll_63 = 10;
-          else i_unroll_63 = 0;
-          Frama_C_show_each_i_(i_unroll_63);
-          tmp_3_unroll_12_unroll_49 = gen_nondet(79);
-          if (tmp_3_unroll_12_unroll_49) goto L_unrolling_10_loop;
-          tmp_4_unroll_12_unroll_49 = gen_nondet(80);
-          if (tmp_4_unroll_12_unroll_49) goto L0;
-          tmp_5_unroll_12_unroll_49 = gen_nondet(81);
-          if (tmp_5_unroll_12_unroll_49) goto L3;
+          int tmp_2_unfold_12_unfold_49;
+          int tmp_3_unfold_12_unfold_49;
+          int tmp_4_unfold_12_unfold_49;
+          int tmp_5_unfold_12_unfold_49;
+          L1_unfolding_4_loop_unfolding_13_loop:
+          j_unfold_63 = gen_nondet(76);
+          tmp_2_unfold_12_unfold_49 = gen_nondet(77);
+          if (tmp_2_unfold_12_unfold_49 > 10) i_unfold_63 = 10;
+          else i_unfold_63 = 0;
+          Frama_C_show_each_i_(i_unfold_63);
+          tmp_3_unfold_12_unfold_49 = gen_nondet(79);
+          if (tmp_3_unfold_12_unfold_49) goto L_unfolding_10_loop;
+          tmp_4_unfold_12_unfold_49 = gen_nondet(80);
+          if (tmp_4_unfold_12_unfold_49) goto L0;
+          tmp_5_unfold_12_unfold_49 = gen_nondet(81);
+          if (tmp_5_unfold_12_unfold_49) goto L3;
         }
-        i_unroll_63 ++;
-        unrolling_3_loop_unrolling_14_loop: ;
-        /*@ loop pragma UNROLL "done", 2; */
-        while (i_unroll_63 < 4) {
+        i_unfold_63 ++;
+        unfolding_3_loop_unfolding_14_loop: ;
+        /*@ loop unfold "done", 2; */
+        while (i_unfold_63 < 4) {
           {
-            int tmp_2_unroll_60;
-            int tmp_3_unroll_60;
-            int tmp_4_unroll_60;
-            int tmp_5_unroll_60;
-            L1_unrolling_15_loop: j_unroll_63 = gen_nondet(76);
-            tmp_2_unroll_60 = gen_nondet(77);
-            if (tmp_2_unroll_60 > 10) i_unroll_63 = 10; else i_unroll_63 = 0;
-            Frama_C_show_each_i_(i_unroll_63);
-            tmp_3_unroll_60 = gen_nondet(79);
-            if (tmp_3_unroll_60) goto L_unrolling_10_loop;
-            tmp_4_unroll_60 = gen_nondet(80);
-            if (tmp_4_unroll_60) goto L0;
-            tmp_5_unroll_60 = gen_nondet(81);
-            if (tmp_5_unroll_60) goto L3;
+            int tmp_2_unfold_60;
+            int tmp_3_unfold_60;
+            int tmp_4_unfold_60;
+            int tmp_5_unfold_60;
+            L1_unfolding_15_loop: j_unfold_63 = gen_nondet(76);
+            tmp_2_unfold_60 = gen_nondet(77);
+            if (tmp_2_unfold_60 > 10) i_unfold_63 = 10; else i_unfold_63 = 0;
+            Frama_C_show_each_i_(i_unfold_63);
+            tmp_3_unfold_60 = gen_nondet(79);
+            if (tmp_3_unfold_60) goto L_unfolding_10_loop;
+            tmp_4_unfold_60 = gen_nondet(80);
+            if (tmp_4_unfold_60) goto L0;
+            tmp_5_unfold_60 = gen_nondet(81);
+            if (tmp_5_unfold_60) goto L3;
           }
-          i_unroll_63 ++;
+          i_unfold_63 ++;
         }
-        unrolling_2_loop_unrolling_16_loop: ;
+        unfolding_2_loop_unfolding_16_loop: ;
       }
     }
     n --;
-    if (! (n > 0)) goto unrolling_8_loop;
-    unrolling_9_loop: ;
-    /*@ loop pragma UNROLL "done", 2; */
+    if (! (n > 0)) goto unfolding_8_loop;
+    unfolding_9_loop: ;
+    /*@ loop unfold "done", 2; */
     while (1) {
       {
         int tmp_1;
@@ -337,45 +337,45 @@ void main(void)
         {
           int j;
           int i = 0;
-          if (! (i < 4)) goto unrolling_2_loop;
+          if (! (i < 4)) goto unfolding_2_loop;
           {
-            int tmp_2_unroll_24;
-            int tmp_3_unroll_24;
-            int tmp_4_unroll_24;
-            int tmp_5_unroll_24;
-            L1_unrolling_6_loop: j = gen_nondet(76);
-            tmp_2_unroll_24 = gen_nondet(77);
-            if (tmp_2_unroll_24 > 10) i = 10; else i = 0;
+            int tmp_2_unfold_24;
+            int tmp_3_unfold_24;
+            int tmp_4_unfold_24;
+            int tmp_5_unfold_24;
+            L1_unfolding_6_loop: j = gen_nondet(76);
+            tmp_2_unfold_24 = gen_nondet(77);
+            if (tmp_2_unfold_24 > 10) i = 10; else i = 0;
             Frama_C_show_each_i_(i);
-            tmp_3_unroll_24 = gen_nondet(79);
-            if (tmp_3_unroll_24) goto L;
-            tmp_4_unroll_24 = gen_nondet(80);
-            if (tmp_4_unroll_24) goto L0;
-            tmp_5_unroll_24 = gen_nondet(81);
-            if (tmp_5_unroll_24) goto L3;
+            tmp_3_unfold_24 = gen_nondet(79);
+            if (tmp_3_unfold_24) goto L;
+            tmp_4_unfold_24 = gen_nondet(80);
+            if (tmp_4_unfold_24) goto L0;
+            tmp_5_unfold_24 = gen_nondet(81);
+            if (tmp_5_unfold_24) goto L3;
           }
           i ++;
-          unrolling_5_loop: ;
-          if (! (i < 4)) goto unrolling_2_loop;
+          unfolding_5_loop: ;
+          if (! (i < 4)) goto unfolding_2_loop;
           {
-            int tmp_2_unroll_12;
-            int tmp_3_unroll_12;
-            int tmp_4_unroll_12;
-            int tmp_5_unroll_12;
-            L1_unrolling_4_loop: j = gen_nondet(76);
-            tmp_2_unroll_12 = gen_nondet(77);
-            if (tmp_2_unroll_12 > 10) i = 10; else i = 0;
+            int tmp_2_unfold_12;
+            int tmp_3_unfold_12;
+            int tmp_4_unfold_12;
+            int tmp_5_unfold_12;
+            L1_unfolding_4_loop: j = gen_nondet(76);
+            tmp_2_unfold_12 = gen_nondet(77);
+            if (tmp_2_unfold_12 > 10) i = 10; else i = 0;
             Frama_C_show_each_i_(i);
-            tmp_3_unroll_12 = gen_nondet(79);
-            if (tmp_3_unroll_12) goto L;
-            tmp_4_unroll_12 = gen_nondet(80);
-            if (tmp_4_unroll_12) goto L0;
-            tmp_5_unroll_12 = gen_nondet(81);
-            if (tmp_5_unroll_12) goto L3;
+            tmp_3_unfold_12 = gen_nondet(79);
+            if (tmp_3_unfold_12) goto L;
+            tmp_4_unfold_12 = gen_nondet(80);
+            if (tmp_4_unfold_12) goto L0;
+            tmp_5_unfold_12 = gen_nondet(81);
+            if (tmp_5_unfold_12) goto L3;
           }
           i ++;
-          unrolling_3_loop: ;
-          /*@ loop pragma UNROLL "done", 2; */
+          unfolding_3_loop: ;
+          /*@ loop unfold "done", 2; */
           while (i < 4) {
             {
               int tmp_2;
@@ -395,13 +395,13 @@ void main(void)
             }
             i ++;
           }
-          unrolling_2_loop: ;
+          unfolding_2_loop: ;
         }
       }
       n --;
       if (! (n > 0)) break;
     }
-    unrolling_8_loop: ;
+    unfolding_8_loop: ;
     Frama_C_show_each_y_(y);
     Frama_C_show_each_x_(x);
   }
diff --git a/tests/syntax/oracle/unroll_const.res.oracle b/tests/syntax/oracle/unroll_const.res.oracle
index add94fa163ae3fc3072359d080e92e25b6ebd985..8f17a08e2914d6515a2fb8be09a0528bb8e915bb 100644
--- a/tests/syntax/oracle/unroll_const.res.oracle
+++ b/tests/syntax/oracle/unroll_const.res.oracle
@@ -21,156 +21,154 @@ int volatile c;
 void main(void)
 {
   unsigned int i = (unsigned int)0;
-  if (! c) goto unrolling_2_loop;
+  if (! c) goto unfolding_2_loop;
   i ++;
-  unrolling_6_loop: ;
-  if (! c) goto unrolling_2_loop;
+  unfolding_6_loop: ;
+  if (! c) goto unfolding_2_loop;
   i ++;
-  unrolling_5_loop: ;
-  if (! c) goto unrolling_2_loop;
+  unfolding_5_loop: ;
+  if (! c) goto unfolding_2_loop;
   i ++;
-  unrolling_4_loop: ;
-  if (! c) goto unrolling_2_loop;
+  unfolding_4_loop: ;
+  if (! c) goto unfolding_2_loop;
   i ++;
-  unrolling_3_loop: ;
-  /*@ loop pragma UNROLL sizeof(t) / sizeof(t[0]);
-      loop pragma UNROLL "done", 4;
-  */
+  unfolding_3_loop: ;
+  /*@ loop unfold sizeof(t) / sizeof(t[0]);
+      loop unfold "done", 4; */
   while (c) i ++;
-  unrolling_2_loop: ;
-  if (! c) goto unrolling_8_loop;
+  unfolding_2_loop: ;
+  if (! c) goto unfolding_8_loop;
   i ++;
-  unrolling_20_loop: ;
-  if (! c) goto unrolling_8_loop;
+  unfolding_20_loop: ;
+  if (! c) goto unfolding_8_loop;
   i ++;
-  unrolling_19_loop: ;
-  if (! c) goto unrolling_8_loop;
+  unfolding_19_loop: ;
+  if (! c) goto unfolding_8_loop;
   i ++;
-  unrolling_18_loop: ;
-  if (! c) goto unrolling_8_loop;
+  unfolding_18_loop: ;
+  if (! c) goto unfolding_8_loop;
   i ++;
-  unrolling_17_loop: ;
-  if (! c) goto unrolling_8_loop;
+  unfolding_17_loop: ;
+  if (! c) goto unfolding_8_loop;
   i ++;
-  unrolling_16_loop: ;
-  if (! c) goto unrolling_8_loop;
+  unfolding_16_loop: ;
+  if (! c) goto unfolding_8_loop;
   i ++;
-  unrolling_15_loop: ;
-  if (! c) goto unrolling_8_loop;
+  unfolding_15_loop: ;
+  if (! c) goto unfolding_8_loop;
   i ++;
-  unrolling_14_loop: ;
-  if (! c) goto unrolling_8_loop;
+  unfolding_14_loop: ;
+  if (! c) goto unfolding_8_loop;
   i ++;
-  unrolling_13_loop: ;
-  if (! c) goto unrolling_8_loop;
+  unfolding_13_loop: ;
+  if (! c) goto unfolding_8_loop;
   i ++;
-  unrolling_12_loop: ;
-  if (! c) goto unrolling_8_loop;
+  unfolding_12_loop: ;
+  if (! c) goto unfolding_8_loop;
   i ++;
-  unrolling_11_loop: ;
-  if (! c) goto unrolling_8_loop;
+  unfolding_11_loop: ;
+  if (! c) goto unfolding_8_loop;
   i ++;
-  unrolling_10_loop: ;
-  if (! c) goto unrolling_8_loop;
+  unfolding_10_loop: ;
+  if (! c) goto unfolding_8_loop;
   i ++;
-  unrolling_9_loop: ;
-  /*@ loop pragma UNROLL \offset(&s.v.l);
-      loop pragma UNROLL "done", 12; */
+  unfolding_9_loop: ;
+  /*@ loop unfold \offset(&s.v.l);
+      loop unfold "done", 12; */
   while (c) i ++;
-  unrolling_8_loop: ;
-  if (! c) goto unrolling_22_loop;
+  unfolding_8_loop: ;
+  if (! c) goto unfolding_22_loop;
   i ++;
-  unrolling_27_loop: ;
-  if (! c) goto unrolling_22_loop;
+  unfolding_27_loop: ;
+  if (! c) goto unfolding_22_loop;
   i ++;
-  unrolling_26_loop: ;
-  if (! c) goto unrolling_22_loop;
+  unfolding_26_loop: ;
+  if (! c) goto unfolding_22_loop;
   i ++;
-  unrolling_25_loop: ;
-  if (! c) goto unrolling_22_loop;
+  unfolding_25_loop: ;
+  if (! c) goto unfolding_22_loop;
   i ++;
-  unrolling_24_loop: ;
-  if (! c) goto unrolling_22_loop;
+  unfolding_24_loop: ;
+  if (! c) goto unfolding_22_loop;
   i ++;
-  unrolling_23_loop: ;
-  /*@ loop pragma UNROLL s.i + s.v.l;
-      loop pragma UNROLL "done", 5; */
+  unfolding_23_loop: ;
+  /*@ loop unfold s.i + s.v.l;
+      loop unfold "done", 5; */
   while (c) i ++;
-  unrolling_22_loop: ;
-  if (! c) goto unrolling_29_loop;
+  unfolding_22_loop: ;
+  if (! c) goto unfolding_29_loop;
   i ++;
-  unrolling_33_loop: ;
-  if (! c) goto unrolling_29_loop;
+  unfolding_33_loop: ;
+  if (! c) goto unfolding_29_loop;
   i ++;
-  unrolling_32_loop: ;
-  if (! c) goto unrolling_29_loop;
+  unfolding_32_loop: ;
+  if (! c) goto unfolding_29_loop;
   i ++;
-  unrolling_31_loop: ;
-  if (! c) goto unrolling_29_loop;
+  unfolding_31_loop: ;
+  if (! c) goto unfolding_29_loop;
   i ++;
-  unrolling_30_loop: ;
-  /*@ loop pragma UNROLL \max(t[..]);
-      loop pragma UNROLL "done", 4; */
+  unfolding_30_loop: ;
+  /*@ loop unfold \max(t[..]);
+      loop unfold "done", 4; */
   while (c) i ++;
-  unrolling_29_loop: ;
-  /*@ loop pragma UNROLL \min(t[..]); */
+  unfolding_29_loop: ;
+  /*@ loop unfold \min(t[..]); */
   while (c) i ++;
-  if (! c) goto unrolling_35_loop;
+  if (! c) goto unfolding_35_loop;
   i ++;
-  unrolling_41_loop: ;
-  if (! c) goto unrolling_35_loop;
+  unfolding_41_loop: ;
+  if (! c) goto unfolding_35_loop;
   i ++;
-  unrolling_40_loop: ;
-  if (! c) goto unrolling_35_loop;
+  unfolding_40_loop: ;
+  if (! c) goto unfolding_35_loop;
   i ++;
-  unrolling_39_loop: ;
-  if (! c) goto unrolling_35_loop;
+  unfolding_39_loop: ;
+  if (! c) goto unfolding_35_loop;
   i ++;
-  unrolling_38_loop: ;
-  if (! c) goto unrolling_35_loop;
+  unfolding_38_loop: ;
+  if (! c) goto unfolding_35_loop;
   i ++;
-  unrolling_37_loop: ;
-  if (! c) goto unrolling_35_loop;
+  unfolding_37_loop: ;
+  if (! c) goto unfolding_35_loop;
   i ++;
-  unrolling_36_loop: ;
-  /*@ loop pragma UNROLL \max({1, 1 + s.i});
-      loop pragma UNROLL "done", 6; */
+  unfolding_36_loop: ;
+  /*@ loop unfold \max({1, 1 + s.i});
+      loop unfold "done", 6; */
   while (c) i ++;
-  unrolling_35_loop: ;
-  if (! c) goto unrolling_43_loop;
+  unfolding_35_loop: ;
+  if (! c) goto unfolding_43_loop;
   i ++;
-  unrolling_45_loop: ;
-  if (! c) goto unrolling_43_loop;
+  unfolding_45_loop: ;
+  if (! c) goto unfolding_43_loop;
   i ++;
-  unrolling_44_loop: ;
-  /*@ loop pragma UNROLL \min(t[{1, 3}]) + \max(t[{1, 3}]);
-      loop pragma UNROLL "done", 2;
-  */
+  unfolding_44_loop: ;
+  /*@ loop unfold \min(t[{1, 3}]) + \max(t[{1, 3}]);
+      loop unfold "done", 2; */
   while (c) i ++;
-  unrolling_43_loop: ;
-  if (! c) goto unrolling_47_loop;
+  unfolding_43_loop: ;
+  if (! c) goto unfolding_47_loop;
   i ++;
-  unrolling_53_loop: ;
-  if (! c) goto unrolling_47_loop;
+  unfolding_53_loop: ;
+  if (! c) goto unfolding_47_loop;
   i ++;
-  unrolling_52_loop: ;
-  if (! c) goto unrolling_47_loop;
+  unfolding_52_loop: ;
+  if (! c) goto unfolding_47_loop;
   i ++;
-  unrolling_51_loop: ;
-  if (! c) goto unrolling_47_loop;
+  unfolding_51_loop: ;
+  if (! c) goto unfolding_47_loop;
   i ++;
-  unrolling_50_loop: ;
-  if (! c) goto unrolling_47_loop;
+  unfolding_50_loop: ;
+  if (! c) goto unfolding_47_loop;
   i ++;
-  unrolling_49_loop: ;
-  if (! c) goto unrolling_47_loop;
+  unfolding_49_loop: ;
+  if (! c) goto unfolding_47_loop;
   i ++;
-  unrolling_48_loop: ;
-  /*@ loop pragma UNROLL \min(u[.. 1].i1) * \max(u[.. 1].i1);
-      loop pragma UNROLL "done", 6;
+  unfolding_48_loop: ;
+  /*@ loop unfold \min(u[.. 1].i1) * \max(u[.. 1].i1);
+      loop unfold "done", 6;
   */
   while (c) i ++;
-  unrolling_47_loop: ;
+  unfolding_47_loop: ;
   return;
 }
 
diff --git a/tests/syntax/oracle/unroll_labels.0.res.oracle b/tests/syntax/oracle/unroll_labels.0.res.oracle
index 783cbed13c8bc550ce424f8f44cddbbebf330997..b4bf202e0196a60e2d7f5e338888f790ee8eaa7a 100644
--- a/tests/syntax/oracle/unroll_labels.0.res.oracle
+++ b/tests/syntax/oracle/unroll_labels.0.res.oracle
@@ -23,7 +23,7 @@ void main(void)
   int j = 0;
   {
     int i = 1;
-    if (! (i < 4)) goto unrolling_2_loop;
+    if (! (i < 4)) goto unfolding_2_loop;
     switch (i) {
       case 1: j ++;
       break;
@@ -36,8 +36,8 @@ void main(void)
       default: j = 0;
     }
     i ++;
-    unrolling_6_loop: ;
-    if (! (i < 4)) goto unrolling_2_loop;
+    unfolding_6_loop: ;
+    if (! (i < 4)) goto unfolding_2_loop;
     switch (i) {
       case 1: j ++;
       break;
@@ -50,8 +50,8 @@ void main(void)
       default: j = 0;
     }
     i ++;
-    unrolling_5_loop: ;
-    if (! (i < 4)) goto unrolling_2_loop;
+    unfolding_5_loop: ;
+    if (! (i < 4)) goto unfolding_2_loop;
     switch (i) {
       case 1: j ++;
       break;
@@ -64,8 +64,8 @@ void main(void)
       default: j = 0;
     }
     i ++;
-    unrolling_4_loop: ;
-    if (! (i < 4)) goto unrolling_2_loop;
+    unfolding_4_loop: ;
+    if (! (i < 4)) goto unfolding_2_loop;
     switch (i) {
       case 1: j ++;
       break;
@@ -78,10 +78,10 @@ void main(void)
       default: j = 0;
     }
     i ++;
-    unrolling_3_loop: ;
+    unfolding_3_loop: ;
     /*@ loop invariant \false;
-        loop pragma UNROLL "completely", 4;
-        loop pragma UNROLL "done", 4;
+        loop unfold "completely", 4;
+        loop unfold "done", 4;
     */
     while (i < 4) {
       switch (i) {
@@ -97,63 +97,63 @@ void main(void)
       }
       i ++;
     }
-    unrolling_2_loop: ;
+    unfolding_2_loop: ;
   }
   {
     int x = 0;
     L:
     {
-      if (! (x < 5)) goto unrolling_8_loop;
+      if (! (x < 5)) goto unfolding_8_loop;
       {
-        int y_unroll_32 = 0;
+        int y_unfold_32 = 0;
         x ++;
-        y_unroll_32 ++;
+        y_unfold_32 ++;
       }
-      unrolling_11_loop: ;
-      if (! (x < 5)) goto unrolling_8_loop;
+      unfolding_11_loop: ;
+      if (! (x < 5)) goto unfolding_8_loop;
       {
-        int y_unroll_28 = 0;
+        int y_unfold_28 = 0;
         x ++;
-        y_unroll_28 ++;
+        y_unfold_28 ++;
       }
-      unrolling_10_loop: ;
-      if (! (x < 5)) goto unrolling_8_loop;
+      unfolding_10_loop: ;
+      if (! (x < 5)) goto unfolding_8_loop;
       {
-        int y_unroll_24 = 0;
+        int y_unfold_24 = 0;
         x ++;
-        y_unroll_24 ++;
+        y_unfold_24 ++;
       }
-      unrolling_9_loop: ;
-      /*@ loop pragma UNROLL 3;
-          loop pragma UNROLL "done", 3; */
+      unfolding_9_loop: ;
+      /*@ loop unfold 3;
+          loop unfold "done", 3; */
       while (x < 5) {
         int y = 0;
         x ++;
         y ++;
       }
-      unrolling_8_loop: ;
+      unfolding_8_loop: ;
     }
   }
   j = 0;
-  if (! foo) goto unrolling_18_loop;
+  if (! foo) goto unfolding_18_loop;
   switch (j) {
     case -1: j ++;
     break;
     case 0:
     {
-      if (! (j < 5)) goto unrolling_13_loop_unrolling_48_loop;
+      if (! (j < 5)) goto unfolding_13_loop_unfolding_48_loop;
       j ++;
-      unrolling_16_loop_unrolling_45_loop: ;
-      if (! (j < 5)) goto unrolling_13_loop_unrolling_48_loop;
+      unfolding_16_loop_unfolding_45_loop: ;
+      if (! (j < 5)) goto unfolding_13_loop_unfolding_48_loop;
       j ++;
-      unrolling_15_loop_unrolling_46_loop: ;
-      if (! (j < 5)) goto unrolling_13_loop_unrolling_48_loop;
+      unfolding_15_loop_unfolding_46_loop: ;
+      if (! (j < 5)) goto unfolding_13_loop_unfolding_48_loop;
       j ++;
-      unrolling_14_loop_unrolling_47_loop: ;
-      /*@ loop pragma UNROLL "done", 3;
-          loop pragma UNROLL 3; */
+      unfolding_14_loop_unfolding_47_loop: ;
+      /*@ loop unfold "done", 3;
+          loop unfold 3; */
       while (j < 5) j ++;
-      unrolling_13_loop_unrolling_48_loop: ;
+      unfolding_13_loop_unfolding_48_loop: ;
     }
     break;
     case 5: j = -1;
@@ -161,26 +161,26 @@ void main(void)
     default: ;
     goto return_label;
   }
-  unrolling_44_loop: ;
-  if (! foo) goto unrolling_18_loop;
+  unfolding_44_loop: ;
+  if (! foo) goto unfolding_18_loop;
   switch (j) {
     case -1: j ++;
     break;
     case 0:
     {
-      if (! (j < 5)) goto unrolling_13_loop_unrolling_43_loop;
+      if (! (j < 5)) goto unfolding_13_loop_unfolding_43_loop;
       j ++;
-      unrolling_16_loop_unrolling_40_loop: ;
-      if (! (j < 5)) goto unrolling_13_loop_unrolling_43_loop;
+      unfolding_16_loop_unfolding_40_loop: ;
+      if (! (j < 5)) goto unfolding_13_loop_unfolding_43_loop;
       j ++;
-      unrolling_15_loop_unrolling_41_loop: ;
-      if (! (j < 5)) goto unrolling_13_loop_unrolling_43_loop;
+      unfolding_15_loop_unfolding_41_loop: ;
+      if (! (j < 5)) goto unfolding_13_loop_unfolding_43_loop;
       j ++;
-      unrolling_14_loop_unrolling_42_loop: ;
-      /*@ loop pragma UNROLL "done", 3;
-          loop pragma UNROLL 3; */
+      unfolding_14_loop_unfolding_42_loop: ;
+      /*@ loop unfold "done", 3;
+          loop unfold 3; */
       while (j < 5) j ++;
-      unrolling_13_loop_unrolling_43_loop: ;
+      unfolding_13_loop_unfolding_43_loop: ;
     }
     break;
     case 5: j = -1;
@@ -188,26 +188,26 @@ void main(void)
     default: ;
     goto return_label;
   }
-  unrolling_39_loop: ;
-  if (! foo) goto unrolling_18_loop;
+  unfolding_39_loop: ;
+  if (! foo) goto unfolding_18_loop;
   switch (j) {
     case -1: j ++;
     break;
     case 0:
     {
-      if (! (j < 5)) goto unrolling_13_loop_unrolling_38_loop;
+      if (! (j < 5)) goto unfolding_13_loop_unfolding_38_loop;
       j ++;
-      unrolling_16_loop_unrolling_35_loop: ;
-      if (! (j < 5)) goto unrolling_13_loop_unrolling_38_loop;
+      unfolding_16_loop_unfolding_35_loop: ;
+      if (! (j < 5)) goto unfolding_13_loop_unfolding_38_loop;
       j ++;
-      unrolling_15_loop_unrolling_36_loop: ;
-      if (! (j < 5)) goto unrolling_13_loop_unrolling_38_loop;
+      unfolding_15_loop_unfolding_36_loop: ;
+      if (! (j < 5)) goto unfolding_13_loop_unfolding_38_loop;
       j ++;
-      unrolling_14_loop_unrolling_37_loop: ;
-      /*@ loop pragma UNROLL "done", 3;
-          loop pragma UNROLL 3; */
+      unfolding_14_loop_unfolding_37_loop: ;
+      /*@ loop unfold "done", 3;
+          loop unfold 3; */
       while (j < 5) j ++;
-      unrolling_13_loop_unrolling_38_loop: ;
+      unfolding_13_loop_unfolding_38_loop: ;
     }
     break;
     case 5: j = -1;
@@ -215,26 +215,26 @@ void main(void)
     default: ;
     goto return_label;
   }
-  unrolling_34_loop: ;
-  if (! foo) goto unrolling_18_loop;
+  unfolding_34_loop: ;
+  if (! foo) goto unfolding_18_loop;
   switch (j) {
     case -1: j ++;
     break;
     case 0:
     {
-      if (! (j < 5)) goto unrolling_13_loop_unrolling_33_loop;
+      if (! (j < 5)) goto unfolding_13_loop_unfolding_33_loop;
       j ++;
-      unrolling_16_loop_unrolling_30_loop: ;
-      if (! (j < 5)) goto unrolling_13_loop_unrolling_33_loop;
+      unfolding_16_loop_unfolding_30_loop: ;
+      if (! (j < 5)) goto unfolding_13_loop_unfolding_33_loop;
       j ++;
-      unrolling_15_loop_unrolling_31_loop: ;
-      if (! (j < 5)) goto unrolling_13_loop_unrolling_33_loop;
+      unfolding_15_loop_unfolding_31_loop: ;
+      if (! (j < 5)) goto unfolding_13_loop_unfolding_33_loop;
       j ++;
-      unrolling_14_loop_unrolling_32_loop: ;
-      /*@ loop pragma UNROLL "done", 3;
-          loop pragma UNROLL 3; */
+      unfolding_14_loop_unfolding_32_loop: ;
+      /*@ loop unfold "done", 3;
+          loop unfold 3; */
       while (j < 5) j ++;
-      unrolling_13_loop_unrolling_33_loop: ;
+      unfolding_13_loop_unfolding_33_loop: ;
     }
     break;
     case 5: j = -1;
@@ -242,26 +242,26 @@ void main(void)
     default: ;
     goto return_label;
   }
-  unrolling_29_loop: ;
-  if (! foo) goto unrolling_18_loop;
+  unfolding_29_loop: ;
+  if (! foo) goto unfolding_18_loop;
   switch (j) {
     case -1: j ++;
     break;
     case 0:
     {
-      if (! (j < 5)) goto unrolling_13_loop_unrolling_28_loop;
+      if (! (j < 5)) goto unfolding_13_loop_unfolding_28_loop;
       j ++;
-      unrolling_16_loop_unrolling_25_loop: ;
-      if (! (j < 5)) goto unrolling_13_loop_unrolling_28_loop;
+      unfolding_16_loop_unfolding_25_loop: ;
+      if (! (j < 5)) goto unfolding_13_loop_unfolding_28_loop;
       j ++;
-      unrolling_15_loop_unrolling_26_loop: ;
-      if (! (j < 5)) goto unrolling_13_loop_unrolling_28_loop;
+      unfolding_15_loop_unfolding_26_loop: ;
+      if (! (j < 5)) goto unfolding_13_loop_unfolding_28_loop;
       j ++;
-      unrolling_14_loop_unrolling_27_loop: ;
-      /*@ loop pragma UNROLL "done", 3;
-          loop pragma UNROLL 3; */
+      unfolding_14_loop_unfolding_27_loop: ;
+      /*@ loop unfold "done", 3;
+          loop unfold 3; */
       while (j < 5) j ++;
-      unrolling_13_loop_unrolling_28_loop: ;
+      unfolding_13_loop_unfolding_28_loop: ;
     }
     break;
     case 5: j = -1;
@@ -269,26 +269,26 @@ void main(void)
     default: ;
     goto return_label;
   }
-  unrolling_24_loop: ;
-  if (! foo) goto unrolling_18_loop;
+  unfolding_24_loop: ;
+  if (! foo) goto unfolding_18_loop;
   switch (j) {
     case -1: j ++;
     break;
     case 0:
     {
-      if (! (j < 5)) goto unrolling_13_loop_unrolling_23_loop;
+      if (! (j < 5)) goto unfolding_13_loop_unfolding_23_loop;
       j ++;
-      unrolling_16_loop_unrolling_20_loop: ;
-      if (! (j < 5)) goto unrolling_13_loop_unrolling_23_loop;
+      unfolding_16_loop_unfolding_20_loop: ;
+      if (! (j < 5)) goto unfolding_13_loop_unfolding_23_loop;
       j ++;
-      unrolling_15_loop_unrolling_21_loop: ;
-      if (! (j < 5)) goto unrolling_13_loop_unrolling_23_loop;
+      unfolding_15_loop_unfolding_21_loop: ;
+      if (! (j < 5)) goto unfolding_13_loop_unfolding_23_loop;
       j ++;
-      unrolling_14_loop_unrolling_22_loop: ;
-      /*@ loop pragma UNROLL "done", 3;
-          loop pragma UNROLL 3; */
+      unfolding_14_loop_unfolding_22_loop: ;
+      /*@ loop unfold "done", 3;
+          loop unfold 3; */
       while (j < 5) j ++;
-      unrolling_13_loop_unrolling_23_loop: ;
+      unfolding_13_loop_unfolding_23_loop: ;
     }
     break;
     case 5: j = -1;
@@ -296,28 +296,28 @@ void main(void)
     default: ;
     goto return_label;
   }
-  unrolling_19_loop: ;
-  /*@ loop pragma UNROLL SIX;
-      loop pragma UNROLL "done", 6; */
+  unfolding_19_loop: ;
+  /*@ loop unfold SIX;
+      loop unfold "done", 6; */
   while (foo) 
     switch (j) {
       case -1: j ++;
       break;
       case 0:
       {
-        if (! (j < 5)) goto unrolling_13_loop;
+        if (! (j < 5)) goto unfolding_13_loop;
         j ++;
-        unrolling_16_loop: ;
-        if (! (j < 5)) goto unrolling_13_loop;
+        unfolding_16_loop: ;
+        if (! (j < 5)) goto unfolding_13_loop;
         j ++;
-        unrolling_15_loop: ;
-        if (! (j < 5)) goto unrolling_13_loop;
+        unfolding_15_loop: ;
+        if (! (j < 5)) goto unfolding_13_loop;
         j ++;
-        unrolling_14_loop: ;
-        /*@ loop pragma UNROLL 3;
-            loop pragma UNROLL "done", 3; */
+        unfolding_14_loop: ;
+        /*@ loop unfold 3;
+            loop unfold "done", 3; */
         while (j < 5) j ++;
-        unrolling_13_loop: ;
+        unfolding_13_loop: ;
       }
       break;
       case 5: j = -1;
@@ -325,25 +325,25 @@ void main(void)
       default: ;
       goto return_label;
     }
-  unrolling_18_loop: ;
+  unfolding_18_loop: ;
   if (j == 0) goto zero;
   if (j == 1) goto un;
   goto return_label;
   zero:
   {
-    if (! (j < 5)) goto unrolling_50_loop;
-    un_unrolling_56_loop: j ++;
-    unrolling_55_loop: ;
-    if (! (j < 5)) goto unrolling_50_loop;
-    un_unrolling_54_loop: j ++;
-    unrolling_53_loop: ;
-    if (! (j < 5)) goto unrolling_50_loop;
-    un_unrolling_52_loop: j ++;
-    unrolling_51_loop: ;
-    /*@ loop pragma UNROLL 3;
-        loop pragma UNROLL "done", 3; */
+    if (! (j < 5)) goto unfolding_50_loop;
+    un_unfolding_56_loop: j ++;
+    unfolding_55_loop: ;
+    if (! (j < 5)) goto unfolding_50_loop;
+    un_unfolding_54_loop: j ++;
+    unfolding_53_loop: ;
+    if (! (j < 5)) goto unfolding_50_loop;
+    un_unfolding_52_loop: j ++;
+    unfolding_51_loop: ;
+    /*@ loop unfold 3;
+        loop unfold "done", 3; */
     while (j < 5) un: j ++;
-    unrolling_50_loop: ;
+    unfolding_50_loop: ;
   }
   return_label: return;
 }
@@ -351,34 +351,34 @@ void main(void)
 void main2(void)
 {
   int i = 0;
-  if (! (i < 2)) goto unrolling_58_loop;
+  if (! (i < 2)) goto unfolding_58_loop;
   {
-    int j_unroll_192 = 0;
-    while (j_unroll_192 < 2) {
+    int j_unfold_192 = 0;
+    while (j_unfold_192 < 2) {
       i ++;
-      goto foo_unrolling_62_loop;
+      goto foo_unfolding_62_loop;
       i ++;
-      foo_unrolling_62_loop: ;
-      j_unroll_192 ++;
+      foo_unfolding_62_loop: ;
+      j_unfold_192 ++;
     }
   }
   i ++;
-  unrolling_61_loop: ;
-  if (! (i < 2)) goto unrolling_58_loop;
+  unfolding_61_loop: ;
+  if (! (i < 2)) goto unfolding_58_loop;
   {
-    int j_unroll_184 = 0;
-    while (j_unroll_184 < 2) {
+    int j_unfold_184 = 0;
+    while (j_unfold_184 < 2) {
       i ++;
-      goto foo_unrolling_60_loop;
+      goto foo_unfolding_60_loop;
       i ++;
-      foo_unrolling_60_loop: ;
-      j_unroll_184 ++;
+      foo_unfolding_60_loop: ;
+      j_unfold_184 ++;
     }
   }
   i ++;
-  unrolling_59_loop: ;
-  /*@ loop pragma UNROLL 2;
-      loop pragma UNROLL "done", 2; */
+  unfolding_59_loop: ;
+  /*@ loop unfold 2;
+      loop unfold "done", 2; */
   while (i < 2) {
     {
       int j = 0;
@@ -392,34 +392,34 @@ void main2(void)
     }
     i ++;
   }
-  unrolling_58_loop: ;
+  unfolding_58_loop: ;
   return;
 }
 
 void main2_done(void)
 {
   int i = 0;
-  /*@ loop pragma UNROLL 2;
-      loop pragma UNROLL "done", 2; */
+  /*@ loop unfold 2;
+      loop unfold "done", 2; */
   while (i < 2) {
     {
       int j = 0;
-      if (! (j < 2)) goto unrolling_64_loop;
+      if (! (j < 2)) goto unfolding_64_loop;
       i ++;
-      goto foo_unrolling_68_loop;
+      goto foo_unfolding_68_loop;
       i ++;
-      foo_unrolling_68_loop: ;
+      foo_unfolding_68_loop: ;
       j ++;
-      unrolling_67_loop: ;
-      if (! (j < 2)) goto unrolling_64_loop;
+      unfolding_67_loop: ;
+      if (! (j < 2)) goto unfolding_64_loop;
       i ++;
-      goto foo_unrolling_66_loop;
+      goto foo_unfolding_66_loop;
       i ++;
-      foo_unrolling_66_loop: ;
+      foo_unfolding_66_loop: ;
       j ++;
-      unrolling_65_loop: ;
-      /*@ loop pragma UNROLL 2;
-          loop pragma UNROLL "done", 2; */
+      unfolding_65_loop: ;
+      /*@ loop unfold 2;
+          loop unfold "done", 2; */
       while (j < 2) {
         i ++;
         goto foo;
@@ -427,7 +427,7 @@ void main2_done(void)
         foo: ;
         j ++;
       }
-      unrolling_64_loop: ;
+      unfolding_64_loop: ;
     }
     i ++;
   }
@@ -438,46 +438,46 @@ void main3(int c)
 {
   int i = 0;
   if (c == 0) goto foo;
-  if (! (i < 5)) goto unrolling_70_loop;
+  if (! (i < 5)) goto unfolding_70_loop;
   {
-    int j_unroll_244 = 0;
-    if (i == j_unroll_244) goto foo_unrolling_77_loop;
-    if (i == 1) goto unrolling_70_loop;
-    if (i == 2) goto __Cont_unrolling_80_loop;
-    while (j_unroll_244 < 5) {
-      if (i == j_unroll_244) break;
-      if (i < j_unroll_244) goto foo_unrolling_77_loop;
-      if (i == j_unroll_244 + 1) goto __Cont_0_unrolling_78_loop;
-      if (i == j_unroll_244 + 2) goto up_unrolling_79_loop;
+    int j_unfold_244 = 0;
+    if (i == j_unfold_244) goto foo_unfolding_77_loop;
+    if (i == 1) goto unfolding_70_loop;
+    if (i == 2) goto __Cont_unfolding_80_loop;
+    while (j_unfold_244 < 5) {
+      if (i == j_unfold_244) break;
+      if (i < j_unfold_244) goto foo_unfolding_77_loop;
+      if (i == j_unfold_244 + 1) goto __Cont_0_unfolding_78_loop;
+      if (i == j_unfold_244 + 2) goto up_unfolding_79_loop;
       i ++;
-      foo_unrolling_77_loop: i ++;
-      __Cont_0_unrolling_78_loop: j_unroll_244 ++;
+      foo_unfolding_77_loop: i ++;
+      __Cont_0_unfolding_78_loop: j_unfold_244 ++;
     }
-    up_unrolling_79_loop: ;
+    up_unfolding_79_loop: ;
   }
-  __Cont_unrolling_80_loop: i ++;
-  unrolling_76_loop: ;
-  if (! (i < 5)) goto unrolling_70_loop;
+  __Cont_unfolding_80_loop: i ++;
+  unfolding_76_loop: ;
+  if (! (i < 5)) goto unfolding_70_loop;
   {
-    int j_unroll_222 = 0;
-    if (i == j_unroll_222) goto foo_unrolling_72_loop;
-    if (i == 1) goto unrolling_70_loop;
-    if (i == 2) goto __Cont_unrolling_75_loop;
-    while (j_unroll_222 < 5) {
-      if (i == j_unroll_222) break;
-      if (i < j_unroll_222) goto foo_unrolling_72_loop;
-      if (i == j_unroll_222 + 1) goto __Cont_0_unrolling_73_loop;
-      if (i == j_unroll_222 + 2) goto up_unrolling_74_loop;
+    int j_unfold_222 = 0;
+    if (i == j_unfold_222) goto foo_unfolding_72_loop;
+    if (i == 1) goto unfolding_70_loop;
+    if (i == 2) goto __Cont_unfolding_75_loop;
+    while (j_unfold_222 < 5) {
+      if (i == j_unfold_222) break;
+      if (i < j_unfold_222) goto foo_unfolding_72_loop;
+      if (i == j_unfold_222 + 1) goto __Cont_0_unfolding_73_loop;
+      if (i == j_unfold_222 + 2) goto up_unfolding_74_loop;
       i ++;
-      foo_unrolling_72_loop: i ++;
-      __Cont_0_unrolling_73_loop: j_unroll_222 ++;
+      foo_unfolding_72_loop: i ++;
+      __Cont_0_unfolding_73_loop: j_unfold_222 ++;
     }
-    up_unrolling_74_loop: ;
+    up_unfolding_74_loop: ;
   }
-  __Cont_unrolling_75_loop: i ++;
-  unrolling_71_loop: ;
-  /*@ loop pragma UNROLL 2;
-      loop pragma UNROLL "done", 2; */
+  __Cont_unfolding_75_loop: i ++;
+  unfolding_71_loop: ;
+  /*@ loop unfold 2;
+      loop unfold "done", 2; */
   while (i < 5) {
     {
       int j = 0;
@@ -497,7 +497,7 @@ void main3(int c)
     }
     __Cont: i ++;
   }
-  unrolling_70_loop: ;
+  unfolding_70_loop: ;
   return;
 }
 
diff --git a/tests/syntax/oracle/unroll_labels.1.res.oracle b/tests/syntax/oracle/unroll_labels.1.res.oracle
index 0c625a01ef43c99e768623b0906f85096315b8e6..8a9d1c82f7aae87f25994c943465209eb2d93be7 100644
--- a/tests/syntax/oracle/unroll_labels.1.res.oracle
+++ b/tests/syntax/oracle/unroll_labels.1.res.oracle
@@ -19,7 +19,7 @@ void main(void)
   int j = 0;
   {
     int i = 1;
-    if (! (i < 4)) goto unrolling_2_loop;
+    if (! (i < 4)) goto unfolding_2_loop;
     switch (i) {
       case 1: j ++;
       break;
@@ -32,8 +32,8 @@ void main(void)
       default: j = 0;
     }
     i ++;
-    unrolling_6_loop: ;
-    if (! (i < 4)) goto unrolling_2_loop;
+    unfolding_6_loop: ;
+    if (! (i < 4)) goto unfolding_2_loop;
     switch (i) {
       case 1: j ++;
       break;
@@ -46,8 +46,8 @@ void main(void)
       default: j = 0;
     }
     i ++;
-    unrolling_5_loop: ;
-    if (! (i < 4)) goto unrolling_2_loop;
+    unfolding_5_loop: ;
+    if (! (i < 4)) goto unfolding_2_loop;
     switch (i) {
       case 1: j ++;
       break;
@@ -60,8 +60,8 @@ void main(void)
       default: j = 0;
     }
     i ++;
-    unrolling_4_loop: ;
-    if (! (i < 4)) goto unrolling_2_loop;
+    unfolding_4_loop: ;
+    if (! (i < 4)) goto unfolding_2_loop;
     switch (i) {
       case 1: j ++;
       break;
@@ -74,10 +74,10 @@ void main(void)
       default: j = 0;
     }
     i ++;
-    unrolling_3_loop: ;
+    unfolding_3_loop: ;
     /*@ loop invariant \false;
-        loop pragma UNROLL "completely", 4;
-        loop pragma UNROLL "done", 4;
+        loop unfold "completely", 4;
+        loop unfold "done", 4;
     */
     while (i < 4) {
       switch (i) {
@@ -93,63 +93,63 @@ void main(void)
       }
       i ++;
     }
-    unrolling_2_loop: ;
+    unfolding_2_loop: ;
   }
   {
     int x = 0;
     L:
     {
-      if (! (x < 5)) goto unrolling_8_loop;
+      if (! (x < 5)) goto unfolding_8_loop;
       {
-        int y_unroll_32 = 0;
+        int y_unfold_32 = 0;
         x ++;
-        y_unroll_32 ++;
+        y_unfold_32 ++;
       }
-      unrolling_11_loop: ;
-      if (! (x < 5)) goto unrolling_8_loop;
+      unfolding_11_loop: ;
+      if (! (x < 5)) goto unfolding_8_loop;
       {
-        int y_unroll_28 = 0;
+        int y_unfold_28 = 0;
         x ++;
-        y_unroll_28 ++;
+        y_unfold_28 ++;
       }
-      unrolling_10_loop: ;
-      if (! (x < 5)) goto unrolling_8_loop;
+      unfolding_10_loop: ;
+      if (! (x < 5)) goto unfolding_8_loop;
       {
-        int y_unroll_24 = 0;
+        int y_unfold_24 = 0;
         x ++;
-        y_unroll_24 ++;
+        y_unfold_24 ++;
       }
-      unrolling_9_loop: ;
-      /*@ loop pragma UNROLL 3;
-          loop pragma UNROLL "done", 3; */
+      unfolding_9_loop: ;
+      /*@ loop unfold 3;
+          loop unfold "done", 3; */
       while (x < 5) {
         int y = 0;
         x ++;
         y ++;
       }
-      unrolling_8_loop: ;
+      unfolding_8_loop: ;
     }
   }
   j = 0;
-  if (! foo) goto unrolling_18_loop;
+  if (! foo) goto unfolding_18_loop;
   switch (j) {
     case -1: j ++;
     break;
     case 0:
     {
-      if (! (j < 5)) goto unrolling_13_loop_unrolling_48_loop;
+      if (! (j < 5)) goto unfolding_13_loop_unfolding_48_loop;
       j ++;
-      unrolling_16_loop_unrolling_45_loop: ;
-      if (! (j < 5)) goto unrolling_13_loop_unrolling_48_loop;
+      unfolding_16_loop_unfolding_45_loop: ;
+      if (! (j < 5)) goto unfolding_13_loop_unfolding_48_loop;
       j ++;
-      unrolling_15_loop_unrolling_46_loop: ;
-      if (! (j < 5)) goto unrolling_13_loop_unrolling_48_loop;
+      unfolding_15_loop_unfolding_46_loop: ;
+      if (! (j < 5)) goto unfolding_13_loop_unfolding_48_loop;
       j ++;
-      unrolling_14_loop_unrolling_47_loop: ;
-      /*@ loop pragma UNROLL "done", 3;
-          loop pragma UNROLL 3; */
+      unfolding_14_loop_unfolding_47_loop: ;
+      /*@ loop unfold "done", 3;
+          loop unfold 3; */
       while (j < 5) j ++;
-      unrolling_13_loop_unrolling_48_loop: ;
+      unfolding_13_loop_unfolding_48_loop: ;
     }
     break;
     case 5: j = -1;
@@ -157,26 +157,26 @@ void main(void)
     default: ;
     goto return_label;
   }
-  unrolling_44_loop: ;
-  if (! foo) goto unrolling_18_loop;
+  unfolding_44_loop: ;
+  if (! foo) goto unfolding_18_loop;
   switch (j) {
     case -1: j ++;
     break;
     case 0:
     {
-      if (! (j < 5)) goto unrolling_13_loop_unrolling_43_loop;
+      if (! (j < 5)) goto unfolding_13_loop_unfolding_43_loop;
       j ++;
-      unrolling_16_loop_unrolling_40_loop: ;
-      if (! (j < 5)) goto unrolling_13_loop_unrolling_43_loop;
+      unfolding_16_loop_unfolding_40_loop: ;
+      if (! (j < 5)) goto unfolding_13_loop_unfolding_43_loop;
       j ++;
-      unrolling_15_loop_unrolling_41_loop: ;
-      if (! (j < 5)) goto unrolling_13_loop_unrolling_43_loop;
+      unfolding_15_loop_unfolding_41_loop: ;
+      if (! (j < 5)) goto unfolding_13_loop_unfolding_43_loop;
       j ++;
-      unrolling_14_loop_unrolling_42_loop: ;
-      /*@ loop pragma UNROLL "done", 3;
-          loop pragma UNROLL 3; */
+      unfolding_14_loop_unfolding_42_loop: ;
+      /*@ loop unfold "done", 3;
+          loop unfold 3; */
       while (j < 5) j ++;
-      unrolling_13_loop_unrolling_43_loop: ;
+      unfolding_13_loop_unfolding_43_loop: ;
     }
     break;
     case 5: j = -1;
@@ -184,26 +184,26 @@ void main(void)
     default: ;
     goto return_label;
   }
-  unrolling_39_loop: ;
-  if (! foo) goto unrolling_18_loop;
+  unfolding_39_loop: ;
+  if (! foo) goto unfolding_18_loop;
   switch (j) {
     case -1: j ++;
     break;
     case 0:
     {
-      if (! (j < 5)) goto unrolling_13_loop_unrolling_38_loop;
+      if (! (j < 5)) goto unfolding_13_loop_unfolding_38_loop;
       j ++;
-      unrolling_16_loop_unrolling_35_loop: ;
-      if (! (j < 5)) goto unrolling_13_loop_unrolling_38_loop;
+      unfolding_16_loop_unfolding_35_loop: ;
+      if (! (j < 5)) goto unfolding_13_loop_unfolding_38_loop;
       j ++;
-      unrolling_15_loop_unrolling_36_loop: ;
-      if (! (j < 5)) goto unrolling_13_loop_unrolling_38_loop;
+      unfolding_15_loop_unfolding_36_loop: ;
+      if (! (j < 5)) goto unfolding_13_loop_unfolding_38_loop;
       j ++;
-      unrolling_14_loop_unrolling_37_loop: ;
-      /*@ loop pragma UNROLL "done", 3;
-          loop pragma UNROLL 3; */
+      unfolding_14_loop_unfolding_37_loop: ;
+      /*@ loop unfold "done", 3;
+          loop unfold 3; */
       while (j < 5) j ++;
-      unrolling_13_loop_unrolling_38_loop: ;
+      unfolding_13_loop_unfolding_38_loop: ;
     }
     break;
     case 5: j = -1;
@@ -211,26 +211,26 @@ void main(void)
     default: ;
     goto return_label;
   }
-  unrolling_34_loop: ;
-  if (! foo) goto unrolling_18_loop;
+  unfolding_34_loop: ;
+  if (! foo) goto unfolding_18_loop;
   switch (j) {
     case -1: j ++;
     break;
     case 0:
     {
-      if (! (j < 5)) goto unrolling_13_loop_unrolling_33_loop;
+      if (! (j < 5)) goto unfolding_13_loop_unfolding_33_loop;
       j ++;
-      unrolling_16_loop_unrolling_30_loop: ;
-      if (! (j < 5)) goto unrolling_13_loop_unrolling_33_loop;
+      unfolding_16_loop_unfolding_30_loop: ;
+      if (! (j < 5)) goto unfolding_13_loop_unfolding_33_loop;
       j ++;
-      unrolling_15_loop_unrolling_31_loop: ;
-      if (! (j < 5)) goto unrolling_13_loop_unrolling_33_loop;
+      unfolding_15_loop_unfolding_31_loop: ;
+      if (! (j < 5)) goto unfolding_13_loop_unfolding_33_loop;
       j ++;
-      unrolling_14_loop_unrolling_32_loop: ;
-      /*@ loop pragma UNROLL "done", 3;
-          loop pragma UNROLL 3; */
+      unfolding_14_loop_unfolding_32_loop: ;
+      /*@ loop unfold "done", 3;
+          loop unfold 3; */
       while (j < 5) j ++;
-      unrolling_13_loop_unrolling_33_loop: ;
+      unfolding_13_loop_unfolding_33_loop: ;
     }
     break;
     case 5: j = -1;
@@ -238,26 +238,26 @@ void main(void)
     default: ;
     goto return_label;
   }
-  unrolling_29_loop: ;
-  if (! foo) goto unrolling_18_loop;
+  unfolding_29_loop: ;
+  if (! foo) goto unfolding_18_loop;
   switch (j) {
     case -1: j ++;
     break;
     case 0:
     {
-      if (! (j < 5)) goto unrolling_13_loop_unrolling_28_loop;
+      if (! (j < 5)) goto unfolding_13_loop_unfolding_28_loop;
       j ++;
-      unrolling_16_loop_unrolling_25_loop: ;
-      if (! (j < 5)) goto unrolling_13_loop_unrolling_28_loop;
+      unfolding_16_loop_unfolding_25_loop: ;
+      if (! (j < 5)) goto unfolding_13_loop_unfolding_28_loop;
       j ++;
-      unrolling_15_loop_unrolling_26_loop: ;
-      if (! (j < 5)) goto unrolling_13_loop_unrolling_28_loop;
+      unfolding_15_loop_unfolding_26_loop: ;
+      if (! (j < 5)) goto unfolding_13_loop_unfolding_28_loop;
       j ++;
-      unrolling_14_loop_unrolling_27_loop: ;
-      /*@ loop pragma UNROLL "done", 3;
-          loop pragma UNROLL 3; */
+      unfolding_14_loop_unfolding_27_loop: ;
+      /*@ loop unfold "done", 3;
+          loop unfold 3; */
       while (j < 5) j ++;
-      unrolling_13_loop_unrolling_28_loop: ;
+      unfolding_13_loop_unfolding_28_loop: ;
     }
     break;
     case 5: j = -1;
@@ -265,26 +265,26 @@ void main(void)
     default: ;
     goto return_label;
   }
-  unrolling_24_loop: ;
-  if (! foo) goto unrolling_18_loop;
+  unfolding_24_loop: ;
+  if (! foo) goto unfolding_18_loop;
   switch (j) {
     case -1: j ++;
     break;
     case 0:
     {
-      if (! (j < 5)) goto unrolling_13_loop_unrolling_23_loop;
+      if (! (j < 5)) goto unfolding_13_loop_unfolding_23_loop;
       j ++;
-      unrolling_16_loop_unrolling_20_loop: ;
-      if (! (j < 5)) goto unrolling_13_loop_unrolling_23_loop;
+      unfolding_16_loop_unfolding_20_loop: ;
+      if (! (j < 5)) goto unfolding_13_loop_unfolding_23_loop;
       j ++;
-      unrolling_15_loop_unrolling_21_loop: ;
-      if (! (j < 5)) goto unrolling_13_loop_unrolling_23_loop;
+      unfolding_15_loop_unfolding_21_loop: ;
+      if (! (j < 5)) goto unfolding_13_loop_unfolding_23_loop;
       j ++;
-      unrolling_14_loop_unrolling_22_loop: ;
-      /*@ loop pragma UNROLL "done", 3;
-          loop pragma UNROLL 3; */
+      unfolding_14_loop_unfolding_22_loop: ;
+      /*@ loop unfold "done", 3;
+          loop unfold 3; */
       while (j < 5) j ++;
-      unrolling_13_loop_unrolling_23_loop: ;
+      unfolding_13_loop_unfolding_23_loop: ;
     }
     break;
     case 5: j = -1;
@@ -292,28 +292,28 @@ void main(void)
     default: ;
     goto return_label;
   }
-  unrolling_19_loop: ;
-  /*@ loop pragma UNROLL SIX;
-      loop pragma UNROLL "done", 6; */
+  unfolding_19_loop: ;
+  /*@ loop unfold SIX;
+      loop unfold "done", 6; */
   while (foo) 
     switch (j) {
       case -1: j ++;
       break;
       case 0:
       {
-        if (! (j < 5)) goto unrolling_13_loop;
+        if (! (j < 5)) goto unfolding_13_loop;
         j ++;
-        unrolling_16_loop: ;
-        if (! (j < 5)) goto unrolling_13_loop;
+        unfolding_16_loop: ;
+        if (! (j < 5)) goto unfolding_13_loop;
         j ++;
-        unrolling_15_loop: ;
-        if (! (j < 5)) goto unrolling_13_loop;
+        unfolding_15_loop: ;
+        if (! (j < 5)) goto unfolding_13_loop;
         j ++;
-        unrolling_14_loop: ;
-        /*@ loop pragma UNROLL 3;
-            loop pragma UNROLL "done", 3; */
+        unfolding_14_loop: ;
+        /*@ loop unfold 3;
+            loop unfold "done", 3; */
         while (j < 5) j ++;
-        unrolling_13_loop: ;
+        unfolding_13_loop: ;
       }
       break;
       case 5: j = -1;
@@ -321,25 +321,25 @@ void main(void)
       default: ;
       goto return_label;
     }
-  unrolling_18_loop: ;
+  unfolding_18_loop: ;
   if (j == 0) goto zero;
   if (j == 1) goto un;
   goto return_label;
   zero:
   {
-    if (! (j < 5)) goto unrolling_50_loop;
-    un_unrolling_56_loop: j ++;
-    unrolling_55_loop: ;
-    if (! (j < 5)) goto unrolling_50_loop;
-    un_unrolling_54_loop: j ++;
-    unrolling_53_loop: ;
-    if (! (j < 5)) goto unrolling_50_loop;
-    un_unrolling_52_loop: j ++;
-    unrolling_51_loop: ;
-    /*@ loop pragma UNROLL 3;
-        loop pragma UNROLL "done", 3; */
+    if (! (j < 5)) goto unfolding_50_loop;
+    un_unfolding_56_loop: j ++;
+    unfolding_55_loop: ;
+    if (! (j < 5)) goto unfolding_50_loop;
+    un_unfolding_54_loop: j ++;
+    unfolding_53_loop: ;
+    if (! (j < 5)) goto unfolding_50_loop;
+    un_unfolding_52_loop: j ++;
+    unfolding_51_loop: ;
+    /*@ loop unfold 3;
+        loop unfold "done", 3; */
     while (j < 5) un: j ++;
-    unrolling_50_loop: ;
+    unfolding_50_loop: ;
   }
   return_label: return;
 }
@@ -347,34 +347,34 @@ void main(void)
 void main2(void)
 {
   int i = 0;
-  if (! (i < 2)) goto unrolling_58_loop;
+  if (! (i < 2)) goto unfolding_58_loop;
   {
-    int j_unroll_192 = 0;
-    while (j_unroll_192 < 2) {
+    int j_unfold_192 = 0;
+    while (j_unfold_192 < 2) {
       i ++;
-      goto foo_unrolling_62_loop;
+      goto foo_unfolding_62_loop;
       i ++;
-      foo_unrolling_62_loop: ;
-      j_unroll_192 ++;
+      foo_unfolding_62_loop: ;
+      j_unfold_192 ++;
     }
   }
   i ++;
-  unrolling_61_loop: ;
-  if (! (i < 2)) goto unrolling_58_loop;
+  unfolding_61_loop: ;
+  if (! (i < 2)) goto unfolding_58_loop;
   {
-    int j_unroll_184 = 0;
-    while (j_unroll_184 < 2) {
+    int j_unfold_184 = 0;
+    while (j_unfold_184 < 2) {
       i ++;
-      goto foo_unrolling_60_loop;
+      goto foo_unfolding_60_loop;
       i ++;
-      foo_unrolling_60_loop: ;
-      j_unroll_184 ++;
+      foo_unfolding_60_loop: ;
+      j_unfold_184 ++;
     }
   }
   i ++;
-  unrolling_59_loop: ;
-  /*@ loop pragma UNROLL 2;
-      loop pragma UNROLL "done", 2; */
+  unfolding_59_loop: ;
+  /*@ loop unfold 2;
+      loop unfold "done", 2; */
   while (i < 2) {
     {
       int j = 0;
@@ -388,34 +388,34 @@ void main2(void)
     }
     i ++;
   }
-  unrolling_58_loop: ;
+  unfolding_58_loop: ;
   return;
 }
 
 void main2_done(void)
 {
   int i = 0;
-  /*@ loop pragma UNROLL 2;
-      loop pragma UNROLL "done", 2; */
+  /*@ loop unfold 2;
+      loop unfold "done", 2; */
   while (i < 2) {
     {
       int j = 0;
-      if (! (j < 2)) goto unrolling_64_loop;
+      if (! (j < 2)) goto unfolding_64_loop;
       i ++;
-      goto foo_unrolling_68_loop;
+      goto foo_unfolding_68_loop;
       i ++;
-      foo_unrolling_68_loop: ;
+      foo_unfolding_68_loop: ;
       j ++;
-      unrolling_67_loop: ;
-      if (! (j < 2)) goto unrolling_64_loop;
+      unfolding_67_loop: ;
+      if (! (j < 2)) goto unfolding_64_loop;
       i ++;
-      goto foo_unrolling_66_loop;
+      goto foo_unfolding_66_loop;
       i ++;
-      foo_unrolling_66_loop: ;
+      foo_unfolding_66_loop: ;
       j ++;
-      unrolling_65_loop: ;
-      /*@ loop pragma UNROLL 2;
-          loop pragma UNROLL "done", 2; */
+      unfolding_65_loop: ;
+      /*@ loop unfold 2;
+          loop unfold "done", 2; */
       while (j < 2) {
         i ++;
         goto foo;
@@ -423,7 +423,7 @@ void main2_done(void)
         foo: ;
         j ++;
       }
-      unrolling_64_loop: ;
+      unfolding_64_loop: ;
     }
     i ++;
   }
@@ -434,46 +434,46 @@ void main3(int c)
 {
   int i = 0;
   if (c == 0) goto foo;
-  if (! (i < 5)) goto unrolling_70_loop;
+  if (! (i < 5)) goto unfolding_70_loop;
   {
-    int j_unroll_244 = 0;
-    if (i == j_unroll_244) goto foo_unrolling_77_loop;
-    if (i == 1) goto unrolling_70_loop;
-    if (i == 2) goto __Cont_unrolling_80_loop;
-    while (j_unroll_244 < 5) {
-      if (i == j_unroll_244) break;
-      if (i < j_unroll_244) goto foo_unrolling_77_loop;
-      if (i == j_unroll_244 + 1) goto __Cont_0_unrolling_78_loop;
-      if (i == j_unroll_244 + 2) goto up_unrolling_79_loop;
+    int j_unfold_244 = 0;
+    if (i == j_unfold_244) goto foo_unfolding_77_loop;
+    if (i == 1) goto unfolding_70_loop;
+    if (i == 2) goto __Cont_unfolding_80_loop;
+    while (j_unfold_244 < 5) {
+      if (i == j_unfold_244) break;
+      if (i < j_unfold_244) goto foo_unfolding_77_loop;
+      if (i == j_unfold_244 + 1) goto __Cont_0_unfolding_78_loop;
+      if (i == j_unfold_244 + 2) goto up_unfolding_79_loop;
       i ++;
-      foo_unrolling_77_loop: i ++;
-      __Cont_0_unrolling_78_loop: j_unroll_244 ++;
+      foo_unfolding_77_loop: i ++;
+      __Cont_0_unfolding_78_loop: j_unfold_244 ++;
     }
-    up_unrolling_79_loop: ;
+    up_unfolding_79_loop: ;
   }
-  __Cont_unrolling_80_loop: i ++;
-  unrolling_76_loop: ;
-  if (! (i < 5)) goto unrolling_70_loop;
+  __Cont_unfolding_80_loop: i ++;
+  unfolding_76_loop: ;
+  if (! (i < 5)) goto unfolding_70_loop;
   {
-    int j_unroll_222 = 0;
-    if (i == j_unroll_222) goto foo_unrolling_72_loop;
-    if (i == 1) goto unrolling_70_loop;
-    if (i == 2) goto __Cont_unrolling_75_loop;
-    while (j_unroll_222 < 5) {
-      if (i == j_unroll_222) break;
-      if (i < j_unroll_222) goto foo_unrolling_72_loop;
-      if (i == j_unroll_222 + 1) goto __Cont_0_unrolling_73_loop;
-      if (i == j_unroll_222 + 2) goto up_unrolling_74_loop;
+    int j_unfold_222 = 0;
+    if (i == j_unfold_222) goto foo_unfolding_72_loop;
+    if (i == 1) goto unfolding_70_loop;
+    if (i == 2) goto __Cont_unfolding_75_loop;
+    while (j_unfold_222 < 5) {
+      if (i == j_unfold_222) break;
+      if (i < j_unfold_222) goto foo_unfolding_72_loop;
+      if (i == j_unfold_222 + 1) goto __Cont_0_unfolding_73_loop;
+      if (i == j_unfold_222 + 2) goto up_unfolding_74_loop;
       i ++;
-      foo_unrolling_72_loop: i ++;
-      __Cont_0_unrolling_73_loop: j_unroll_222 ++;
+      foo_unfolding_72_loop: i ++;
+      __Cont_0_unfolding_73_loop: j_unfold_222 ++;
     }
-    up_unrolling_74_loop: ;
+    up_unfolding_74_loop: ;
   }
-  __Cont_unrolling_75_loop: i ++;
-  unrolling_71_loop: ;
-  /*@ loop pragma UNROLL 2;
-      loop pragma UNROLL "done", 2; */
+  __Cont_unfolding_75_loop: i ++;
+  unfolding_71_loop: ;
+  /*@ loop unfold 2;
+      loop unfold "done", 2; */
   while (i < 5) {
     {
       int j = 0;
@@ -493,7 +493,7 @@ void main3(int c)
     }
     __Cont: i ++;
   }
-  unrolling_70_loop: ;
+  unfolding_70_loop: ;
   return;
 }
 
diff --git a/tests/syntax/oracle/unroll_visit.res.oracle b/tests/syntax/oracle/unroll_visit.res.oracle
index c65c2723ab53a495d5f822b511d9741d8e1fcb5f..4768a2906b4d130538dab116a8c659800c461649 100644
--- a/tests/syntax/oracle/unroll_visit.res.oracle
+++ b/tests/syntax/oracle/unroll_visit.res.oracle
@@ -27,27 +27,27 @@ typedef char i8;
 void main(void)
 {
   i8 i = (i8)0;
-  if (! ((int)i < 100)) goto unrolling_2_loop;
+  if (! ((int)i < 100)) goto unfolding_2_loop;
   i = (i8)((int)i - 1);
   /*@ assert i < 100; */ ;
   i = (i8)((int)i + 1);
   i = (i8)((int)i + 1);
-  unrolling_4_loop: ;
-  if (! ((int)i < 100)) goto unrolling_2_loop;
+  unfolding_4_loop: ;
+  if (! ((int)i < 100)) goto unfolding_2_loop;
   i = (i8)((int)i - 1);
   /*@ assert i < 100; */ ;
   i = (i8)((int)i + 1);
   i = (i8)((int)i + 1);
-  unrolling_3_loop: ;
-  /*@ loop pragma UNROLL 2;
-      loop pragma UNROLL "done", 2; */
+  unfolding_3_loop: ;
+  /*@ loop unfold 2;
+      loop unfold "done", 2; */
   while ((int)i < 100) {
     i = (i8)((int)i - 1);
     /*@ assert i < 100; */ ;
     i = (i8)((int)i + 1);
     i = (i8)((int)i + 1);
   }
-  unrolling_2_loop: ;
+  unfolding_2_loop: ;
   return;
 }
 
diff --git a/tests/syntax/oracle/very_large_integers.17.res.oracle b/tests/syntax/oracle/very_large_integers.17.res.oracle
index 3358d5f03d550e6db60ecd6b91ac10cfbcfe4eca..952d0b178160cf63405a6d5e13e63727487b832c 100644
--- a/tests/syntax/oracle/very_large_integers.17.res.oracle
+++ b/tests/syntax/oracle/very_large_integers.17.res.oracle
@@ -5,7 +5,7 @@
   ignoring invalid aligned attribute: __aligned__((9223372036854775808)+
                                                    (9223372036854775808) )
 [kernel] very_large_integers.c:141: Warning: 
-  ignoring unrolling directive (not an understood constant expression)
+  ignoring unfolding directive (not an understood constant expression)
 /* Generated by Frama-C */
 int volatile nondet;
 /*@ logic ℤ too_large_integer= 9999999999999999999;
@@ -13,7 +13,7 @@ int volatile nondet;
 int main(void)
 {
   int __retres;
-  /*@ loop pragma UNROLL 99999999999999999999; */
+  /*@ loop unfold 99999999999999999999; */
   while (nondet) ;
   __retres = 0;
   return __retres;
diff --git a/tests/syntax/unroll_const.i b/tests/syntax/unroll_const.i
index 715210a9bf3d1b178a0f9cdf214251984047532b..46e21c26fe2f8b975c530dad74f24558b2b1aaaa 100644
--- a/tests/syntax/unroll_const.i
+++ b/tests/syntax/unroll_const.i
@@ -17,44 +17,44 @@ volatile int c;
 void main() {
   unsigned int i = 0;
 
-  //@ loop pragma UNROLL sizeof(t)/sizeof(t[0]); // 4
+  //@ loop unfold sizeof(t)/sizeof(t[0]); // 4
   while (c) {
     i++;
   }
 
-  //@ loop pragma UNROLL \offset(&s.v.l); // 12
+  //@ loop unfold \offset(&s.v.l); // 12
   while (c) {
     i++;
   }
 
-  //@ loop pragma UNROLL s.i + s.v.l; // 5+0
+  //@ loop unfold s.i + s.v.l; // 5+0
   while (c) {
     i++;
   }
 
 
-  //@ loop pragma UNROLL \max(t[..]); // 4
+  //@ loop unfold \max(t[..]); // 4
   while (c) {
     i++;
   }
 
-  //@ loop pragma UNROLL \min(t[..]); // 0 because of missing initializer
+  //@ loop unfold \min(t[..]); // 0 because of missing initializer
   while (c) {
     i++;
   }
 
-  //@ loop pragma UNROLL \max(\union(1, 1+s.i)); // 6
+  //@ loop unfold \max(\union(1, 1+s.i)); // 6
   while (c) {
     i++;
   }
 
 
-  //@ loop pragma UNROLL \min(t[\union(1, 3)]) + \max(t[\union(1, 3)]); // 2+0
+  //@ loop unfold \min(t[\union(1, 3)]) + \max(t[\union(1, 3)]); // 2+0
   while (c) {
     i++;
   }
 
-  //@ loop pragma UNROLL \min(u[..1].i1) * \max(u[..1].i1); // 2*3
+  //@ loop unfold \min(u[..1].i1) * \max(u[..1].i1); // 2*3
   while (c) {
     i++;
   }
@@ -62,5 +62,3 @@ void main() {
 
 
 }
-
-
diff --git a/tests/syntax/unroll_labels.i b/tests/syntax/unroll_labels.i
index 7747244a7ae8b6e13488bb985d673736de6a9c04..cc85b245b77bb2e776294faefd15b949b7905117 100644
--- a/tests/syntax/unroll_labels.i
+++ b/tests/syntax/unroll_labels.i
@@ -7,7 +7,7 @@ enum { SIX = 6 } ;
 volatile foo;
 void main () {
   int j = 0;
-  /*@ loop pragma UNROLL "completely", 4; */
+  /*@ loop unfold "completely", 4; */
   for (int i=1;i<4;i++) {
     switch (i) {
     case 1: j+=1; break;
@@ -21,7 +21,7 @@ void main () {
   {
     int x = 0;
   L:
-    //@ loop pragma UNROLL 3;
+    //@ loop unfold 3;
     while(x<5) {
       int y=0;
       x++; y++;
@@ -29,13 +29,13 @@ void main () {
   }
 
   j = 0;
-  //@ loop pragma UNROLL SIX;
+  //@ loop unfold SIX;
   while(foo) {
     switch(j) {
     case -1: j++;
       break;
     case 0:
-      //@ loop pragma UNROLL 3;
+      //@ loop unfold 3;
       while (j<5) {j++;}
       break;
     case 5:
@@ -44,19 +44,19 @@ void main () {
     }
   }
 
-  {  
+  {
     if (j==0) goto zero;
     if (j==1) goto un;
     return;
   zero:
-    //@ loop pragma UNROLL 3;
+    //@ loop unfold 3;
     while (j<5) { un: j++;}
   }
 
 }
 
 void main2 () {
-  /*@ loop pragma UNROLL 2; */
+  /*@ loop unfold 2; */
   for (int i=0;i<2;i++) {
     for (int j=0;j<2;j++){
       i += 1;
@@ -68,10 +68,10 @@ void main2 () {
 }
 
 void main2_done () {
-  /*@ loop pragma UNROLL 2;
-    @ loop pragma UNROLL "done", 2; */
+  /*@ loop unfold 2;
+    @ loop unfold "done", 2; */
   for (int i=0;i<2;i++) {
-    /*@ loop pragma UNROLL 2; */
+    /*@ loop unfold 2; */
     for (int j=0;j<2;j++){
       i += 1;
       goto foo;
@@ -84,7 +84,7 @@ void main2_done () {
 void main3 (int c) {
   int i=0;
   if (c == 0) goto foo;
-  /*@ loop pragma UNROLL 2; */
+  /*@ loop unfold 2; */
   for (;i<5;i++) {
     int j = 0 ;
     if (i == j) goto foo;
@@ -102,4 +102,3 @@ void main3 (int c) {
   up:;
   }
 }
-
diff --git a/tests/syntax/unroll_property_status_bts1442.i b/tests/syntax/unroll_property_status_bts1442.i
index 0a8970b5b8990d77268c0b7a7e2b8d8f54512e28..a9939128704514da39f2369ed8ed0be0584779fb 100644
--- a/tests/syntax/unroll_property_status_bts1442.i
+++ b/tests/syntax/unroll_property_status_bts1442.i
@@ -7,7 +7,7 @@ int u(void);
 
 char *strcpy(char*dst, char*src) {
   char* ldst=dst;
-  /*@ loop pragma UNROLL 20; */
+  /*@ loop unfold 20; */
   while (*ldst++ = *src++)
     ;
   return dst;
diff --git a/tests/syntax/unroll_visit.i b/tests/syntax/unroll_visit.i
index f4d949c53ef9a94e93a366b61bbb2a14caf8356c..60bbf94abb1261e78a9178043356b61f68728616 100644
--- a/tests/syntax/unroll_visit.i
+++ b/tests/syntax/unroll_visit.i
@@ -6,7 +6,7 @@ PLUGIN: eva,scope,from,inout
 typedef char i8; // ideally, pretty-printing should keep 'i8' for some casts
 
 void main() {
-   /*@ loop pragma UNROLL 2; */
+   /*@ loop unfold 2; */
   for(i8 i=0; i<100; i++) {
     i--;
     //@ assert i<100;
diff --git a/tests/syntax/very_large_integers.c b/tests/syntax/very_large_integers.c
index 7a203185712a92c869d46f16732c07bfe07cc798..aac454ade3a457ecfb8d55f97b3b578991b02628 100644
--- a/tests/syntax/very_large_integers.c
+++ b/tests/syntax/very_large_integers.c
@@ -136,7 +136,7 @@ int main() {
   do { } while (09);
 #endif
 #ifdef UNROLL_PRAGMA
-  //@ loop pragma UNROLL 99999999999999999999;
+  //@ loop unfold 99999999999999999999;
 #endif
   while (nondet);
   return 0;
diff --git a/tests/test/adpcm.c b/tests/test/adpcm.c
index 0c8d7e005050cd9ac08c833ebc83666d3bebd5fb..0cbd5960dd71649650af4ec3c55b3c6992f35a40 100644
--- a/tests/test/adpcm.c
+++ b/tests/test/adpcm.c
@@ -272,7 +272,7 @@ int encode(int xin1,int xin2)
     tqmf_ptr = tqmf;
     xa = (long)(*tqmf_ptr++) * (*h_ptr++);
     xb = (long)(*tqmf_ptr++) * (*h_ptr++);
-/*@ loop pragma UNROLL 11; */
+/*@ loop unfold 11; */
 /* main multiply accumulate loop for samples and coefficients */
     for(i = 0 ; i < 10 ; i++) {
         xa += (long)(*tqmf_ptr++) * (*h_ptr++);
@@ -284,7 +284,7 @@ int encode(int xin1,int xin2)
 
 /* update delay line tqmf */
     tqmf_ptr1 = tqmf_ptr - 2;
-/*@ loop pragma UNROLL 23; */
+/*@ loop unfold 23; */
     for(i = 0 ; i < 22 ; i++) *tqmf_ptr-- = *tqmf_ptr1--;
     *tqmf_ptr-- = xin1;
     *tqmf_ptr = xin2;
@@ -414,7 +414,7 @@ int filtez(int *bpl,int *dlt)
     int i;
     long int zl;
     zl = (long)(*bpl++) * (*dlt++);
-/*@ loop pragma UNROLL 7; */
+/*@ loop unfold 7; */
     for(i = 1 ; i < 6 ; i++)
         zl += (long)(*bpl++) * (*dlt++);
 
@@ -449,7 +449,7 @@ int quantl(int el,int detl)
         }*/
     mil = 0;
     decis = (decis_levl[mil]*(long)detl) >> 15L;
-/*@ loop pragma UNROLL 30; */
+/*@ loop unfold 30; */
     while(wd <= decis && mil < 29) {             /* FOR/BREAK 662 : 30 possibilities */
       mil++;
       decis = (decis_levl[mil]*(long)detl) >> 15L;
@@ -502,13 +502,13 @@ void upzero(int dlt,int *dlti,int *bli)
     int i,wd2,wd3;
 /*if dlt is zero, then no sum into bli */
     if(dlt == 0) {             /* CONDITION 711 */
-/*@ loop pragma UNROLL 7; */
+/*@ loop unfold 7; */
       for(i = 0 ; i < 6 ; i++) {
         bli[i] = (int)((255L*bli[i]) >> 8L); /* leak factor of 255/256 */
       }
     }
     else {
-/*@ loop pragma UNROLL 7; */
+/*@ loop unfold 7; */
       for(i = 0 ; i < 6 ; i++) {
         if((long)dlt*dlti[i] >= 0) wd2 = 128; else wd2 = -128;   /* CONDITION 718 : 2exp6 possibs */
         wd3 = (int)((255L*bli[i]) >> 8L);    /* leak factor of 255/256 */
@@ -603,7 +603,7 @@ int compressed[10]={0};
 void main () //(int test_data[10], int compressed[10])
 {
   int i;
-  /*@ loop pragma UNROLL 11; loop widen_hints "all", 32767; */   /* Better bounds:    loop invariant detl <= 32064; loop invariant nbh <= 22528; loop invariant nbl <= 18432; */
+  /*@ loop unfold 11; loop widen_hints "all", 32767; */   /* Better bounds:    loop invariant detl <= 32064; loop invariant nbh <= 22528; loop invariant nbl <= 18432; */
   for(i = 0 ; i < 10 ; i += 2)
     compressed[i/2] = encode(test_data[i],test_data[i+1]);
 
diff --git a/tests/test/oracle/adpcm.res.oracle b/tests/test/oracle/adpcm.res.oracle
index 20799a40a8be991c8d9203ef0536131043d8b2f0..7aff5b9c985a6cf322b88737f9b19592e2828b21 100644
--- a/tests/test/oracle/adpcm.res.oracle
+++ b/tests/test/oracle/adpcm.res.oracle
@@ -1679,10 +1679,10 @@
 [inout] Inputs for function filtep:
     \nothing
 [inout] Out (internal) for function filtez:
-    bpl; dlt_0; i; zl; tmp; tmp_0; __retres; tmp_1_unroll_123;
-    tmp_2_unroll_123; tmp_1_unroll_126; tmp_2_unroll_126; tmp_1_unroll_129;
-    tmp_2_unroll_129; tmp_1_unroll_132; tmp_2_unroll_132; tmp_1_unroll_135;
-    tmp_2_unroll_135
+    bpl; dlt_0; i; zl; tmp; tmp_0; __retres; tmp_1_unfold_123;
+    tmp_2_unfold_123; tmp_1_unfold_126; tmp_2_unfold_126; tmp_1_unfold_129;
+    tmp_2_unfold_129; tmp_1_unfold_132; tmp_2_unfold_132; tmp_1_unfold_135;
+    tmp_2_unfold_135
 [inout] Inputs for function filtez:
     delay_bpl[0..5]; delay_dltx[0..5]; delay_dhx[0..5]; delay_bph[0..5]
 [inout] Out (internal) for function logsch:
@@ -1720,28 +1720,28 @@
     rlt1; rlt2; detl; deth; sh; eh; dh; ih; nbh; szh; sph; ph; yh;
     delay_dhx{[0..1]; [3..5]}; delay_bph[0..5]; ah1; ah2; ph1; ph2; rh1; 
     rh2; i; h_ptr; tqmf_ptr; tqmf_ptr1; xa; xb; decis; tmp; tmp_0; tmp_1;
-    tmp_2; tmp_7; tmp_8; tmp_9; tmp_12; tmp_13; __retres; tmp_3_unroll_8;
-    tmp_4_unroll_8; tmp_5_unroll_8; tmp_6_unroll_8; tmp_3_unroll_12;
-    tmp_4_unroll_12; tmp_5_unroll_12; tmp_6_unroll_12; tmp_3_unroll_16;
-    tmp_4_unroll_16; tmp_5_unroll_16; tmp_6_unroll_16; tmp_3_unroll_20;
-    tmp_4_unroll_20; tmp_5_unroll_20; tmp_6_unroll_20; tmp_3_unroll_24;
-    tmp_4_unroll_24; tmp_5_unroll_24; tmp_6_unroll_24; tmp_3_unroll_28;
-    tmp_4_unroll_28; tmp_5_unroll_28; tmp_6_unroll_28; tmp_3_unroll_32;
-    tmp_4_unroll_32; tmp_5_unroll_32; tmp_6_unroll_32; tmp_3_unroll_36;
-    tmp_4_unroll_36; tmp_5_unroll_36; tmp_6_unroll_36; tmp_3_unroll_40;
-    tmp_4_unroll_40; tmp_5_unroll_40; tmp_6_unroll_40; tmp_3_unroll_44;
-    tmp_4_unroll_44; tmp_5_unroll_44; tmp_6_unroll_44; tmp_10_unroll_51;
-    tmp_11_unroll_51; tmp_10_unroll_54; tmp_11_unroll_54; tmp_10_unroll_57;
-    tmp_11_unroll_57; tmp_10_unroll_60; tmp_11_unroll_60; tmp_10_unroll_63;
-    tmp_11_unroll_63; tmp_10_unroll_66; tmp_11_unroll_66; tmp_10_unroll_69;
-    tmp_11_unroll_69; tmp_10_unroll_72; tmp_11_unroll_72; tmp_10_unroll_75;
-    tmp_11_unroll_75; tmp_10_unroll_78; tmp_11_unroll_78; tmp_10_unroll_81;
-    tmp_11_unroll_81; tmp_10_unroll_84; tmp_11_unroll_84; tmp_10_unroll_87;
-    tmp_11_unroll_87; tmp_10_unroll_90; tmp_11_unroll_90; tmp_10_unroll_93;
-    tmp_11_unroll_93; tmp_10_unroll_96; tmp_11_unroll_96; tmp_10_unroll_99;
-    tmp_11_unroll_99; tmp_10_unroll_102; tmp_11_unroll_102; tmp_10_unroll_105;
-    tmp_11_unroll_105; tmp_10_unroll_108; tmp_11_unroll_108; tmp_10_unroll_111;
-    tmp_11_unroll_111; tmp_10_unroll_114; tmp_11_unroll_114
+    tmp_2; tmp_7; tmp_8; tmp_9; tmp_12; tmp_13; __retres; tmp_3_unfold_8;
+    tmp_4_unfold_8; tmp_5_unfold_8; tmp_6_unfold_8; tmp_3_unfold_12;
+    tmp_4_unfold_12; tmp_5_unfold_12; tmp_6_unfold_12; tmp_3_unfold_16;
+    tmp_4_unfold_16; tmp_5_unfold_16; tmp_6_unfold_16; tmp_3_unfold_20;
+    tmp_4_unfold_20; tmp_5_unfold_20; tmp_6_unfold_20; tmp_3_unfold_24;
+    tmp_4_unfold_24; tmp_5_unfold_24; tmp_6_unfold_24; tmp_3_unfold_28;
+    tmp_4_unfold_28; tmp_5_unfold_28; tmp_6_unfold_28; tmp_3_unfold_32;
+    tmp_4_unfold_32; tmp_5_unfold_32; tmp_6_unfold_32; tmp_3_unfold_36;
+    tmp_4_unfold_36; tmp_5_unfold_36; tmp_6_unfold_36; tmp_3_unfold_40;
+    tmp_4_unfold_40; tmp_5_unfold_40; tmp_6_unfold_40; tmp_3_unfold_44;
+    tmp_4_unfold_44; tmp_5_unfold_44; tmp_6_unfold_44; tmp_10_unfold_51;
+    tmp_11_unfold_51; tmp_10_unfold_54; tmp_11_unfold_54; tmp_10_unfold_57;
+    tmp_11_unfold_57; tmp_10_unfold_60; tmp_11_unfold_60; tmp_10_unfold_63;
+    tmp_11_unfold_63; tmp_10_unfold_66; tmp_11_unfold_66; tmp_10_unfold_69;
+    tmp_11_unfold_69; tmp_10_unfold_72; tmp_11_unfold_72; tmp_10_unfold_75;
+    tmp_11_unfold_75; tmp_10_unfold_78; tmp_11_unfold_78; tmp_10_unfold_81;
+    tmp_11_unfold_81; tmp_10_unfold_84; tmp_11_unfold_84; tmp_10_unfold_87;
+    tmp_11_unfold_87; tmp_10_unfold_90; tmp_11_unfold_90; tmp_10_unfold_93;
+    tmp_11_unfold_93; tmp_10_unfold_96; tmp_11_unfold_96; tmp_10_unfold_99;
+    tmp_11_unfold_99; tmp_10_unfold_102; tmp_11_unfold_102; tmp_10_unfold_105;
+    tmp_11_unfold_105; tmp_10_unfold_108; tmp_11_unfold_108; tmp_10_unfold_111;
+    tmp_11_unfold_111; tmp_10_unfold_114; tmp_11_unfold_114
 [inout] Inputs for function encode:
     tqmf[0..23]; h[0..23]; xl; xh; il; szl; spl; sl; el;
     qq4_code4_table{[1]; [8]; [15]}; delay_bpl[0..5]; delay_dltx[0..5];
diff --git a/tests/value/f2.i b/tests/value/f2.i
index 476765a83d193f2a90332a57d4fa24edb59d940e..88bd0e9b50ac5979f934ad5ede3c98ceef96abb7 100644
--- a/tests/value/f2.i
+++ b/tests/value/f2.i
@@ -1,10 +1,10 @@
 /* run.config*
-  
+
   STDOPT: #"-main f"
 */
 int f(int x) {
 /* Here we are */
-/*@ loop pragma UNROLL 10; */
+/*@ loop unfold 10; */
   while(1) { return 0 ;}
   return 2;
 }
diff --git a/tests/value/ghost.i b/tests/value/ghost.i
index 6e602983f0bf0cb8d833469da4b37cd393922909..e8836c6e2a8a520d90c0c24f570de756e84da504 100644
--- a/tests/value/ghost.i
+++ b/tests/value/ghost.i
@@ -12,7 +12,7 @@ int main () {
   G = 0;
 /*@ghost GHOST=G+G ; */
 /* Commentaire avant loop */
- /*@ loop pragma UNROLL 0; */
+ /*@ loop unfold 0; */
   for(i=0; i<=10; i++)
     G++;
 
diff --git a/tests/value/local_slevel.i b/tests/value/local_slevel.i
index d40c3caf0477abdabcdbefad413537242c25ce91..7c127424f77fc006e54230fd5e7abc64082dea8c 100644
--- a/tests/value/local_slevel.i
+++ b/tests/value/local_slevel.i
@@ -24,7 +24,7 @@ void main1() {
 }
 
 void g() {// Do not crash when loop unrolling clears the dependencies of the AST
-  //@ loop pragma UNROLL 1;
+  //@ loop unfold 1;
   for (int i=0; i<5; i++) {
   }
 }
diff --git a/tests/value/oracle/local_slevel.res.oracle b/tests/value/oracle/local_slevel.res.oracle
index 2022cd839a084f2561dfe73db96230c219eec2c3..cb2e9dae5e0e8997cc780bf104b75a7fc9185a40 100644
--- a/tests/value/oracle/local_slevel.res.oracle
+++ b/tests/value/oracle/local_slevel.res.oracle
@@ -200,13 +200,13 @@ void main1(void)
 void g(void)
 {
   int i = 0;
-  if (! (i < 5)) goto unrolling_2_loop;
+  if (! (i < 5)) goto unfolding_2_loop;
   i ++;
-  unrolling_3_loop: ;
-  /*@ loop pragma UNROLL 1;
-      loop pragma UNROLL "done", 1; */
+  unfolding_3_loop: ;
+  /*@ loop unfold 1;
+      loop unfold "done", 1; */
   while (i < 5) i ++;
-  unrolling_2_loop: ;
+  unfolding_2_loop: ;
   return;
 }
 
@@ -266,13 +266,13 @@ void main1(void)
 void g(void)
 {
   int i = 0;
-  if (! (i < 5)) goto unrolling_2_loop;
+  if (! (i < 5)) goto unfolding_2_loop;
   i ++;
-  unrolling_3_loop: ;
-  /*@ loop pragma UNROLL 1;
-      loop pragma UNROLL "done", 1; */
+  unfolding_3_loop: ;
+  /*@ loop unfold 1;
+      loop unfold "done", 1; */
   while (i < 5) i ++;
-  unrolling_2_loop: ;
+  unfolding_2_loop: ;
   return;
 }
 
@@ -332,13 +332,13 @@ void main1(void)
 void g(void)
 {
   int i = 0;
-  if (! (i < 5)) goto unrolling_2_loop;
+  if (! (i < 5)) goto unfolding_2_loop;
   i ++;
-  unrolling_3_loop: ;
-  /*@ loop pragma UNROLL 1;
-      loop pragma UNROLL "done", 1; */
+  unfolding_3_loop: ;
+  /*@ loop unfold 1;
+      loop unfold "done", 1; */
   while (i < 5) i ++;
-  unrolling_2_loop: ;
+  unfolding_2_loop: ;
   return;
 }
 
diff --git a/tests/value/oracle/strings.res.oracle b/tests/value/oracle/strings.res.oracle
index 17a53f17bdc53a87de17f235c7ae66c7f93e46f1..e07c92d0d5dcf8d5efe1fc2b5ae5b8d42e44b112 100644
--- a/tests/value/oracle/strings.res.oracle
+++ b/tests/value/oracle/strings.res.oracle
@@ -69,8 +69,8 @@
   Called from strings.i:53.
 [eva:alarm] strings.i:23: Warning: 
   out of bounds write.
-  assert \valid(tmp_unroll_46);
-  (tmp_unroll_46 from ldst++)
+  assert \valid(tmp_unfold_46);
+  (tmp_unfold_46 from ldst++)
 [kernel] strings.i:23: Warning: 
   all target addresses were invalid. This path is assumed to be dead.
 [eva] Recording results for strcpy
@@ -387,11 +387,11 @@
 [inout] Inputs for function long_chain:
     ANYTHING(origin:Unknown)
 [inout] Out (internal) for function strcpy:
-    src; ldst; b[0..4]; tmp_unroll_46; tmp_1_unroll_46; tmp_0_unroll_46;
-    tmp_unroll_49; tmp_1_unroll_49; tmp_0_unroll_49; tmp_unroll_52;
-    tmp_1_unroll_52; tmp_0_unroll_52; tmp_unroll_55; tmp_1_unroll_55;
-    tmp_0_unroll_55; tmp_unroll_58; tmp_1_unroll_58; tmp_0_unroll_58;
-    tmp_unroll_61; tmp_1_unroll_61; tmp_0_unroll_61
+    src; ldst; b[0..4]; tmp_unfold_46; tmp_1_unfold_46; tmp_0_unfold_46;
+    tmp_unfold_49; tmp_1_unfold_49; tmp_0_unfold_49; tmp_unfold_52;
+    tmp_1_unfold_52; tmp_0_unfold_52; tmp_unfold_55; tmp_1_unfold_55;
+    tmp_0_unfold_55; tmp_unfold_58; tmp_1_unfold_58; tmp_0_unfold_58;
+    tmp_unfold_61; tmp_1_unfold_61; tmp_0_unfold_61
 [inout] Inputs for function strcpy:
     a[0..5]
 [inout] Out (internal) for function string_writes:
@@ -399,8 +399,8 @@
 [inout] Inputs for function string_writes:
     nondet; s3; s4; s5; s6; cc; "tutu"[bits 0 to 7]
 [inout] Out (internal) for function strlen:
-    s; l; tmp_unroll_106; tmp_unroll_109; tmp_unroll_112; tmp_unroll_115;
-    tmp_unroll_118; tmp_unroll_121
+    s; l; tmp_unfold_106; tmp_unfold_109; tmp_unfold_112; tmp_unfold_115;
+    tmp_unfold_118; tmp_unfold_121
 [inout] Inputs for function strlen:
     s1[0..5]
 [inout] Out (internal) for function string_comparison:
diff --git a/tests/value/oracle/unroll.res.oracle b/tests/value/oracle/unroll.res.oracle
index 7bba5131c292d633f107952fbaf5ded1860b83d2..c36bdf2bce155daeb3624c34432aba55098370b2 100644
--- a/tests/value/oracle/unroll.res.oracle
+++ b/tests/value/oracle/unroll.res.oracle
@@ -1,7 +1,7 @@
 [kernel] Parsing unroll.i (no preprocessing)
 [kernel] unroll.i:49: Warning: 
-  ignoring unrolling directive (not an understood constant expression)
-[kernel] unroll.i:54: Warning: ignoring invalid unrolling directive
+  ignoring unfolding directive (not an understood constant expression)
+[kernel] unroll.i:54: Warning: ignoring invalid unfolding directive
 [eva] Analyzing a complete application starting at main
 [eva] Computing initial state
 [eva] Initial state computed
@@ -32,8 +32,8 @@
   NO EFFECTS
 [from] ====== END OF DEPENDENCIES ======
 [inout] Out (internal) for function main:
-    c; G; i; MAX; JMAX; j; k; S; tmp; tmp_unroll_3752; tmp_unroll_3760;
-    tmp_unroll_3768; tmp_unroll_3776; tmp_unroll_3784; tmp_unroll_3792;
-    tmp_unroll_3800; tmp_unroll_3808; tmp_unroll_3816; tmp_unroll_3824
+    c; G; i; MAX; JMAX; j; k; S; tmp; tmp_unfold_3752; tmp_unfold_3760;
+    tmp_unfold_3768; tmp_unfold_3776; tmp_unfold_3784; tmp_unfold_3792;
+    tmp_unfold_3800; tmp_unfold_3808; tmp_unfold_3816; tmp_unfold_3824
 [inout] Inputs for function main:
     \nothing
diff --git a/tests/value/oracle/unroll_simple.res.oracle b/tests/value/oracle/unroll_simple.res.oracle
index c2a14ecd291d27223b0b2cbdd656c3c19ad75c35..503c58f70d4d7da6f10ede70c1c62bf1c38896fc 100644
--- a/tests/value/oracle/unroll_simple.res.oracle
+++ b/tests/value/oracle/unroll_simple.res.oracle
@@ -27,8 +27,8 @@
   NO EFFECTS
 [from] ====== END OF DEPENDENCIES ======
 [inout] Out (internal) for function main:
-    c; G; i; MAX; JMAX; j; tmp; tmp_unroll_774; tmp_unroll_782; tmp_unroll_790;
-    tmp_unroll_798; tmp_unroll_806; tmp_unroll_814; tmp_unroll_822;
-    tmp_unroll_830; tmp_unroll_838; tmp_unroll_846
+    c; G; i; MAX; JMAX; j; tmp; tmp_unfold_774; tmp_unfold_782; tmp_unfold_790;
+    tmp_unfold_798; tmp_unfold_806; tmp_unfold_814; tmp_unfold_822;
+    tmp_unfold_830; tmp_unfold_838; tmp_unfold_846
 [inout] Inputs for function main:
     \nothing
diff --git a/tests/value/strings.i b/tests/value/strings.i
index 0f6087161602aca84fc72009a38b18e5ccb75272..fbb7d4654212d35b89d08a8ad9aca758caa09ab0 100644
--- a/tests/value/strings.i
+++ b/tests/value/strings.i
@@ -19,7 +19,7 @@ char Q, R, S, T, U, V, W, X, Y, Z;
 
 char *strcpy(char*dst, char*src) {
   char* ldst=dst;
-  /*@ loop pragma UNROLL 20; */
+  /*@ loop unfold 20; */
   while (*ldst++ = *src++)
     ;
   return dst;
@@ -27,7 +27,7 @@ char *strcpy(char*dst, char*src) {
 
 unsigned int strlen(char *s) {
   unsigned int l=0;
- /*@ loop pragma UNROLL 20; */
+ /*@ loop unfold 20; */
   while(*s++ != 0)
     l++;
   return l;
diff --git a/tests/value/unroll.i b/tests/value/unroll.i
index e85280c3f7a13802263a86e813bf110a7310c1b7..30e8d256760cb5facc015d9c22814914654fac1e 100644
--- a/tests/value/unroll.i
+++ b/tests/value/unroll.i
@@ -5,21 +5,21 @@ void main (int c) {
   int MAX = 12;
   int JMAX=5;
   int j,k,S;
-  /*@ loop pragma UNROLL 14; */ // first loop unrolled 14 times
+  /*@ loop unfold 14; */ // first loop unrolled 14 times
   for (i=0; i<=MAX; i++)
     {
       G+=i;
     }
-  /*@ loop pragma UNROLL 124; */
+  /*@ loop unfold 124; */
   for (i=0; i<=10*MAX; i++)
     {
       G+=i;
     }
-  /*@ loop pragma UNROLL 12+2; */ // loop unrolled 14 times
+  /*@ loop unfold 12+2; */ // loop unrolled 14 times
   for (i=0; i<=MAX; i++)
     {
       j=0;
-      /*@ loop pragma UNROLL FIFTY_TIMES; */
+      /*@ loop unfold FIFTY_TIMES; */
       while (j<=JMAX)
         {
           G+=i;
@@ -27,7 +27,7 @@ void main (int c) {
           }
     }
 
-//@ loop pragma UNROLL 128*sizeof(char);
+//@ loop unfold 128*sizeof(char);
   do {
     G += i;
     i++;
@@ -35,7 +35,7 @@ void main (int c) {
     }
   while (i<=256 || j>=0);
 
-//@ loop pragma UNROLL 10;
+//@ loop unfold 10;
  do
     { if(c) continue;
 
@@ -45,17 +45,17 @@ void main (int c) {
       }
   while(c);
 
-//@ loop pragma UNROLL c;
+//@ loop unfold c;
  while(0);
 
  S=1;
  k=1;
- //@ loop pragma UNROLL "completly", NB_TIMES;
+ //@ loop unfold "completly", NB_TIMES;
  do {
    S=S*k;
-   k++; 
+   k++;
  } while (k <= NB_TIMES) ;
- 
+
 }
 
 #if 0
@@ -69,7 +69,7 @@ int main2(int c,signed char nr_map) {
   biosmap = g_biosmap;
   if (nr_map<2)  return (-1);
 
-//@ loop pragma UNROLL 200;
+//@ loop unfold 200;
   do {
     unsigned long long start = biosmap->addr;
     unsigned long long size = biosmap->size;
diff --git a/tests/value/unroll_simple.i b/tests/value/unroll_simple.i
index 1a97949fa5cfff01cee54d6547f5a2974d0ae4e5..b0d0ff00e1885936732b34415d446d01e1827c05 100644
--- a/tests/value/unroll_simple.i
+++ b/tests/value/unroll_simple.i
@@ -4,7 +4,7 @@ void main (int c) {
   int JMAX=5;
   int j=3;
 
-//@ loop pragma UNROLL 128;
+//@ loop unfold 128;
   do {
     G += i;
     i++;
@@ -12,7 +12,7 @@ void main (int c) {
     }
   while (i<=256 || j>=0);
 
-//@ loop pragma UNROLL 10;
+//@ loop unfold 10;
  do
     { if(c) continue;
 
diff --git a/tests/value/with_comment.i b/tests/value/with_comment.i
index 61839445263bd8194a3584407fe62cea50942efc..19fc0e342d7779c387b0d73c03bb4f22220c1e05 100644
--- a/tests/value/with_comment.i
+++ b/tests/value/with_comment.i
@@ -1,5 +1,5 @@
 /* run.config*
-  
+
   STDOPT: #"-main main2"
 */
 /* Commentaire avant G comment*/ /* Commentaire avant G2 comment*/
@@ -16,7 +16,7 @@ int main2 () {
   G = 0;
 
 /* Commentaire avant loop comment*/
- /*@ loop pragma UNROLL 0; */
+ /*@ loop unfold 0; */
   for(i=0; i<=10; i++)
     G++;