1 files changed, 44 insertions, 44 deletions
diff --git a/Test/aitest0/Answer b/Test/aitest0/Answer
index cc518d1b..1d19f568 100644
--- a/Test/aitest0/Answer
+++ b/Test/aitest0/Answer
@@ -109,60 +109,60 @@ implementation Evaluate()
 
 
 Boogie program verifier finished with 0 verified, 0 errors
-Intervals.bpl(62,3): Error BP5001: This assertion might not hold.
+Intervals.bpl(64,3): Error BP5001: This assertion might not hold.
 Execution trace:
-    Intervals.bpl(57,5): anon0
-    Intervals.bpl(58,3): anon3_LoopHead
-    Intervals.bpl(58,3): anon3_LoopDone
-Intervals.bpl(73,3): Error BP5001: This assertion might not hold.
+    Intervals.bpl(59,5): anon0
+    Intervals.bpl(60,3): anon3_LoopHead
+    Intervals.bpl(60,3): anon3_LoopDone
+Intervals.bpl(75,3): Error BP5001: This assertion might not hold.
 Execution trace:
-    Intervals.bpl(68,5): anon0
-    Intervals.bpl(69,3): anon3_LoopHead
-    Intervals.bpl(69,3): anon3_LoopDone
-Intervals.bpl(92,3): Error BP5001: This assertion might not hold.
+    Intervals.bpl(70,5): anon0
+    Intervals.bpl(71,3): anon3_LoopHead
+    Intervals.bpl(71,3): anon3_LoopDone
+Intervals.bpl(94,3): Error BP5001: This assertion might not hold.
 Execution trace:
-    Intervals.bpl(87,5): anon0
-    Intervals.bpl(88,3): loop_head
-    Intervals.bpl(91,3): after_loop
-Intervals.bpl(138,3): Error BP5001: This assertion might not hold.
+    Intervals.bpl(89,5): anon0
+    Intervals.bpl(90,3): loop_head
+    Intervals.bpl(93,3): after_loop
+Intervals.bpl(140,3): Error BP5001: This assertion might not hold.
 Execution trace:
-    Intervals.bpl(133,5): anon0
-    Intervals.bpl(134,3): anon3_LoopHead
-    Intervals.bpl(134,3): anon3_LoopDone
-Intervals.bpl(149,3): Error BP5001: This assertion might not hold.
+    Intervals.bpl(135,5): anon0
+    Intervals.bpl(136,3): anon3_LoopHead
+    Intervals.bpl(136,3): anon3_LoopDone
+Intervals.bpl(151,3): Error BP5001: This assertion might not hold.
 Execution trace:
-    Intervals.bpl(144,5): anon0
-    Intervals.bpl(145,3): anon3_LoopHead
-    Intervals.bpl(145,3): anon3_LoopDone
-Intervals.bpl(200,3): Error BP5001: This assertion might not hold.
+    Intervals.bpl(146,5): anon0
+    Intervals.bpl(147,3): anon3_LoopHead
+    Intervals.bpl(147,3): anon3_LoopDone
+Intervals.bpl(202,3): Error BP5001: This assertion might not hold.
 Execution trace:
-    Intervals.bpl(190,8): anon0
-    Intervals.bpl(191,3): anon4_LoopHead
-    Intervals.bpl(191,3): anon4_LoopDone
-Intervals.bpl(238,3): Error BP5001: This assertion might not hold.
+    Intervals.bpl(192,8): anon0
+    Intervals.bpl(193,3): anon4_LoopHead
+    Intervals.bpl(193,3): anon4_LoopDone
+Intervals.bpl(240,3): Error BP5001: This assertion might not hold.
 Execution trace:
-    Intervals.bpl(233,5): anon0
-    Intervals.bpl(234,3): anon3_LoopHead
-    Intervals.bpl(234,3): anon3_LoopDone
-Intervals.bpl(250,3): Error BP5001: This assertion might not hold.
+    Intervals.bpl(235,5): anon0
+    Intervals.bpl(236,3): anon3_LoopHead
+    Intervals.bpl(236,3): anon3_LoopDone
+Intervals.bpl(252,3): Error BP5001: This assertion might not hold.
 Execution trace:
-    Intervals.bpl(244,8): anon0
-    Intervals.bpl(245,3): anon3_LoopHead
-    Intervals.bpl(245,3): anon3_LoopDone
-Intervals.bpl(261,3): Error BP5001: This assertion might not hold.
+    Intervals.bpl(246,8): anon0
+    Intervals.bpl(247,3): anon3_LoopHead
+    Intervals.bpl(247,3): anon3_LoopDone
+Intervals.bpl(263,3): Error BP5001: This assertion might not hold.
 Execution trace:
-    Intervals.bpl(256,5): anon0
-    Intervals.bpl(257,3): anon3_LoopHead
-    Intervals.bpl(257,3): anon3_LoopDone
-Intervals.bpl(283,3): Error BP5001: This assertion might not hold.
+    Intervals.bpl(258,5): anon0
+    Intervals.bpl(259,3): anon3_LoopHead
+    Intervals.bpl(259,3): anon3_LoopDone
+Intervals.bpl(285,3): Error BP5001: This assertion might not hold.
 Execution trace:
-    Intervals.bpl(278,5): anon0
-    Intervals.bpl(279,3): anon3_LoopHead
-    Intervals.bpl(279,3): anon3_LoopDone
-Intervals.bpl(305,3): Error BP5001: This assertion might not hold.
+    Intervals.bpl(280,5): anon0
+    Intervals.bpl(281,3): anon3_LoopHead
+    Intervals.bpl(281,3): anon3_LoopDone
+Intervals.bpl(307,3): Error BP5001: This assertion might not hold.
 Execution trace:
-    Intervals.bpl(300,5): anon0
-    Intervals.bpl(301,3): anon3_LoopHead
-    Intervals.bpl(301,3): anon3_LoopDone
+    Intervals.bpl(302,5): anon0
+    Intervals.bpl(303,3): anon3_LoopHead
+    Intervals.bpl(303,3): anon3_LoopDone
 
 Boogie program verifier finished with 16 verified, 11 errors