From d9ed5e32fd306f0da3fc2a24ec17c81bff1c24fc Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Wed, 7 May 2014 20:17:09 +0100
Subject: Enabled prover lit tests.

---
 Test/prover/Answer                             | 68 +++++++++++++-------------
 Test/prover/EQ_v2.Eval__v4.Eval_out.bpl        |  2 +
 Test/prover/EQ_v2.Eval__v4.Eval_out.bpl.expect | 28 +++++++++++
 Test/prover/z3mutl.bpl                         |  2 +
 Test/prover/z3mutl.bpl.expect                  | 17 +++++++
 5 files changed, 83 insertions(+), 34 deletions(-)
 create mode 100644 Test/prover/EQ_v2.Eval__v4.Eval_out.bpl.expect
 create mode 100644 Test/prover/z3mutl.bpl.expect

(limited to 'Test/prover')

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
-- 
cgit v1.2.3