1 files changed, 20 insertions, 18 deletions
diff --git a/Test/aitest0/Answer b/Test/aitest0/Answer
index 58750460..e517aa18 100644
--- a/Test/aitest0/Answer
+++ b/Test/aitest0/Answer
@@ -18,34 +18,34 @@ implementation Join(b: bool)
   var z: int;
 
   start:
-    assume true;
+    assume {:inferred} true;
     GlobalFlag := true;
     x := 3;
     y := 4;
     z := x + y;
-    assume x == 3 && y == 4 && z == 7;
+    assume {:inferred} x == 3 && y == 4 && z == 7;
     goto Then, Else;
 
   Then:
-    assume x == 3 && y == 4 && z == 7;
+    assume {:inferred} x == 3 && y == 4 && z == 7;
     assume b <==> true;
     x := x + 1;
-    assume x == 4 && y == 4 && z == 7;
+    assume {:inferred} x == 4 && y == 4 && z == 7;
     goto join;
 
   Else:
-    assume x == 3 && y == 4 && z == 7;
+    assume {:inferred} x == 3 && y == 4 && z == 7;
     assume b <==> false;
     y := 4;
-    assume x == 3 && y == 4 && z == 7;
+    assume {:inferred} x == 3 && y == 4 && z == 7;
     goto join;
 
   join:
-    assume y == 4 && z == 7;
+    assume {:inferred} y == 4 && z == 7;
     assert y == 4;
     assert z == 7;
     assert GlobalFlag <==> true;
-    assume y == 4 && z == 7;
+    assume {:inferred} y == 4 && z == 7;
     return;
 }
 
@@ -61,27 +61,27 @@ implementation Loop()
   var i: int;
 
   start:
-    assume true;
+    assume {:inferred} true;
     c := 0;
     i := 0;
-    assume c == 0 && i == 0;
+    assume {:inferred} c == 0 && i == 0;
     goto test;
 
   test:  // cut point
-    assume c == 0;
-    assume c == 0;
+    assume {:inferred} c == 0;
+    assume {:inferred} c == 0;
     goto Then, Else;
 
   Then:
-    assume c == 0;
+    assume {:inferred} c == 0;
     assume i < 10;
     i := i + 1;
-    assume c == 0;
+    assume {:inferred} c == 0;
     goto test;
 
   Else:
-    assume c == 0;
-    assume c == 0;
+    assume {:inferred} c == 0;
+    assume {:inferred} c == 0;
     return;
 }
 
@@ -96,16 +96,18 @@ implementation Evaluate()
   var i: int;
 
   start:
-    assume true;
+    assume {:inferred} true;
     i := 5;
     i := 3 * i + 1;
     i := 3 * (i + 1);
     i := 1 + 3 * i;
     i := (i + 1) * 3;
-    assume i == 465;
+    assume {:inferred} i == 465;
     return;
 }
 
 
 
 Boogie program verifier finished with 0 verified, 0 errors
+
+Boogie program verifier finished with 1 verified, 0 errors