1 files changed, 259 insertions, 259 deletions
diff --git a/Test/z3api/Answer b/Test/z3api/Answer
index d18f12ef..6fa628b0 100644
--- a/Test/z3api/Answer
+++ b/Test/z3api/Answer
@@ -1,259 +1,259 @@
-
--------------------- boog0.bpl --------------------
-boog0.bpl(49,1): Error BP5003: A postcondition might not hold on this return path.
-boog0.bpl(43,3): Related location: This is the postcondition that might not hold.
-Execution trace:
-    boog0.bpl(46,7): anon0
-
-Boogie program verifier finished with 1 verified, 1 error
-
--------------------- boog1.bpl --------------------
-
-Boogie program verifier finished with 1 verified, 0 errors
-
--------------------- boog2.bpl --------------------
-boog2.bpl(24,1): Error BP5003: A postcondition might not hold on this return path.
-boog2.bpl(20,3): Related location: This is the postcondition that might not hold.
-Execution trace:
-    boog2.bpl(23,8): anon0
-
-Boogie program verifier finished with 1 verified, 1 error
-
--------------------- boog3.bpl --------------------
-boog3.bpl(7,3): Error BP5001: This assertion might not hold.
-Execution trace:
-    boog3.bpl(7,3): anon0
-
-Boogie program verifier finished with 0 verified, 1 error
-
--------------------- boog4.bpl --------------------
-
-Boogie program verifier finished with 1 verified, 0 errors
-
--------------------- boog5.bpl --------------------
-boog5.bpl(37,3): Error BP5003: A postcondition might not hold on this return path.
-boog5.bpl(30,3): Related location: This is the postcondition that might not hold.
-Execution trace:
-    boog5.bpl(33,3): anon0
-    boog5.bpl(36,13): anon3_Else
-
-Boogie program verifier finished with 0 verified, 1 error
-
--------------------- boog6.bpl --------------------
-
-Boogie program verifier finished with 1 verified, 0 errors
-
--------------------- boog7.bpl --------------------
-boog7.bpl(18,1): Error BP5003: A postcondition might not hold on this return path.
-boog7.bpl(14,3): Related location: This is the postcondition that might not hold.
-Execution trace:
-    boog7.bpl(17,11): anon0
-
-Boogie program verifier finished with 0 verified, 1 error
-
--------------------- boog8.bpl --------------------
-boog8.bpl(23,1): Error BP5003: A postcondition might not hold on this return path.
-boog8.bpl(19,3): Related location: This is the postcondition that might not hold.
-Execution trace:
-    boog8.bpl(22,11): anon0
-
-Boogie program verifier finished with 0 verified, 1 error
-
--------------------- boog9.bpl --------------------
-boog9.bpl(20,1): Error BP5003: A postcondition might not hold on this return path.
-boog9.bpl(16,3): Related location: This is the postcondition that might not hold.
-Execution trace:
-    boog9.bpl(19,11): anon0
-
-Boogie program verifier finished with 0 verified, 1 error
-
--------------------- boog10.bpl --------------------
-boog10.bpl(19,3): Error BP5001: This assertion might not hold.
-Execution trace:
-    boog10.bpl(19,3): anon0
-
-Boogie program verifier finished with 0 verified, 1 error
-
--------------------- boog11.bpl --------------------
-boog11.bpl(15,1): Error BP5003: A postcondition might not hold on this return path.
-boog11.bpl(11,3): Related location: This is the postcondition that might not hold.
-Execution trace:
-    boog11.bpl(14,8): anon0
-
-Boogie program verifier finished with 0 verified, 1 error
-
--------------------- boog12.bpl --------------------
-boog12.bpl(19,1): Error BP5003: A postcondition might not hold on this return path.
-boog12.bpl(14,3): Related location: This is the postcondition that might not hold.
-Execution trace:
-    boog12.bpl(17,16): anon0
-
-Boogie program verifier finished with 0 verified, 1 error
-
--------------------- boog13.bpl --------------------
-boog13.bpl(10,18): Error: more than one declaration of variable name: v
-1 name resolution errors detected in boog13.bpl
-
--------------------- boog14.bpl --------------------
-boog14.bpl(12,1): Error BP5003: A postcondition might not hold on this return path.
-boog14.bpl(9,1): Related location: This is the postcondition that might not hold.
-Execution trace:
-    boog14.bpl(11,8): anon0
-
-Boogie program verifier finished with 0 verified, 1 error
-
--------------------- boog15.bpl --------------------
-boog15.bpl(11,1): Error BP5003: A postcondition might not hold on this return path.
-boog15.bpl(8,1): Related location: This is the postcondition that might not hold.
-Execution trace:
-    boog15.bpl(10,8): anon0
-
-Boogie program verifier finished with 0 verified, 1 error
-
--------------------- boog16.bpl --------------------
-boog16.bpl(12,1): Error BP5003: A postcondition might not hold on this return path.
-boog16.bpl(9,1): Related location: This is the postcondition that might not hold.
-Execution trace:
-    boog16.bpl(11,8): anon0
-
-Boogie program verifier finished with 0 verified, 1 error
-
--------------------- boog17.bpl --------------------
-boog17.bpl(26,3): Error BP5001: This assertion might not hold.
-Execution trace:
-    boog17.bpl(17,1): start
-
-Boogie program verifier finished with 0 verified, 1 error
-
--------------------- boog18.bpl --------------------
-boog18.bpl(16,1): Error BP5003: A postcondition might not hold on this return path.
-boog18.bpl(13,1): Related location: This is the postcondition that might not hold.
-Execution trace:
-    boog18.bpl(15,4): anon0
-
-Boogie program verifier finished with 0 verified, 1 error
-
--------------------- boog19.bpl --------------------
-
-Boogie program verifier finished with 1 verified, 0 errors
-
--------------------- boog20.bpl --------------------
-boog20.bpl(16,1): Error BP5001: This assertion might not hold.
-Execution trace:
-    boog20.bpl(16,1): anon0
-
-Boogie program verifier finished with 0 verified, 1 error
-
--------------------- boog21.bpl --------------------
-
-Boogie program verifier finished with 1 verified, 0 errors
-
--------------------- boog22.bpl --------------------
-boog22.bpl(5,9): Error: more than one declaration of function/procedure name: f1
-1 name resolution errors detected in boog22.bpl
-
--------------------- boog23.bpl --------------------
-
-Boogie program verifier finished with 1 verified, 0 errors
-
--------------------- boog24.bpl --------------------
-
-Boogie program verifier finished with 1 verified, 0 errors
-
--------------------- boog25.bpl --------------------
-
-Boogie program verifier finished with 1 verified, 0 errors
-
--------------------- boog28.bpl --------------------
-
-Boogie program verifier finished with 1 verified, 0 errors
-
--------------------- boog29.bpl --------------------
-
-Boogie program verifier finished with 1 verified, 0 errors
-
--------------------- boog30.bpl --------------------
-
-Boogie program verifier finished with 1 verified, 0 errors
-
--------------------- boog31.bpl --------------------
-boog31.bpl(13,1): Error BP5001: This assertion might not hold.
-Execution trace:
-    boog31.bpl(13,1): anon0
-
-Boogie program verifier finished with 0 verified, 1 error
-
--------------------- boog34.bpl --------------------
-
-Boogie program verifier finished with 1 verified, 0 errors
-
--------------------- boog35.bpl --------------------
-boog35.bpl(16,3): Error BP5001: This assertion might not hold.
-Execution trace:
-    boog35.bpl(14,11): anon0
-
-Boogie program verifier finished with 1 verified, 1 error
-
--------------------- bar1.bpl --------------------
-bar1.bpl(25,1): Error BP5003: A postcondition might not hold on this return path.
-bar1.bpl(21,1): Related location: This is the postcondition that might not hold.
-Execution trace:
-    bar1.bpl(24,3): anon0
-    Inlined call to procedure foo begins
-        bar1.bpl(13,5): anon0
-        Inlined call to procedure bar begins
-            bar1.bpl(7,5): anon0
-        Inlined call to procedure bar ends
-        Inlined call to procedure bar begins
-            bar1.bpl(7,5): anon0
-        Inlined call to procedure bar ends
-    Inlined call to procedure foo ends
-
-Boogie program verifier finished with 0 verified, 1 error
-
--------------------- bar2.bpl --------------------
-bar2.bpl(21,3): Error BP5001: This assertion might not hold.
-Execution trace:
-    bar2.bpl(19,3): anon0
-    Inlined call to procedure foo begins
-        bar2.bpl(5,3): anon0
-        bar2.bpl(9,7): anon3_Else
-    Inlined call to procedure foo ends
-    Inlined call to procedure foo begins
-        bar2.bpl(5,3): anon0
-        bar2.bpl(6,7): anon3_Then
-    Inlined call to procedure foo ends
-
-Boogie program verifier finished with 0 verified, 1 error
-
--------------------- bar3.bpl --------------------
-bar3.bpl(41,1): Error BP5003: A postcondition might not hold on this return path.
-bar3.bpl(34,1): Related location: This is the postcondition that might not hold.
-Execution trace:
-    bar3.bpl(38,3): anon0
-    Inlined call to procedure foo begins
-        bar3.bpl(18,3): anon0
-        bar3.bpl(24,7): anon3_Else
-        Inlined call to procedure bar begins
-            bar3.bpl(7,3): anon0
-            bar3.bpl(10,7): anon3_Else
-        Inlined call to procedure bar ends
-        Inlined call to procedure bar begins
-            bar3.bpl(7,3): anon0
-            bar3.bpl(10,7): anon3_Else
-        Inlined call to procedure bar ends
-    Inlined call to procedure foo ends
-    Inlined call to procedure bar begins
-        bar3.bpl(7,3): anon0
-        bar3.bpl(10,7): anon3_Else
-    Inlined call to procedure bar ends
-
-Boogie program verifier finished with 0 verified, 1 error
-
--------------------- bar4.bpl --------------------
-
-Boogie program verifier finished with 1 verified, 0 errors
-
--------------------- bar6.bpl --------------------
-
-Boogie program verifier finished with 1 verified, 0 errors
+
+-------------------- boog0.bpl --------------------
+boog0.bpl(49,1): Error BP5003: A postcondition might not hold on this return path.
+boog0.bpl(43,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+    boog0.bpl(46,7): anon0
+
+Boogie program verifier finished with 1 verified, 1 error
+
+-------------------- boog1.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+-------------------- boog2.bpl --------------------
+boog2.bpl(24,1): Error BP5003: A postcondition might not hold on this return path.
+boog2.bpl(20,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+    boog2.bpl(23,8): anon0
+
+Boogie program verifier finished with 1 verified, 1 error
+
+-------------------- boog3.bpl --------------------
+boog3.bpl(7,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    boog3.bpl(7,3): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- boog4.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+-------------------- boog5.bpl --------------------
+boog5.bpl(37,3): Error BP5003: A postcondition might not hold on this return path.
+boog5.bpl(30,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+    boog5.bpl(33,3): anon0
+    boog5.bpl(36,13): anon3_Else
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- boog6.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+-------------------- boog7.bpl --------------------
+boog7.bpl(18,1): Error BP5003: A postcondition might not hold on this return path.
+boog7.bpl(14,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+    boog7.bpl(17,11): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- boog8.bpl --------------------
+boog8.bpl(23,1): Error BP5003: A postcondition might not hold on this return path.
+boog8.bpl(19,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+    boog8.bpl(22,11): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- boog9.bpl --------------------
+boog9.bpl(20,1): Error BP5003: A postcondition might not hold on this return path.
+boog9.bpl(16,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+    boog9.bpl(19,11): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- boog10.bpl --------------------
+boog10.bpl(19,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    boog10.bpl(19,3): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- boog11.bpl --------------------
+boog11.bpl(15,1): Error BP5003: A postcondition might not hold on this return path.
+boog11.bpl(11,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+    boog11.bpl(14,8): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- boog12.bpl --------------------
+boog12.bpl(19,1): Error BP5003: A postcondition might not hold on this return path.
+boog12.bpl(14,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+    boog12.bpl(17,16): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- boog13.bpl --------------------
+boog13.bpl(10,18): Error: more than one declaration of variable name: v
+1 name resolution errors detected in boog13.bpl
+
+-------------------- boog14.bpl --------------------
+boog14.bpl(12,1): Error BP5003: A postcondition might not hold on this return path.
+boog14.bpl(9,1): Related location: This is the postcondition that might not hold.
+Execution trace:
+    boog14.bpl(11,8): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- boog15.bpl --------------------
+boog15.bpl(11,1): Error BP5003: A postcondition might not hold on this return path.
+boog15.bpl(8,1): Related location: This is the postcondition that might not hold.
+Execution trace:
+    boog15.bpl(10,8): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- boog16.bpl --------------------
+boog16.bpl(12,1): Error BP5003: A postcondition might not hold on this return path.
+boog16.bpl(9,1): Related location: This is the postcondition that might not hold.
+Execution trace:
+    boog16.bpl(11,8): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- boog17.bpl --------------------
+boog17.bpl(26,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    boog17.bpl(17,1): start
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- boog18.bpl --------------------
+boog18.bpl(16,1): Error BP5003: A postcondition might not hold on this return path.
+boog18.bpl(13,1): Related location: This is the postcondition that might not hold.
+Execution trace:
+    boog18.bpl(15,4): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- boog19.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+-------------------- boog20.bpl --------------------
+boog20.bpl(16,1): Error BP5001: This assertion might not hold.
+Execution trace:
+    boog20.bpl(16,1): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- boog21.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+-------------------- boog22.bpl --------------------
+boog22.bpl(5,9): Error: more than one declaration of function/procedure name: f1
+1 name resolution errors detected in boog22.bpl
+
+-------------------- boog23.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+-------------------- boog24.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+-------------------- boog25.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+-------------------- boog28.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+-------------------- boog29.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+-------------------- boog30.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+-------------------- boog31.bpl --------------------
+boog31.bpl(13,1): Error BP5001: This assertion might not hold.
+Execution trace:
+    boog31.bpl(13,1): anon0
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- boog34.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+-------------------- boog35.bpl --------------------
+boog35.bpl(16,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    boog35.bpl(14,11): anon0
+
+Boogie program verifier finished with 1 verified, 1 error
+
+-------------------- bar1.bpl --------------------
+bar1.bpl(25,1): Error BP5003: A postcondition might not hold on this return path.
+bar1.bpl(21,1): Related location: This is the postcondition that might not hold.
+Execution trace:
+    bar1.bpl(24,3): anon0
+    Inlined call to procedure foo begins
+        bar1.bpl(13,5): anon0
+        Inlined call to procedure bar begins
+            bar1.bpl(7,5): anon0
+        Inlined call to procedure bar ends
+        Inlined call to procedure bar begins
+            bar1.bpl(7,5): anon0
+        Inlined call to procedure bar ends
+    Inlined call to procedure foo ends
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- bar2.bpl --------------------
+bar2.bpl(21,3): Error BP5001: This assertion might not hold.
+Execution trace:
+    bar2.bpl(19,3): anon0
+    Inlined call to procedure foo begins
+        bar2.bpl(5,3): anon0
+        bar2.bpl(9,7): anon3_Else
+    Inlined call to procedure foo ends
+    Inlined call to procedure foo begins
+        bar2.bpl(5,3): anon0
+        bar2.bpl(6,7): anon3_Then
+    Inlined call to procedure foo ends
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- bar3.bpl --------------------
+bar3.bpl(41,1): Error BP5003: A postcondition might not hold on this return path.
+bar3.bpl(34,1): Related location: This is the postcondition that might not hold.
+Execution trace:
+    bar3.bpl(38,3): anon0
+    Inlined call to procedure foo begins
+        bar3.bpl(18,3): anon0
+        bar3.bpl(24,7): anon3_Else
+        Inlined call to procedure bar begins
+            bar3.bpl(7,3): anon0
+            bar3.bpl(10,7): anon3_Else
+        Inlined call to procedure bar ends
+        Inlined call to procedure bar begins
+            bar3.bpl(7,3): anon0
+            bar3.bpl(10,7): anon3_Else
+        Inlined call to procedure bar ends
+    Inlined call to procedure foo ends
+    Inlined call to procedure bar begins
+        bar3.bpl(7,3): anon0
+        bar3.bpl(10,7): anon3_Else
+    Inlined call to procedure bar ends
+
+Boogie program verifier finished with 0 verified, 1 error
+
+-------------------- bar4.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
+
+-------------------- bar6.bpl --------------------
+
+Boogie program verifier finished with 1 verified, 0 errors