Enabled prover lit tests.

5 files changed, 83 insertions, 34 deletions

diff --git a/Test/prover/Answer b/Test/prover/Answer
index 13621984..9d972092 100644
--- a/Test/prover/Answer
+++ b/Test/prover/Answer
@@ -1,50 +1,50 @@
 ==================== -z3multipleErrors ========================

 

 -------------------- z3mutl.bpl --------------------

-z3mutl.bpl(20,5): Error BP5001: This assertion might not hold.

+z3mutl.bpl(22,5): Error BP5001: This assertion might not hold.

 Execution trace:

-    z3mutl.bpl(5,1): start

-    z3mutl.bpl(8,1): L1

-    z3mutl.bpl(20,1): L5

-z3mutl.bpl(20,5): Error BP5001: This assertion might not hold.

+    z3mutl.bpl(7,1): start

+    z3mutl.bpl(10,1): L1

+    z3mutl.bpl(22,1): L5

+z3mutl.bpl(22,5): Error BP5001: This assertion might not hold.

 Execution trace:

-    z3mutl.bpl(5,1): start

-    z3mutl.bpl(11,1): L2

-    z3mutl.bpl(20,1): L5

-z3mutl.bpl(20,5): Error BP5001: This assertion might not hold.

+    z3mutl.bpl(7,1): start

+    z3mutl.bpl(13,1): L2

+    z3mutl.bpl(22,1): L5

+z3mutl.bpl(22,5): Error BP5001: This assertion might not hold.

 Execution trace:

-    z3mutl.bpl(5,1): start

-    z3mutl.bpl(14,1): L3

-    z3mutl.bpl(20,1): L5

+    z3mutl.bpl(7,1): start

+    z3mutl.bpl(16,1): L3

+    z3mutl.bpl(22,1): L5

 

 Boogie program verifier finished with 0 verified, 3 errors

 

 -------------------- EQ_v2.Eval__v4.Eval_out.bpl --------------------

-EQ_v2.Eval__v4.Eval_out.bpl(2101,5): Error BP5003: A postcondition might not hold on this return path.

-EQ_v2.Eval__v4.Eval_out.bpl(1715,3): Related location: This is the postcondition that might not hold.

+EQ_v2.Eval__v4.Eval_out.bpl(2103,5): Error BP5003: A postcondition might not hold on this return path.

+EQ_v2.Eval__v4.Eval_out.bpl(1717,3): Related location: This is the postcondition that might not hold.

 Execution trace:

-    EQ_v2.Eval__v4.Eval_out.bpl(1786,3): AA_INSTR_EQ_BODY

-    EQ_v2.Eval__v4.Eval_out.bpl(1862,3): inline$v2.Eval$0$label_11_case_2#2

-    EQ_v2.Eval__v4.Eval_out.bpl(1894,3): inline$v2.Eval$0$label_12#2

-    EQ_v2.Eval__v4.Eval_out.bpl(1989,3): inline$v4.Eval$0$label_11_case_2#2

-    EQ_v2.Eval__v4.Eval_out.bpl(2011,3): inline$v4.Eval$0$label_14_true#2

-    EQ_v2.Eval__v4.Eval_out.bpl(2081,3): inline$v4.Eval$0$label_12#2

-EQ_v2.Eval__v4.Eval_out.bpl(2101,5): Error BP5003: A postcondition might not hold on this return path.

-EQ_v2.Eval__v4.Eval_out.bpl(1715,3): Related location: This is the postcondition that might not hold.

+    EQ_v2.Eval__v4.Eval_out.bpl(1788,3): AA_INSTR_EQ_BODY

+    EQ_v2.Eval__v4.Eval_out.bpl(1864,3): inline$v2.Eval$0$label_11_case_2#2

+    EQ_v2.Eval__v4.Eval_out.bpl(1896,3): inline$v2.Eval$0$label_12#2

+    EQ_v2.Eval__v4.Eval_out.bpl(1991,3): inline$v4.Eval$0$label_11_case_2#2

+    EQ_v2.Eval__v4.Eval_out.bpl(2013,3): inline$v4.Eval$0$label_14_true#2

+    EQ_v2.Eval__v4.Eval_out.bpl(2083,3): inline$v4.Eval$0$label_12#2

+EQ_v2.Eval__v4.Eval_out.bpl(2103,5): Error BP5003: A postcondition might not hold on this return path.

+EQ_v2.Eval__v4.Eval_out.bpl(1717,3): Related location: This is the postcondition that might not hold.

 Execution trace:

-    EQ_v2.Eval__v4.Eval_out.bpl(1786,3): AA_INSTR_EQ_BODY

-    EQ_v2.Eval__v4.Eval_out.bpl(1875,3): inline$v2.Eval$0$label_11_case_1#2

-    EQ_v2.Eval__v4.Eval_out.bpl(1894,3): inline$v2.Eval$0$label_12#2

-    EQ_v2.Eval__v4.Eval_out.bpl(2032,3): inline$v4.Eval$0$label_11_case_1#2

-    EQ_v2.Eval__v4.Eval_out.bpl(2054,3): inline$v4.Eval$0$label_13_true#2

-    EQ_v2.Eval__v4.Eval_out.bpl(2081,3): inline$v4.Eval$0$label_12#2

-EQ_v2.Eval__v4.Eval_out.bpl(2152,5): Error BP5003: A postcondition might not hold on this return path.

-EQ_v2.Eval__v4.Eval_out.bpl(2120,3): Related location: This is the postcondition that might not hold.

+    EQ_v2.Eval__v4.Eval_out.bpl(1788,3): AA_INSTR_EQ_BODY

+    EQ_v2.Eval__v4.Eval_out.bpl(1877,3): inline$v2.Eval$0$label_11_case_1#2

+    EQ_v2.Eval__v4.Eval_out.bpl(1896,3): inline$v2.Eval$0$label_12#2

+    EQ_v2.Eval__v4.Eval_out.bpl(2034,3): inline$v4.Eval$0$label_11_case_1#2

+    EQ_v2.Eval__v4.Eval_out.bpl(2056,3): inline$v4.Eval$0$label_13_true#2

+    EQ_v2.Eval__v4.Eval_out.bpl(2083,3): inline$v4.Eval$0$label_12#2

+EQ_v2.Eval__v4.Eval_out.bpl(2154,5): Error BP5003: A postcondition might not hold on this return path.

+EQ_v2.Eval__v4.Eval_out.bpl(2122,3): Related location: This is the postcondition that might not hold.

 Execution trace:

-    EQ_v2.Eval__v4.Eval_out.bpl(2133,3): AA_INSTR_EQ_BODY

-EQ_v2.Eval__v4.Eval_out.bpl(2192,5): Error BP5003: A postcondition might not hold on this return path.

-EQ_v2.Eval__v4.Eval_out.bpl(2167,3): Related location: This is the postcondition that might not hold.

+    EQ_v2.Eval__v4.Eval_out.bpl(2135,3): AA_INSTR_EQ_BODY

+EQ_v2.Eval__v4.Eval_out.bpl(2194,5): Error BP5003: A postcondition might not hold on this return path.

+EQ_v2.Eval__v4.Eval_out.bpl(2169,3): Related location: This is the postcondition that might not hold.

 Execution trace:

-    EQ_v2.Eval__v4.Eval_out.bpl(2178,3): AA_INSTR_EQ_BODY

+    EQ_v2.Eval__v4.Eval_out.bpl(2180,3): AA_INSTR_EQ_BODY

 

 Boogie program verifier finished with 6 verified, 4 errors

diff --git a/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl b/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl
index e53e00b4..24c9d5ea 100644
--- a/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl
+++ b/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -typeEncoding:m -z3multipleErrors %s > %t

+// RUN: %diff %s.expect %t

 var v4.Mem: [name][int]int;

 

 var v4.alloc: int;

diff --git a/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl.expect b/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl.expect
new file mode 100644
index 00000000..628a1fe4
--- /dev/null
+++ b/Test/prover/EQ_v2.Eval__v4.Eval_out.bpl.expect
@@ -0,0 +1,28 @@
+EQ_v2.Eval__v4.Eval_out.bpl(2103,5): Error BP5003: A postcondition might not hold on this return path.
+EQ_v2.Eval__v4.Eval_out.bpl(1717,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+    EQ_v2.Eval__v4.Eval_out.bpl(1788,3): AA_INSTR_EQ_BODY
+    EQ_v2.Eval__v4.Eval_out.bpl(1864,3): inline$v2.Eval$0$label_11_case_2#2
+    EQ_v2.Eval__v4.Eval_out.bpl(1896,3): inline$v2.Eval$0$label_12#2
+    EQ_v2.Eval__v4.Eval_out.bpl(1991,3): inline$v4.Eval$0$label_11_case_2#2
+    EQ_v2.Eval__v4.Eval_out.bpl(2013,3): inline$v4.Eval$0$label_14_true#2
+    EQ_v2.Eval__v4.Eval_out.bpl(2083,3): inline$v4.Eval$0$label_12#2
+EQ_v2.Eval__v4.Eval_out.bpl(2103,5): Error BP5003: A postcondition might not hold on this return path.
+EQ_v2.Eval__v4.Eval_out.bpl(1717,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+    EQ_v2.Eval__v4.Eval_out.bpl(1788,3): AA_INSTR_EQ_BODY
+    EQ_v2.Eval__v4.Eval_out.bpl(1877,3): inline$v2.Eval$0$label_11_case_1#2
+    EQ_v2.Eval__v4.Eval_out.bpl(1896,3): inline$v2.Eval$0$label_12#2
+    EQ_v2.Eval__v4.Eval_out.bpl(2034,3): inline$v4.Eval$0$label_11_case_1#2
+    EQ_v2.Eval__v4.Eval_out.bpl(2056,3): inline$v4.Eval$0$label_13_true#2
+    EQ_v2.Eval__v4.Eval_out.bpl(2083,3): inline$v4.Eval$0$label_12#2
+EQ_v2.Eval__v4.Eval_out.bpl(2154,5): Error BP5003: A postcondition might not hold on this return path.
+EQ_v2.Eval__v4.Eval_out.bpl(2122,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+    EQ_v2.Eval__v4.Eval_out.bpl(2135,3): AA_INSTR_EQ_BODY
+EQ_v2.Eval__v4.Eval_out.bpl(2194,5): Error BP5003: A postcondition might not hold on this return path.
+EQ_v2.Eval__v4.Eval_out.bpl(2169,3): Related location: This is the postcondition that might not hold.
+Execution trace:
+    EQ_v2.Eval__v4.Eval_out.bpl(2180,3): AA_INSTR_EQ_BODY
+
+Boogie program verifier finished with 6 verified, 4 errors
diff --git a/Test/prover/z3mutl.bpl b/Test/prover/z3mutl.bpl
index 73cd62b1..b184a6a4 100644
--- a/Test/prover/z3mutl.bpl
+++ b/Test/prover/z3mutl.bpl
@@ -1,3 +1,5 @@
+// RUN: %boogie -typeEncoding:m -z3multipleErrors %s > %t

+// RUN: %diff %s.expect %t

 var x:int;

 

 procedure Foo(){

diff --git a/Test/prover/z3mutl.bpl.expect b/Test/prover/z3mutl.bpl.expect
new file mode 100644
index 00000000..a4e7fea7
--- /dev/null
+++ b/Test/prover/z3mutl.bpl.expect
@@ -0,0 +1,17 @@
+z3mutl.bpl(22,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    z3mutl.bpl(7,1): start
+    z3mutl.bpl(10,1): L1
+    z3mutl.bpl(22,1): L5
+z3mutl.bpl(22,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    z3mutl.bpl(7,1): start
+    z3mutl.bpl(13,1): L2
+    z3mutl.bpl(22,1): L5
+z3mutl.bpl(22,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    z3mutl.bpl(7,1): start
+    z3mutl.bpl(16,1): L3
+    z3mutl.bpl(22,1): L5
+
+Boogie program verifier finished with 0 verified, 3 errors