fixes to z3api

1 files changed, 123 insertions, 51 deletions

diff --git a/Test/z3api/Answer b/Test/z3api/Answer
index 782aa852..d18f12ef 100644
--- a/Test/z3api/Answer
+++ b/Test/z3api/Answer
@@ -1,9 +1,9 @@
 

 -------------------- boog0.bpl --------------------

-boog0.bpl(51,1): Error BP5003: A postcondition might not hold at this return statement.

-boog0.bpl(45,3): Related location: This is the postcondition that might not hold.

+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(48,7): anon0

+    boog0.bpl(46,7): anon0

 

 Boogie program verifier finished with 1 verified, 1 error

 

@@ -12,17 +12,17 @@ Boogie program verifier finished with 1 verified, 1 error
 Boogie program verifier finished with 1 verified, 0 errors

 

 -------------------- boog2.bpl --------------------

-boog2.bpl(23,1): Error BP5003: A postcondition might not hold at this return statement.

-boog2.bpl(19,3): Related location: This is the postcondition that might not hold.

+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(22,8): anon0

+    boog2.bpl(23,8): anon0

 

 Boogie program verifier finished with 1 verified, 1 error

 

 -------------------- boog3.bpl --------------------

-boog3.bpl(6,3): Error BP5001: This assertion might not hold.

+boog3.bpl(7,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    boog3.bpl(6,3): anon0

+    boog3.bpl(7,3): anon0

 

 Boogie program verifier finished with 0 verified, 1 error

 

@@ -31,11 +31,11 @@ Boogie program verifier finished with 0 verified, 1 error
 Boogie program verifier finished with 1 verified, 0 errors

 

 -------------------- boog5.bpl --------------------

-boog5.bpl(36,3): Error BP5003: A postcondition might not hold at this return statement.

-boog5.bpl(29,3): Related location: This is the postcondition that might not hold.

+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(32,3): anon0

-    boog5.bpl(35,13): anon3_Else

+    boog5.bpl(33,3): anon0

+    boog5.bpl(36,13): anon3_Else

 

 Boogie program verifier finished with 0 verified, 1 error

 

@@ -44,91 +44,92 @@ Boogie program verifier finished with 0 verified, 1 error
 Boogie program verifier finished with 1 verified, 0 errors

 

 -------------------- boog7.bpl --------------------

-boog7.bpl(17,1): Error BP5003: A postcondition might not hold at this return statement.

-boog7.bpl(13,3): Related location: This is the postcondition that might not hold.

+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(16,11): anon0

+    boog7.bpl(17,11): anon0

 

 Boogie program verifier finished with 0 verified, 1 error

 

 -------------------- boog8.bpl --------------------

-boog8.bpl(7,12): Error: no bitvector handling specified, please use /bv:i or /bv:z flag

-boog8.bpl(7,18): Error: no bitvector handling specified, please use /bv:i or /bv:z flag

-2 type checking errors detected in 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(19,1): Error BP5003: A postcondition might not hold at this return statement.

-boog9.bpl(15,3): Related location: This is the postcondition that might not hold.

+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(18,11): anon0

+    boog9.bpl(19,11): anon0

 

 Boogie program verifier finished with 0 verified, 1 error

 

 -------------------- boog10.bpl --------------------

-boog10.bpl(18,3): Error BP5001: This assertion might not hold.

+boog10.bpl(19,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    boog10.bpl(18,3): anon0

+    boog10.bpl(19,3): anon0

 

 Boogie program verifier finished with 0 verified, 1 error

 

 -------------------- boog11.bpl --------------------

-boog11.bpl(14,1): Error BP5003: A postcondition might not hold at this return statement.

-boog11.bpl(10,3): Related location: This is the postcondition that might not hold.

+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(13,8): anon0

+    boog11.bpl(14,8): anon0

 

 Boogie program verifier finished with 0 verified, 1 error

 

 -------------------- boog12.bpl --------------------

-boog12.bpl(18,1): Error BP5003: A postcondition might not hold at this return statement.

-boog12.bpl(13,3): Related location: This is the postcondition that might not hold.

+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(16,16): anon0

+    boog12.bpl(17,16): anon0

 

 Boogie program verifier finished with 0 verified, 1 error

 

 -------------------- boog13.bpl --------------------

-boog13.bpl(9,11): Error: more than one declaration of variable name: v

+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(11,1): Error BP5003: A postcondition might not hold at this return statement.

-boog14.bpl(8,1): Related location: This is the postcondition that might not hold.

+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(10,8): anon0

+    boog14.bpl(11,8): anon0

 

 Boogie program verifier finished with 0 verified, 1 error

 

 -------------------- boog15.bpl --------------------

-boog15.bpl(10,1): Error BP5003: A postcondition might not hold at this return statement.

-boog15.bpl(7,1): Related location: This is the postcondition that might not hold.

+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(9,8): anon0

+    boog15.bpl(10,8): anon0

 

 Boogie program verifier finished with 0 verified, 1 error

 

 -------------------- boog16.bpl --------------------

-boog16.bpl(11,1): Error BP5003: A postcondition might not hold at this return statement.

-boog16.bpl(8,1): Related location: This is the postcondition that might not hold.

+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(10,8): anon0

+    boog16.bpl(11,8): anon0

 

 Boogie program verifier finished with 0 verified, 1 error

 

 -------------------- boog17.bpl --------------------

-boog17.bpl(24,3): Error BP5001: This assertion might not hold.

+boog17.bpl(26,3): Error BP5001: This assertion might not hold.

 Execution trace:

-    boog17.bpl(15,1): start

-    boog17.bpl(19,1): label_3

-    boog17.bpl(22,1): label_4

+    boog17.bpl(17,1): start

 

 Boogie program verifier finished with 0 verified, 1 error

 

 -------------------- boog18.bpl --------------------

-boog18.bpl(15,1): Error BP5003: A postcondition might not hold at this return statement.

-boog18.bpl(12,1): Related location: This is the postcondition that might not hold.

+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(14,4): anon0

+    boog18.bpl(15,4): anon0

 

 Boogie program verifier finished with 0 verified, 1 error

 

@@ -137,9 +138,9 @@ Boogie program verifier finished with 0 verified, 1 error
 Boogie program verifier finished with 1 verified, 0 errors

 

 -------------------- boog20.bpl --------------------

-boog20.bpl(15,1): Error BP5001: This assertion might not hold.

+boog20.bpl(16,1): Error BP5001: This assertion might not hold.

 Execution trace:

-    boog20.bpl(15,1): anon0

+    boog20.bpl(16,1): anon0

 

 Boogie program verifier finished with 0 verified, 1 error

 

@@ -148,7 +149,7 @@ Boogie program verifier finished with 0 verified, 1 error
 Boogie program verifier finished with 1 verified, 0 errors

 

 -------------------- boog22.bpl --------------------

-boog22.bpl(4,9): Error: more than one declaration of function/procedure name: f1

+boog22.bpl(5,9): Error: more than one declaration of function/procedure name: f1

 1 name resolution errors detected in boog22.bpl

 

 -------------------- boog23.bpl --------------------

@@ -176,12 +177,83 @@ Boogie program verifier finished with 1 verified, 0 errors
 Boogie program verifier finished with 1 verified, 0 errors

 

 -------------------- boog31.bpl --------------------

-boog31.bpl(12,1): Error BP5001: This assertion might not hold.

+boog31.bpl(13,1): Error BP5001: This assertion might not hold.

 Execution trace:

-    boog31.bpl(12,1): anon0

+    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