fixes to z3api

2 files changed, 129 insertions, 58 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

diff --git a/Test/z3api/runtest.bat b/Test/z3api/runtest.bat
index e9bc968e..6645667e 100644
--- a/Test/z3api/runtest.bat
+++ b/Test/z3api/runtest.bat
@@ -3,15 +3,14 @@ setlocal
 

 set BGEXE=..\..\Binaries\Boogie.exe

 

-for %%f in (boog0.bpl boog1.bpl boog2.bpl boog3.bpl boog4.bpl boog5.bpl boog6.bpl boog7.bpl boog8.bpl boog9.bpl boog10.bpl boog11.bpl boog13.bpl boog14.bpl boog16.bpl boog17.bpl boog18.bpl boog20.bpl boog21.bpl boog22.bpl boog24.bpl boog28.bpl boog29.bpl boog30.bpl boog31.bpl boog34.bpl) do (

+for %%f in (boog0.bpl boog1.bpl boog2.bpl boog3.bpl boog4.bpl boog5.bpl boog6.bpl boog7.bpl boog8.bpl boog9.bpl boog10.bpl boog11.bpl boog12.bpl boog13.bpl boog14.bpl boog15.bpl boog16.bpl boog17.bpl boog18.bpl boog19.bpl boog20.bpl boog21.bpl boog22.bpl boog23.bpl boog24.bpl boog25.bpl boog28.bpl boog29.bpl boog30.bpl boog31.bpl boog34.bpl boog35.bpl) do (

   echo.

   echo -------------------- %%f --------------------

   %BGEXE% %* /nologo /typeEncoding:m /prover:z3api %%f

 )

 

-REM boog12.bpl

-REM boog15.bpl

-

-REM boog19.bpl

-REM boog23.bpl

-REM boog25.bpl
\ No newline at end of file
+for %%f in (bar1.bpl bar2.bpl bar3.bpl bar4.bpl bar6.bpl) do (

+  echo.

+  echo -------------------- %%f --------------------

+  %BGEXE% %* /nologo /noinfer /stratifiedInline:1 /prover:z3api %%f

+)
\ No newline at end of file