Initial set of files.

1 files changed, 187 insertions, 0 deletions

diff --git a/Test/z3api/Answer b/Test/z3api/Answer
new file mode 100644
index 00000000..782aa852
--- /dev/null
+++ b/Test/z3api/Answer
@@ -0,0 +1,187 @@
+

+-------------------- 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.

+Execution trace:

+    boog0.bpl(48,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(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.

+Execution trace:

+    boog2.bpl(22,8): anon0

+

+Boogie program verifier finished with 1 verified, 1 error

+

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

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

+Execution trace:

+    boog3.bpl(6,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(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.

+Execution trace:

+    boog5.bpl(32,3): anon0

+    boog5.bpl(35,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(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.

+Execution trace:

+    boog7.bpl(16,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

+

+-------------------- 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.

+Execution trace:

+    boog9.bpl(18,11): anon0

+

+Boogie program verifier finished with 0 verified, 1 error

+

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

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

+Execution trace:

+    boog10.bpl(18,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.

+Execution trace:

+    boog11.bpl(13,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.

+Execution trace:

+    boog12.bpl(16,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

+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.

+Execution trace:

+    boog14.bpl(10,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.

+Execution trace:

+    boog15.bpl(9,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.

+Execution trace:

+    boog16.bpl(10,8): anon0

+

+Boogie program verifier finished with 0 verified, 1 error

+

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

+boog17.bpl(24,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

+

+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.

+Execution trace:

+    boog18.bpl(14,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(15,1): Error BP5001: This assertion might not hold.

+Execution trace:

+    boog20.bpl(15,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(4,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(12,1): Error BP5001: This assertion might not hold.

+Execution trace:

+    boog31.bpl(12,1): anon0

+

+Boogie program verifier finished with 0 verified, 1 error

+

+-------------------- boog34.bpl --------------------

+

+Boogie program verifier finished with 1 verified, 0 errors