diff --git a/src/example-archive/c-testsuite/working/00021.working.c b/src/example-archive/c-testsuite/working/00021.working.c
index 4c03382d..e5fcf5ce 100644
--- a/src/example-archive/c-testsuite/working/00021.working.c
+++ b/src/example-archive/c-testsuite/working/00021.working.c
@@ -4,8 +4,8 @@ foo(int a, int b)
 			let mid = (2i64 + (i64) a);
 			let res = mid - (i64) b;  
 			(i64) MINi32() <= mid; mid <= (i64) MAXi32(); 
-			(i64) MINi32() <= res; res <= (i64) MAXi32(); @*/
-/*@ ensures return == (2i32 + a) - b; @*/
+			(i64) MINi32() <= res; res <= (i64) MAXi32(); 
+    ensures return == (2i32 + a) - b; @*/
 {
 	return 2 + a - b;
 }
diff --git a/src/example-archive/c-testsuite/working/00023.working.c b/src/example-archive/c-testsuite/working/00023.working.c
index 773aa3f9..ffd57ba5 100644
--- a/src/example-archive/c-testsuite/working/00023.working.c
+++ b/src/example-archive/c-testsuite/working/00023.working.c
@@ -2,8 +2,8 @@ int x;
 
 int
 main()
-/*@ accesses x; @*/
-/*@ ensures return == 0i32; @*/
+/*@ accesses x;
+    ensures return == 0i32; @*/
 {
 	x = 0;
 	return x;
diff --git a/src/example-archive/c-testsuite/working/00024.working.c b/src/example-archive/c-testsuite/working/00024.working.c
index e949129c..8d3d6e72 100644
--- a/src/example-archive/c-testsuite/working/00024.working.c
+++ b/src/example-archive/c-testsuite/working/00024.working.c
@@ -4,8 +4,8 @@ s v;
 
 int
 main()
-/*@ accesses v; @*/
-/*@ ensures return == 0i32; @*/
+/*@ accesses v;
+    ensures return == 0i32; @*/
 {
 	v.x = 1;
 	v.y = 2;
diff --git a/src/example-archive/c-testsuite/working/00033.working.c b/src/example-archive/c-testsuite/working/00033.working.c
index f47f648e..058ac64b 100644
--- a/src/example-archive/c-testsuite/working/00033.working.c
+++ b/src/example-archive/c-testsuite/working/00033.working.c
@@ -3,8 +3,8 @@ int g;
 int
 effect()
 /*@ requires 
-        take Pre = RW<int>(&g); @*/
-/*@ ensures 
+        take Pre = RW<int>(&g);
+    ensures 
         take Post = RW<int>(&g); 
         Post == 1i32;  
         return == 1i32; @*/
@@ -16,10 +16,10 @@ effect()
 int
 main()
 /*@ requires 
-        take Pre = RW<int>(&g); @*/
-/*@ ensures 
-        take Post = RW<int>(&g); @*/
-/*@ ensures return == 0i32; @*/
+        take Pre = RW<int>(&g);
+    ensures 
+        take Post = RW<int>(&g);
+        return == 0i32; @*/
 {
     int x;
     
diff --git a/src/example-archive/c-testsuite/working/00047.working.c b/src/example-archive/c-testsuite/working/00047.working.c
index f60a3de0..226fa68d 100644
--- a/src/example-archive/c-testsuite/working/00047.working.c
+++ b/src/example-archive/c-testsuite/working/00047.working.c
@@ -2,12 +2,12 @@ struct { int a; int b; int c; } s = {1, 2, 3};
 
 int
 main()
-/*@ accesses s; @*/
-/*@ requires 
+/*@ accesses s;
+    requires 
 			s.a == 1i32;
 			s.b == 2i32; 
-			s.c == 3i32; @*/
-/*@ ensures return == 0i32; @*/
+			s.c == 3i32;
+    ensures return == 0i32; @*/
 {
 	if (s.a != 1)
 		return 1;
diff --git a/src/example-archive/c-testsuite/working/00048.working.c b/src/example-archive/c-testsuite/working/00048.working.c
index ed5dee9f..9904be52 100644
--- a/src/example-archive/c-testsuite/working/00048.working.c
+++ b/src/example-archive/c-testsuite/working/00048.working.c
@@ -3,11 +3,11 @@ struct S s = { .b = 2, .a = 1};
 
 int
 main()
-/*@ accesses s; @*/
-/*@ requires 
+/*@ accesses s;
+    requires 
 			s.a == 1i32;
-			s.b == 2i32; @*/
-/*@ ensures return == 0i32; @*/
+			s.b == 2i32;
+    ensures return == 0i32; @*/
 {
 	if(s.a != 1)
 		return 1;
diff --git a/src/example-archive/c-testsuite/working/00062.working.c b/src/example-archive/c-testsuite/working/00062.working.c
index 22fc49d9..29570d9d 100644
--- a/src/example-archive/c-testsuite/working/00062.working.c
+++ b/src/example-archive/c-testsuite/working/00062.working.c
@@ -16,9 +16,9 @@ int x = 0;
 
 int
 main()
-/*@ accesses x; @*/
-/*@ requires x == 0i32; @*/
-/*@ ensures return == 0i32; @*/
+/*@ accesses x;
+    requires x == 0i32;
+    ensures return == 0i32; @*/
 {
 	return x;
 }
diff --git a/src/example-archive/c-testsuite/working/00067.working.c b/src/example-archive/c-testsuite/working/00067.working.c
index 799265e5..ba1ac25b 100644
--- a/src/example-archive/c-testsuite/working/00067.working.c
+++ b/src/example-archive/c-testsuite/working/00067.working.c
@@ -13,9 +13,9 @@ int x = 1;
 #endif
 
 int main()
-/*@ accesses x; @*/
-/*@ requires x == 0i32; @*/
-/*@ ensures return == 0i32; @*/
+/*@ accesses x;
+    requires x == 0i32;
+    ensures return == 0i32; @*/
 {
 	return x;
 }
diff --git a/src/example-archive/c-testsuite/working/00068.working.c b/src/example-archive/c-testsuite/working/00068.working.c
index 6556d681..a3e758b1 100644
--- a/src/example-archive/c-testsuite/working/00068.working.c
+++ b/src/example-archive/c-testsuite/working/00068.working.c
@@ -8,9 +8,9 @@ X
 
 int
 main()
-/*@ accesses x; @*/
-/*@ requires x == 0i32; @*/
-/*@ ensures return == 0i32; @*/
+/*@ accesses x;
+    requires x == 0i32;
+    ensures return == 0i32; @*/
 {
 	return x;
 }
diff --git a/src/example-archive/c-testsuite/working/00069.working.c b/src/example-archive/c-testsuite/working/00069.working.c
index c09cf6ac..66e7b70a 100644
--- a/src/example-archive/c-testsuite/working/00069.working.c
+++ b/src/example-archive/c-testsuite/working/00069.working.c
@@ -8,9 +8,9 @@ int x = 0;
 
 int
 main()
-/*@ accesses x; @*/
-/*@ requires x == 0i32; @*/
-/*@ ensures return == 0i32; @*/
+/*@ accesses x;
+    requires x == 0i32;
+    ensures return == 0i32; @*/
 {
 	return x;
 }
diff --git a/src/example-archive/c-testsuite/working/00070.working.c b/src/example-archive/c-testsuite/working/00070.working.c
index b80fde3a..382bc2c9 100644
--- a/src/example-archive/c-testsuite/working/00070.working.c
+++ b/src/example-archive/c-testsuite/working/00070.working.c
@@ -10,9 +10,9 @@ X
 
 int
 main()
-/*@ accesses x; @*/
-/*@ requires x == 0i32; @*/
-/*@ ensures return == 0i32; @*/
+/*@ accesses x;
+    requires x == 0i32;
+    ensures return == 0i32; @*/
 {
 	return x;
 }
diff --git a/src/example-archive/c-testsuite/working/00078.working.c b/src/example-archive/c-testsuite/working/00078.working.c
index 90678dea..b94187b0 100644
--- a/src/example-archive/c-testsuite/working/00078.working.c
+++ b/src/example-archive/c-testsuite/working/00078.working.c
@@ -1,8 +1,8 @@
 int
 f1(char *p)
 /*@ requires 
-			take PreP = RW<char>(p); @*/
-/*@ ensures 
+			take PreP = RW<char>(p);
+    ensures 
 			take PostP = RW<char>(p);
 			return == 1i32 + (i32) PreP; @*/
 {
diff --git a/src/example-archive/c-testsuite/working/00090.working.c b/src/example-archive/c-testsuite/working/00090.working.c
index f9e29452..245882bc 100644
--- a/src/example-archive/c-testsuite/working/00090.working.c
+++ b/src/example-archive/c-testsuite/working/00090.working.c
@@ -4,13 +4,13 @@ int a[3] = {0, 1, 2};
 
 int
 main()
-/*@ accesses a; @*/
-/*@ requires 
+/*@ accesses a;
+    requires 
 			a[0u64] == 0i32; 
 			a[1u64] == 1i32; 
 			a[2u64] == 2i32; 
-			@*/
-/*@ ensures return == 0i32; @*/
+
+    ensures return == 0i32; @*/
 {
 	/*@ focus RW<int>, 0u64; @*/
 	/*@ focus RW<int>, 1u64; @*/
diff --git a/src/example-archive/c-testsuite/working/00096.working.c b/src/example-archive/c-testsuite/working/00096.working.c
index 89008665..0bb5e671 100644
--- a/src/example-archive/c-testsuite/working/00096.working.c
+++ b/src/example-archive/c-testsuite/working/00096.working.c
@@ -2,8 +2,8 @@ int x, x = 3, x;
 
 int
 main()
-/*@ accesses x; @*/
-/*@ ensures return == 0i32; @*/
+/*@ accesses x;
+    ensures return == 0i32; @*/
 {
 	if (x != 3)
 		return 0;
diff --git a/src/example-archive/c-testsuite/working/00107.working.c b/src/example-archive/c-testsuite/working/00107.working.c
index 14ee49a9..643cf510 100644
--- a/src/example-archive/c-testsuite/working/00107.working.c
+++ b/src/example-archive/c-testsuite/working/00107.working.c
@@ -3,9 +3,9 @@ myint x = (myint)1;
 
 int
 main(void)
-/*@ accesses x; @*/
-/*@ requires x == 1i32; @*/
-/*@ ensures return == 0i32; @*/
+/*@ accesses x;
+    requires x == 1i32;
+    ensures return == 0i32; @*/
 {
 	return x-1;
 }
diff --git a/src/example-archive/c-testsuite/working/00146.working.c b/src/example-archive/c-testsuite/working/00146.working.c
index 050043a3..bfbd53a7 100644
--- a/src/example-archive/c-testsuite/working/00146.working.c
+++ b/src/example-archive/c-testsuite/working/00146.working.c
@@ -3,11 +3,11 @@ struct S s = {1, 2};
 
 int
 main()
-/*@ accesses s; @*/
-/*@ requires 
+/*@ accesses s;
+    requires 
 			s.a == 1i32; 
-			s.b == 2i32; @*/
-/*@ ensures return == 0i32; @*/
+			s.b == 2i32;
+    ensures return == 0i32; @*/
 {
 	if(s.a != 1)
 		return 1;
diff --git a/src/example-archive/dafny-tutorial/working/abs_1.c b/src/example-archive/dafny-tutorial/working/abs_1.c
index 5f5a14ab..1225c5c0 100644
--- a/src/example-archive/dafny-tutorial/working/abs_1.c
+++ b/src/example-archive/dafny-tutorial/working/abs_1.c
@@ -14,8 +14,8 @@ function (i32) abs_spec(i32 x)
 int abs(int x)
 /*@ requires 
       let MINi32 = (i64) -2147483647i64;
-      MINi32 < (i64) x; @*/
-/*@ ensures 
+      MINi32 < (i64) x;
+    ensures 
       0i32 <= return; 
       (x < 0i32 && return == (0i32 - x)) || (0i32 <= x && return == x); 
       0i32 <= return && (return == x || return == (0i32 - x));  // Same property
diff --git a/src/example-archive/dafny-tutorial/working/abs_2.c b/src/example-archive/dafny-tutorial/working/abs_2.c
index c048c02d..e1406d01 100644
--- a/src/example-archive/dafny-tutorial/working/abs_2.c
+++ b/src/example-archive/dafny-tutorial/working/abs_2.c
@@ -6,8 +6,8 @@ int abs_2(int x)
       let MINi32 = (i64) -2147483647i64;
 
       MINi32 <= (i64) x; 
-      x < 0i32; @*/
-/*@ ensures 
+      x < 0i32;
+    ensures 
       0i32 <= return; 
       (return == x || return == (0i32 - x)); @*/
 {
diff --git a/src/example-archive/dafny-tutorial/working/abs_3.c b/src/example-archive/dafny-tutorial/working/abs_3.c
index 6200d350..f85490ef 100644
--- a/src/example-archive/dafny-tutorial/working/abs_3.c
+++ b/src/example-archive/dafny-tutorial/working/abs_3.c
@@ -3,8 +3,8 @@
 
 int abs_3(int x)
 /*@ requires 
-      x == (0i32 - 1i32); @*/ // TODO: syntax is bad 
-/*@ ensures 
+      x == (0i32 - 1i32);  // TODO: syntax is bad 
+    ensures 
       0i32 <= return;
       (return == x || return == (0i32 - x)); 
       return == 1i32; @*/
diff --git a/src/example-archive/dafny-tutorial/working/binary_search.c b/src/example-archive/dafny-tutorial/working/binary_search.c
index 62c3cb74..0891241e 100644
--- a/src/example-archive/dafny-tutorial/working/binary_search.c
+++ b/src/example-archive/dafny-tutorial/working/binary_search.c
@@ -8,8 +8,8 @@ int binary_search(int *a, int length, int value)
       0i32 <= length; 
       (2i64 * (i64) length) <= MAXi32; 
       take IndexPre = each (i32 j; 0i32 <= j && j < length)
-                           {RW<int>(a + j)}; @*/
-/*@ ensures 
+                           {RW<int>(a + j)};
+    ensures 
       take IndexPost = each (i32 j; 0i32 <= j && j < length)
                             {RW<int>(a + j)}; 
       IndexPost == IndexPre; 
diff --git a/src/example-archive/dafny-tutorial/working/linear_search.c b/src/example-archive/dafny-tutorial/working/linear_search.c
index 71409722..99cc9a65 100644
--- a/src/example-archive/dafny-tutorial/working/linear_search.c
+++ b/src/example-archive/dafny-tutorial/working/linear_search.c
@@ -4,8 +4,8 @@ int linear_search(int *a, int length, int key)
 /*@ requires 
       0i32 < length; 
       take IndexPre = each (i32 j; 0i32 <= j && j < length)
-                           {RW<int>(a + j)}; @*/
-/*@ ensures 
+                           {RW<int>(a + j)};
+    ensures 
       take IndexPost = each (i32 j; 0i32 <= j && j < length)
                             {RW<int>(a + j)};
       (return < 0i32) || (IndexPost[return] == key); 
diff --git a/src/example-archive/dafny-tutorial/working/max.c b/src/example-archive/dafny-tutorial/working/max.c
index 81291ae3..f1d32d2a 100644
--- a/src/example-archive/dafny-tutorial/working/max.c
+++ b/src/example-archive/dafny-tutorial/working/max.c
@@ -14,8 +14,8 @@ function (i32) max_spec (i32 a, i32 b)
 
 int max(int a, int b)
 /*@ ensures 
-      (a >= b && return == a) || (a < b && return == b); @*/
-/*@ ensures 
+      (a >= b && return == a) || (a < b && return == b);
+
       return == max_spec(a,b); @*/
 {
   if (a > b)
diff --git a/src/example-archive/dafny-tutorial/working/multiple_returns.c b/src/example-archive/dafny-tutorial/working/multiple_returns.c
index 6e419f0d..662cfc97 100644
--- a/src/example-archive/dafny-tutorial/working/multiple_returns.c
+++ b/src/example-archive/dafny-tutorial/working/multiple_returns.c
@@ -17,8 +17,8 @@ void multiple_returns(int x, int y, struct int_pair *ret)
       MINi32 <= (i64) x + (i64) y; 
       (i64) x + (i64) y <= MAXi32;
       MINi32 <= (i64) x - (i64) y; 
-      (i64) x - (i64) y <= MAXi32;  @*/
-/*@ ensures 
+      (i64) x - (i64) y <= MAXi32;
+    ensures 
       take PairPost = RW<struct int_pair>(ret);
       PairPost.fst == x + y;
       PairPost.snd == x - y; @*/
diff --git a/src/example-archive/should-fail/working/c_sequencing_race.c b/src/example-archive/should-fail/working/c_sequencing_race.c
index 0babc927..8b6a0b1f 100644
--- a/src/example-archive/should-fail/working/c_sequencing_race.c
+++ b/src/example-archive/should-fail/working/c_sequencing_race.c
@@ -2,9 +2,9 @@
 
 int
 f (int *x)
-/*@ requires take xv = RW(x); @*/
-/*@ requires 0i32 <= xv && xv < 500i32; @*/
-/*@ ensures take xv2 = RW(x); @*/
+/*@ requires take xv = RW(x);
+             0i32 <= xv && xv < 500i32;
+    ensures take xv2 = RW(x); @*/
 {
   return ((*x) + (*x));
 }
diff --git a/src/example-archive/simple-examples/working/add_1.c b/src/example-archive/simple-examples/working/add_1.c
index c62adc34..d774c53b 100644
--- a/src/example-archive/simple-examples/working/add_1.c
+++ b/src/example-archive/simple-examples/working/add_1.c
@@ -3,8 +3,8 @@
 // non-faulting.
 
 signed int add_1(signed int x, signed int y)
-/*@ requires x == 0i32; y == 0i32; @*/
-/*@ ensures return == x + y; @*/
+/*@ requires x == 0i32; y == 0i32;
+    ensures return == x + y; @*/
 {
   signed int i;
   i = x + y;
diff --git a/src/example-archive/simple-examples/working/add_2.c b/src/example-archive/simple-examples/working/add_2.c
index 10c84bf0..a0024aef 100644
--- a/src/example-archive/simple-examples/working/add_2.c
+++ b/src/example-archive/simple-examples/working/add_2.c
@@ -2,8 +2,8 @@
 // requires-clause sets one integer to be zero 
 
 signed int add_2(signed int x, signed int y)
-/*@ requires x == 0i32; @*/
-/*@ ensures return == y; @*/
+/*@ requires x == 0i32;
+    ensures return == y; @*/
 {
   signed int i;
   i = x + y;
diff --git a/src/example-archive/simple-examples/working/add_3.c b/src/example-archive/simple-examples/working/add_3.c
index 1d391f1f..f8dde358 100644
--- a/src/example-archive/simple-examples/working/add_3.c
+++ b/src/example-archive/simple-examples/working/add_3.c
@@ -6,8 +6,8 @@ signed int add_3(signed int x, signed int y)
       let MAXi32 = 2147483647i64; 
       let MINi32 = -2147483648i64;
       let sum = (i64) x + (i64) y;
-      MINi32 <= sum; sum <= MAXi32; @*/
-/*@ ensures return == x + y; @*/
+      MINi32 <= sum; sum <= MAXi32;
+    ensures return == x + y; @*/
 {
   signed int i;
   i = x + y;
diff --git a/src/example-archive/simple-examples/working/add_4.c b/src/example-archive/simple-examples/working/add_4.c
index 3f8ef0d7..841908d5 100644
--- a/src/example-archive/simple-examples/working/add_4.c
+++ b/src/example-archive/simple-examples/working/add_4.c
@@ -3,8 +3,8 @@
 signed int inc_1(signed int i)
 /*@ requires 
       let MAXi32 = 2147483647i64; 
-      (i64) i + 1i64 <  MAXi32; @*/
-/*@ ensures return == i + 1i32; @*/
+      (i64) i + 1i64 <  MAXi32;
+    ensures return == i + 1i32; @*/
 {
   i = i + 1;
   return i;
diff --git a/src/example-archive/simple-examples/working/add_5.c b/src/example-archive/simple-examples/working/add_5.c
index 0068cba1..e9bc1daf 100644
--- a/src/example-archive/simple-examples/working/add_5.c
+++ b/src/example-archive/simple-examples/working/add_5.c
@@ -4,8 +4,8 @@
 signed int add_5(signed int x, signed int y)
 /*@ requires 
       let sum = (i64) x + (i64) y;
-      (i64) MINi32() <= sum; sum <= (i64) MAXi32(); @*/
-/*@ ensures return == x + y; @*/
+      (i64) MINi32() <= sum; sum <= (i64) MAXi32();
+    ensures return == x + y; @*/
 {
   signed int i;
   i = x + y;
diff --git a/src/example-archive/simple-examples/working/add_uint_1.c b/src/example-archive/simple-examples/working/add_uint_1.c
index 0a716c17..73b0e0e0 100644
--- a/src/example-archive/simple-examples/working/add_uint_1.c
+++ b/src/example-archive/simple-examples/working/add_uint_1.c
@@ -4,8 +4,8 @@
 unsigned int add_uint_1(unsigned int x, unsigned int y)
 /*@ requires 
       let MAXi32 = 2147483647i64;
-      (i64) x + (i64) y <= MAXi32; @*/
-/*@ ensures return == x + y; @*/
+      (i64) x + (i64) y <= MAXi32;
+    ensures return == x + y; @*/
 {
   signed int i;
   i = x + y;
diff --git a/src/example-archive/simple-examples/working/array_1.c b/src/example-archive/simple-examples/working/array_1.c
index 2435926c..8788c081 100644
--- a/src/example-archive/simple-examples/working/array_1.c
+++ b/src/example-archive/simple-examples/working/array_1.c
@@ -4,8 +4,8 @@ void array_1(int *arr, int size, int off)
 /*@ requires 
       take arrayStart = each (i32 j; 0i32 <= j && j < size) {RW(arr + j)}; 
       0i32 <= off; 
-      off < size; @*/
-/*@ ensures take arrayEnd = each (i32 j; 0i32 <= j && j < size) {RW(arr + j)}; @*/
+      off < size;
+    ensures take arrayEnd = each (i32 j; 0i32 <= j && j < size) {RW(arr + j)}; @*/
 {
   int i = off;
   /*@ focus RW<int>, i; @*/  // <-- required to read / write
diff --git a/src/example-archive/simple-examples/working/array_2.c b/src/example-archive/simple-examples/working/array_2.c
index accb09e0..e4b27c3a 100644
--- a/src/example-archive/simple-examples/working/array_2.c
+++ b/src/example-archive/simple-examples/working/array_2.c
@@ -5,8 +5,8 @@ int array_2(int *arr, int size, int off)
       take arrayStart = each (i32 j; 0i32  <= j && j < size) {RW(arr + j)};
       0i32 <= off; 
       off < size; 
-      arrayStart[off] != 0i32; @*/
-/*@ ensures  
+      arrayStart[off] != 0i32;
+    ensures  
       take arrayEnd = each (i32 j; 0i32  <= j && j < size) {RW(arr + j)};
       arrayEnd[off] == 7i32; 
       return == arrayStart[off]; @*/
diff --git a/src/example-archive/simple-examples/working/array_3.c b/src/example-archive/simple-examples/working/array_3.c
index a45e9ba1..d8ffcf33 100644
--- a/src/example-archive/simple-examples/working/array_3.c
+++ b/src/example-archive/simple-examples/working/array_3.c
@@ -5,8 +5,8 @@
 void array_3(int *arr, int n)
 /*@ requires 
       0i32 < n;
-      take arrayStart = each (i32 j; 0i32 <= j && j < n) {RW<int>(arr + j)}; @*/
-/*@ ensures 
+      take arrayStart = each (i32 j; 0i32 <= j && j < n) {RW<int>(arr + j)};
+    ensures 
       take arrayEnd = each (i32 j; 0i32 <= j && j < n) {RW<int>(arr + j)};
       each (i32 j; 0i32 <= j && j < n) {arrayEnd[j] == 7i32}; @*/
 {
diff --git a/src/example-archive/simple-examples/working/assert_1.c b/src/example-archive/simple-examples/working/assert_1.c
index 42737070..dbadae88 100644
--- a/src/example-archive/simple-examples/working/assert_1.c
+++ b/src/example-archive/simple-examples/working/assert_1.c
@@ -3,8 +3,8 @@
 #include <assert.h>
 
 int assert_1(int x)
-/*@ requires x == 7i32; @*/
-/*@ ensures return == 0i32; @*/
+/*@ requires x == 7i32;
+    ensures return == 0i32; @*/
 {
   x = 0;
   assert(x == 0);
@@ -14,8 +14,8 @@ int assert_1(int x)
 // An alternative syntax for the same assertion: 
 
 int assert_1_alt(int x)
-/*@ requires x == 7i32; @*/
-/*@ ensures return == 0i32; @*/
+/*@ requires x == 7i32;
+    ensures return == 0i32; @*/
 {
   x = 0;
   /*@ assert(x == 0i32); @*/
diff --git a/src/example-archive/simple-examples/working/assert_2.c b/src/example-archive/simple-examples/working/assert_2.c
index 9c18097b..116b6051 100644
--- a/src/example-archive/simple-examples/working/assert_2.c
+++ b/src/example-archive/simple-examples/working/assert_2.c
@@ -4,8 +4,8 @@ void assert_2(int *x, int *y)
 /*@ requires 
       take Xpre = RW<int>(x); 
       take Ypre = RW<int>(y);
-      *x == 7i32; *y == 7i32; @*/
-/*@ ensures 
+      *x == 7i32; *y == 7i32;
+    ensures 
       take Xpost = RW<int>(x);
       take Ypost = RW<int>(y);
       *x == 0i32; *y == 0i32; @*/
diff --git a/src/example-archive/simple-examples/working/assert_3.c b/src/example-archive/simple-examples/working/assert_3.c
index 7e5c7b89..ebd9a385 100644
--- a/src/example-archive/simple-examples/working/assert_3.c
+++ b/src/example-archive/simple-examples/working/assert_3.c
@@ -14,8 +14,8 @@ void assert_3(int *x, int *y)
 /*@ requires 
       take Xpre = RW<int>(x); 
       take Ypre = RW<int>(y);
-      *x == 7i32; *y == 7i32; @*/
-/*@ ensures 
+      *x == 7i32; *y == 7i32;
+    ensures 
       take Xpost = RW<int>(x);
       take Ypost = RW<int>(y);
       *x == 0i32; *y == 0i32; @*/
diff --git a/src/example-archive/simple-examples/working/cast_4.c b/src/example-archive/simple-examples/working/cast_4.c
index e94c051f..9667fe97 100644
--- a/src/example-archive/simple-examples/working/cast_4.c
+++ b/src/example-archive/simple-examples/working/cast_4.c
@@ -5,8 +5,8 @@
 #define OFFSET 374328
 
 int cast_4(int *ptr_original)
-/*@ requires take Pre = W<int>(ptr_original); @*/
-/*@ ensures take Post = RW<int>(ptr_original);
+/*@ requires take Pre = W<int>(ptr_original);
+    ensures take Post = RW<int>(ptr_original);
             return == 7i32; @*/
 {
   *ptr_original = 7;
diff --git a/src/example-archive/simple-examples/working/cn_function_1.c b/src/example-archive/simple-examples/working/cn_function_1.c
index 2a8c5ad2..dd1250b7 100644
--- a/src/example-archive/simple-examples/working/cn_function_1.c
+++ b/src/example-archive/simple-examples/working/cn_function_1.c
@@ -9,8 +9,8 @@ function (i32) bw_or(i32 x, i32 y)
 // Define bitwise-OR in code
 int c_bw_or(int x, int y)
 // Lift the bitwise-OR function to a specification function 
-/*@ cn_function bw_or; @*/
-/*@ ensures return == bw_or(x,y); @*/  // <-- Trivial, should hold by construction 
+/*@ cn_function bw_or;
+    ensures return == bw_or(x,y); @*/  // <-- Trivial, should hold by construction 
 {
   return x | y;
 }
diff --git a/src/example-archive/simple-examples/working/cn_function_2.c b/src/example-archive/simple-examples/working/cn_function_2.c
index bd36b55b..76c73c67 100644
--- a/src/example-archive/simple-examples/working/cn_function_2.c
+++ b/src/example-archive/simple-examples/working/cn_function_2.c
@@ -8,8 +8,8 @@ function (i32) bw_or_tern(i32 x, i32 y, i32 z)
 // Define bitwise-OR in code
 int c_bw_or_tern(int x, int y, int z)
 // Lift the bitwise-OR function to a specification function 
-/*@ cn_function bw_or_tern; @*/
-/*@ ensures return == bw_or_tern(x,y,z); @*/  // <-- Trivial, should hold by construction 
+/*@ cn_function bw_or_tern;
+    ensures return == bw_or_tern(x,y,z); @*/  // <-- Trivial, should hold by construction 
 {
   return x | (y | z);
 }
diff --git a/src/example-archive/simple-examples/working/dec_1.c b/src/example-archive/simple-examples/working/dec_1.c
index 1a1db352..b4a07231 100644
--- a/src/example-archive/simple-examples/working/dec_1.c
+++ b/src/example-archive/simple-examples/working/dec_1.c
@@ -1,8 +1,8 @@
 // Pre and post-read decrement 
 
 int dec_1_pre(int i) 
-/*@ requires i >= 1i32; @*/
-/*@ ensures return == i - 1i32; @*/
+/*@ requires i >= 1i32;
+    ensures return == i - 1i32; @*/
 { 
   int start, pre, post; 
   start = i; 
@@ -12,12 +12,12 @@ int dec_1_pre(int i)
 }
 
 int dec_1_post(int i) 
-/*@ requires i >= 1i32; @*/
-/*@ ensures return == i - 1i32; @*/
+/*@ requires i >= 1i32;
+    ensures return == i - 1i32; @*/
 { 
   int start, pre, post; 
   start = i; 
   pre = i--; 
   assert(pre == start);
   return i; 
-}
\ No newline at end of file
+}
diff --git a/src/example-archive/simple-examples/working/effect_1.c b/src/example-archive/simple-examples/working/effect_1.c
index 7528da5c..70012209 100644
--- a/src/example-archive/simple-examples/working/effect_1.c
+++ b/src/example-archive/simple-examples/working/effect_1.c
@@ -7,8 +7,8 @@ int g;
 void
 write_g_to_1()
 /*@ requires 
-        take Pre = W<int>(&g); @*/
-/*@ ensures 
+        take Pre = W<int>(&g);
+    ensures 
         take Post = RW<int>(&g); 
         Post == 1i32; @*/
 {
@@ -19,8 +19,8 @@ write_g_to_1()
 int
 effect_1()
 /*@ requires 
-      take Pre = W<int>(&g); @*/
-/*@ ensures 
+      take Pre = W<int>(&g);
+    ensures 
       take Post = RW<int>(&g); 
       return == 1i32; @*/
 {
@@ -31,4 +31,4 @@ effect_1()
   if(g)
     return 1;
   return 0; 
-} 
\ No newline at end of file
+} 
diff --git a/src/example-archive/simple-examples/working/free_1.c b/src/example-archive/simple-examples/working/free_1.c
index 9879d011..94f14b9a 100644
--- a/src/example-archive/simple-examples/working/free_1.c
+++ b/src/example-archive/simple-examples/working/free_1.c
@@ -4,15 +4,15 @@
 // only works on ints.
 
 void my_free_int(int *target)
-/*@ trusted; @*/
-/*@ requires take ToFree = RW<int>(target); @*/
+/*@ trusted;
+    requires take ToFree = RW<int>(target); @*/
 {}
 
 void free_1(int *x, int *y)
 /*@ requires 
       take Xpre = RW<int>(x); 
-      take Ypre = RW<int>(y); @*/
-/*@ ensures take Ypost = RW<int>(y); @*/
+      take Ypre = RW<int>(y);
+    ensures take Ypost = RW<int>(y); @*/
 {
   *x = 7;
   my_free_int(x);
diff --git a/src/example-archive/simple-examples/working/inc_1.c b/src/example-archive/simple-examples/working/inc_1.c
index 6706f9c0..2d52e8ed 100644
--- a/src/example-archive/simple-examples/working/inc_1.c
+++ b/src/example-archive/simple-examples/working/inc_1.c
@@ -2,8 +2,8 @@
 int inc_1_pre(int i) 
 /*@ requires 
       let MAXi32 = 2147483647i64; 
-      (i64) i + 1i64 <  MAXi32; @*/
-/*@ ensures return == i + 1i32; @*/
+      (i64) i + 1i64 <  MAXi32;
+    ensures return == i + 1i32; @*/
 { 
   int start, pre, post; 
   start = i; 
@@ -15,12 +15,12 @@ int inc_1_pre(int i)
 int inc_1_post(int i) 
 /*@ requires 
       let MAXi32 = 2147483647i64; 
-      (i64) i + 1i64 <  MAXi32; @*/
-/*@ ensures return == i + 1i32; @*/
+      (i64) i + 1i64 <  MAXi32;
+    ensures return == i + 1i32; @*/
 { 
   int start, pre, post; 
   start = i; 
   pre = i++; 
   assert(pre == start);
   return i; 
-}
\ No newline at end of file
+}
diff --git a/src/example-archive/simple-examples/working/list_1.c b/src/example-archive/simple-examples/working/list_1.c
index 13343a13..7ef17d6b 100644
--- a/src/example-archive/simple-examples/working/list_1.c
+++ b/src/example-archive/simple-examples/working/list_1.c
@@ -4,8 +4,8 @@
 #include "list_preds.h"
 
 struct list_node *list_1(struct list_node *xs)
-/*@ requires take Xs = IntListSeg(xs,NULL); @*/
-/*@ ensures 
+/*@ requires take Xs = IntListSeg(xs,NULL);
+    ensures 
       take Ys = IntListSeg(return,NULL); 
       Ys == Xs; @*/
 {
diff --git a/src/example-archive/simple-examples/working/list_2.c b/src/example-archive/simple-examples/working/list_2.c
index 07b1157d..8d8b003c 100644
--- a/src/example-archive/simple-examples/working/list_2.c
+++ b/src/example-archive/simple-examples/working/list_2.c
@@ -18,8 +18,8 @@ lemma IntListSeqSnoc(pointer p, pointer tail)
 @*/
 
 void list_2(struct list_node *head)
-/*@ requires take Xs = IntListSeg(head,NULL); @*/
-/*@ ensures take Ys = IntListSeg(head,NULL); @*/
+/*@ requires take Xs = IntListSeg(head,NULL);
+    ensures take Ys = IntListSeg(head,NULL); @*/
 {
   struct list_node *curr;
   curr = head;
diff --git a/src/example-archive/simple-examples/working/list_3.c b/src/example-archive/simple-examples/working/list_3.c
index 38a90f80..662b7973 100644
--- a/src/example-archive/simple-examples/working/list_3.c
+++ b/src/example-archive/simple-examples/working/list_3.c
@@ -30,8 +30,8 @@ lemma IntListSeqSnocVal(pointer p, pointer tail, i32 tval)
 
 
 void list_3(struct list_node *head)
-/*@ requires take Xs = IntListSeg(head,NULL); @*/
-/*@ ensures  take Ys = IntListSegVal(head,NULL,7i32); @*/
+/*@ requires take Xs = IntListSeg(head,NULL);
+    ensures  take Ys = IntListSegVal(head,NULL,7i32); @*/
 {
   struct list_node *curr;
   curr = head;
diff --git a/src/example-archive/simple-examples/working/list_4.c b/src/example-archive/simple-examples/working/list_4.c
index b9281bf4..3fadf76c 100644
--- a/src/example-archive/simple-examples/working/list_4.c
+++ b/src/example-archive/simple-examples/working/list_4.c
@@ -4,8 +4,8 @@
 #include "list_preds.h"
 
 struct list_node *list_reverse_1(struct list_node *head)
-/*@ requires take ListPre  = IntListSeg(head, NULL); @*/
-/*@ ensures  take ListPost = IntListSeg(return, NULL); @*/
+/*@ requires take ListPre  = IntListSeg(head, NULL);
+    ensures  take ListPost = IntListSeg(return, NULL); @*/
 {
   struct list_node *prev, *next, *curr;
   curr = head;
diff --git a/src/example-archive/simple-examples/working/loop_7.c b/src/example-archive/simple-examples/working/loop_7.c
index acacc085..5cc40f7a 100644
--- a/src/example-archive/simple-examples/working/loop_7.c
+++ b/src/example-archive/simple-examples/working/loop_7.c
@@ -3,8 +3,8 @@
 // that the value of `n` is unknown, which causes the proof to fail 
 
 int loop_7(int n)
-/*@ requires 0i32 < n; @*/
-/*@ ensures return == n; @*/
+/*@ requires 0i32 < n;
+    ensures return == n; @*/
 {
   int i = 0;
   while (i < n)
diff --git a/src/example-archive/simple-examples/working/malloc_1.c b/src/example-archive/simple-examples/working/malloc_1.c
index aa4fb8af..77c45068 100644
--- a/src/example-archive/simple-examples/working/malloc_1.c
+++ b/src/example-archive/simple-examples/working/malloc_1.c
@@ -4,8 +4,8 @@
 // function that only works on ints.
 
 int *my_malloc__int()
-/*@ trusted; @*/
-/*@ ensures take New = W<int>(return); @*/
+/*@ trusted;
+    ensures take New = W<int>(return); @*/
 {}
 
 int *malloc__1()
diff --git a/src/example-archive/simple-examples/working/power_1.c b/src/example-archive/simple-examples/working/power_1.c
index de643f34..cf84ca21 100644
--- a/src/example-archive/simple-examples/working/power_1.c
+++ b/src/example-archive/simple-examples/working/power_1.c
@@ -8,9 +8,9 @@
 //   2. the inductive case - power(2,y+1) == 2 * power_uf(2,y)
 
 void lemma_power_uf_def(int y)
-/*@ trusted; @*/
-/*@ requires y >= 0i32; @*/
-/*@ ensures 
+/*@ trusted;
+    requires y >= 0i32;
+    ensures 
       (power_uf(2i32,0i32)) == 1i32; 
       (power_uf(2i32,y+1i32)) == (2i32 * power_uf(2i32,y)); @*/
 {}
diff --git a/src/example-archive/simple-examples/working/pred_2.c b/src/example-archive/simple-examples/working/pred_2.c
index 27eaf079..aba7b5e5 100644
--- a/src/example-archive/simple-examples/working/pred_2.c
+++ b/src/example-archive/simple-examples/working/pred_2.c
@@ -21,8 +21,8 @@ function (i32) test_if_zero(i32 x) {
 void pred_2_var1(int *p) 
 /*@ requires 
       take PreP = RW<int>(p); 
-      PreP == 0i32; @*/
-/*@ ensures 
+      PreP == 0i32;
+    ensures 
       take TestP = TestMemoryEqZero_2_var1(p); 
       TestP == 1i32; @*/
 { 
@@ -49,8 +49,8 @@ predicate (i32) TestMemoryEqZero_2_Helper(pointer p, i32 x) {
 void pred_2_var2(int *p) 
 /*@ requires 
       take PreP = RW<int>(p); 
-      PreP == 0i32; @*/
-/*@ ensures 
+      PreP == 0i32;
+    ensures 
       take TestP = TestMemoryEqZero_2_var2(p); 
       TestP == 1i32; @*/
 { 
@@ -69,8 +69,8 @@ predicate (i32) TestMemoryEqZero_2_var3(pointer p) {
 void pred_2_var3(int *p) 
 /*@ requires 
       take PreP = RW<int>(p); 
-      PreP == 0i32; @*/
-/*@ ensures 
+      PreP == 0i32;
+    ensures 
       take TestP = TestMemoryEqZero_2_var3(p); 
       TestP == 1i32; @*/
 { 
diff --git a/src/example-archive/simple-examples/working/struct_1.c b/src/example-archive/simple-examples/working/struct_1.c
index 2465dd24..b16e4e2d 100644
--- a/src/example-archive/simple-examples/working/struct_1.c
+++ b/src/example-archive/simple-examples/working/struct_1.c
@@ -7,8 +7,8 @@ struct s
 };
 
 void struct_1(struct s *p)
-/*@ requires take StructPre  = RW<struct s>(p); @*/
-/*@ ensures  
+/*@ requires take StructPre  = RW<struct s>(p);
+    ensures  
       take StructPost = RW<struct s>(p);
       StructPre.x == StructPost.x;
       StructPost.y == 0i32; @*/
diff --git a/src/example-archive/simple-examples/working/swap_1.c b/src/example-archive/simple-examples/working/swap_1.c
index 483547f2..5c2607eb 100644
--- a/src/example-archive/simple-examples/working/swap_1.c
+++ b/src/example-archive/simple-examples/working/swap_1.c
@@ -3,8 +3,8 @@
 void swap_1(int *a, int *b)
 /*@ requires 
     take Pa = RW(a); 
-    take Pb = RW(b); @*/
-/*@ ensures 
+    take Pb = RW(b);
+    ensures 
     take Qa = RW(a);
     take Qb = RW(b);
     Qb == Pa;
diff --git a/src/example-archive/simple-examples/working/write_1.c b/src/example-archive/simple-examples/working/write_1.c
index bde260db..0024b2b7 100644
--- a/src/example-archive/simple-examples/working/write_1.c
+++ b/src/example-archive/simple-examples/working/write_1.c
@@ -1,8 +1,8 @@
 // Write into a memory cell
 
 void write_1(int *cell)
-/*@ requires take CellPre = RW<int>(cell); @*/
-/*@ ensures 
+/*@ requires take CellPre = RW<int>(cell);
+    ensures 
       take CellPost = RW<int>(cell);
       CellPost == 7i32; @*/
 {
diff --git a/src/example-archive/simple-examples/working/write_2.c b/src/example-archive/simple-examples/working/write_2.c
index abc798f5..c4b25573 100644
--- a/src/example-archive/simple-examples/working/write_2.c
+++ b/src/example-archive/simple-examples/working/write_2.c
@@ -2,8 +2,8 @@
 
 void write_2(int *cell1, int *cell2)
 /*@ requires take Cell1Pre = RW<int>(cell1);
-             take Cell2Pre = RW<int>(cell2); @*/
-/*@ ensures take Cell1Post = RW<int>(cell1);
+             take Cell2Pre = RW<int>(cell2);
+    ensures take Cell1Post = RW<int>(cell1);
             take Cell2Post = RW<int>(cell2);
             Cell1Post == 7i32; Cell2Post == 8i32; @*/
 {
diff --git a/src/example-archive/simple-examples/working/write_3.c b/src/example-archive/simple-examples/working/write_3.c
index 342c7d39..15572577 100644
--- a/src/example-archive/simple-examples/working/write_3.c
+++ b/src/example-archive/simple-examples/working/write_3.c
@@ -3,8 +3,8 @@
 void write_3(int *cell1, int *cell2)
 /*@ requires 
       take Cell1Pre = RW<int>(cell1);
-      cell1 == cell2; @*/
-/*@ ensures 
+      cell1 == cell2;
+    ensures 
       take Cell2Post = RW<int>(cell2);
       Cell2Post == 8i32; @*/
 {
diff --git a/src/example-archive/simple-examples/working/write_5.c b/src/example-archive/simple-examples/working/write_5.c
index 07d4e634..9b27c5ff 100644
--- a/src/example-archive/simple-examples/working/write_5.c
+++ b/src/example-archive/simple-examples/working/write_5.c
@@ -3,8 +3,8 @@
 void write_5(int *pair)
 /*@ requires 
       take Cell1Pre = RW(pair);
-      take Cell2Pre = RW(pair + 1i32); @*/
-/*@ ensures 
+      take Cell2Pre = RW(pair + 1i32);
+    ensures 
       take Cell1Post = RW(pair);
       take Cell2Post = RW(pair + 1i32); 
       Cell1Post == 7i32; 
@@ -18,8 +18,8 @@ void write_5(int *pair)
 
 void write_5_alt(int *pair)
 /*@ requires 
-      take PairPre = each (i32 j; j == 0i32 || j == 1i32) {RW(pair + j)}; @*/
-/*@ ensures 
+      take PairPre = each (i32 j; j == 0i32 || j == 1i32) {RW(pair + j)};
+    ensures 
       take PairPost = each (i32 j; j == 0i32 || j == 1i32) {RW(pair + j)}; 
       PairPost[0i32] == 7i32; 
       PairPost[1i32] == 8i32; 
diff --git a/src/exercises/dllist/predicates.h b/src/exercises/dllist/predicates.h
index e8aaaff2..8793a88e 100644
--- a/src/exercises/dllist/predicates.h
+++ b/src/exercises/dllist/predicates.h
@@ -1,16 +1,5 @@
 /*@
-predicate (datatype DlList) DlList_at (pointer p) {
-    if (is_null(p)) {
-        return Empty_DlList{};
-    } else {
-        take n = RW<struct dllist>(p);
-        take L = Take_Left(n.prev, p, n);
-        take R = Take_Right(n.next, p, n);
-        return Nonempty_DlList{left: L, curr: n, right: R};
-    }
-}
-
-predicate (datatype List) Take_Right (pointer p, 
+predicate [rec] (datatype List) Take_Right (pointer p, 
                                         pointer prev_pointer, 
                                         struct dllist prev_dllist) {
     if (is_null(p)) {
@@ -24,7 +13,7 @@ predicate (datatype List) Take_Right (pointer p,
     }
 }
 
-predicate (datatype List) Take_Left (pointer p, 
+predicate [rec] (datatype List) Take_Left (pointer p, 
                                          pointer next_pointer, 
                                          struct dllist next_dllist) {
     if (is_null(p)) {
@@ -37,4 +26,17 @@ predicate (datatype List) Take_Left (pointer p,
         return Cons{Head: P.data, Tail: T};
     }
 }
+
+
+predicate (datatype DlList) DlList_at (pointer p) {
+    if (is_null(p)) {
+        return Empty_DlList{};
+    } else {
+        take n = RW<struct dllist>(p);
+        take L = Take_Left(n.prev, p, n);
+        take R = Take_Right(n.next, p, n);
+        return Nonempty_DlList{left: L, curr: n, right: R};
+    }
+}
+
 @*/
diff --git a/src/exercises/list/cn_types.h b/src/exercises/list/cn_types.h
index b4be8911..e294c6eb 100644
--- a/src/exercises/list/cn_types.h
+++ b/src/exercises/list/cn_types.h
@@ -4,7 +4,7 @@ datatype List {
   Cons {i32 Head, datatype List Tail}
 }
 
-predicate (datatype List) SLList_At(pointer p) {
+predicate [rec] (datatype List) SLList_At(pointer p) {
   if (is_null(p)) {
     return Nil{};
   } else {
diff --git a/src/exercises/queue/cn_types_3.test.h b/src/exercises/queue/cn_types_3.test.h
index 59455ee9..2d3056de 100644
--- a/src/exercises/queue/cn_types_3.test.h
+++ b/src/exercises/queue/cn_types_3.test.h
@@ -1,5 +1,5 @@
 /*@
-predicate (datatype List) QueueAux (pointer f, pointer b) {
+predicate [rec] (datatype List) QueueAux (pointer f, pointer b) {
   if (ptr_eq(f,b)) {
     return Nil{};
   } else {
diff --git a/src/exercises/queue/cn_types_3.verif.h b/src/exercises/queue/cn_types_3.verif.h
index 59455ee9..2d3056de 100644
--- a/src/exercises/queue/cn_types_3.verif.h
+++ b/src/exercises/queue/cn_types_3.verif.h
@@ -1,5 +1,5 @@
 /*@
-predicate (datatype List) QueueAux (pointer f, pointer b) {
+predicate [rec] (datatype List) QueueAux (pointer f, pointer b) {
   if (ptr_eq(f,b)) {
     return Nil{};
   } else {
diff --git a/src/underconstruction/bst/cn_types.h b/src/underconstruction/bst/cn_types.h
index 979f8566..d56fe354 100644
--- a/src/underconstruction/bst/cn_types.h
+++ b/src/underconstruction/bst/cn_types.h
@@ -7,7 +7,7 @@ datatype Tree {
     Node {datatype Tree Left, i32 Data, datatype Tree Right}
 } 
 
-predicate (datatype Tree) Tree_At (pointer t) 
+predicate [rec] (datatype Tree) Tree_At (pointer t) 
 {
     if (is_null(t))
     {