From f45eb9f44f32cbab80e0aaaff167f6b60b9abbc3 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Wed, 7 May 2014 20:06:38 +0100
Subject: Enabled lit loop unrolling test

---
 Test/test16/Answer                  | 24 ++++++++++++------------
 Test/test16/LoopUnroll.bpl          |  6 ++++++
 Test/test16/LoopUnroll.bpl.1.expect |  7 +++++++
 Test/test16/LoopUnroll.bpl.2.expect |  2 ++
 Test/test16/LoopUnroll.bpl.3.expect | 11 +++++++++++
 5 files changed, 38 insertions(+), 12 deletions(-)
 create mode 100644 Test/test16/LoopUnroll.bpl.1.expect
 create mode 100644 Test/test16/LoopUnroll.bpl.2.expect
 create mode 100644 Test/test16/LoopUnroll.bpl.3.expect

diff --git a/Test/test16/Answer b/Test/test16/Answer
index 5fac425b..8c0b0187 100644
--- a/Test/test16/Answer
+++ b/Test/test16/Answer
@@ -1,23 +1,23 @@
 -------------------- LoopUnroll.bpl /loopUnroll:1 --------------------
-LoopUnroll.bpl(56,5): Error BP5001: This assertion might not hold.
+LoopUnroll.bpl(62,5): Error BP5001: This assertion might not hold.
 Execution trace:
-    LoopUnroll.bpl(52,5): anon0#1
-    LoopUnroll.bpl(53,3): anon2_LoopHead#1
-    LoopUnroll.bpl(55,5): anon2_LoopBody#1
+    LoopUnroll.bpl(58,5): anon0#1
+    LoopUnroll.bpl(59,3): anon2_LoopHead#1
+    LoopUnroll.bpl(61,5): anon2_LoopBody#1
 
 Boogie program verifier finished with 2 verified, 1 error
 -------------------- LoopUnroll.bpl /loopUnroll:2 --------------------
 
 Boogie program verifier finished with 1 verified, 0 errors
 -------------------- LoopUnroll.bpl /loopUnroll:3 --------------------
-LoopUnroll.bpl(74,5): Error BP5001: This assertion might not hold.
+LoopUnroll.bpl(80,5): Error BP5001: This assertion might not hold.
 Execution trace:
-    LoopUnroll.bpl(68,5): anon0#3
-    LoopUnroll.bpl(69,3): anon2_LoopHead#3
-    LoopUnroll.bpl(71,5): anon2_LoopBody#3
-    LoopUnroll.bpl(69,3): anon2_LoopHead#2
-    LoopUnroll.bpl(71,5): anon2_LoopBody#2
-    LoopUnroll.bpl(69,3): anon2_LoopHead#1
-    LoopUnroll.bpl(71,5): anon2_LoopBody#1
+    LoopUnroll.bpl(74,5): anon0#3
+    LoopUnroll.bpl(75,3): anon2_LoopHead#3
+    LoopUnroll.bpl(77,5): anon2_LoopBody#3
+    LoopUnroll.bpl(75,3): anon2_LoopHead#2
+    LoopUnroll.bpl(77,5): anon2_LoopBody#2
+    LoopUnroll.bpl(75,3): anon2_LoopHead#1
+    LoopUnroll.bpl(77,5): anon2_LoopBody#1
 
 Boogie program verifier finished with 0 verified, 1 error
diff --git a/Test/test16/LoopUnroll.bpl b/Test/test16/LoopUnroll.bpl
index 83bf2686..13841d2c 100644
--- a/Test/test16/LoopUnroll.bpl
+++ b/Test/test16/LoopUnroll.bpl
@@ -1,3 +1,9 @@
+// RUN: %boogie -loopUnroll:1 -logPrefix:-lu1 LoopUnroll.bpl > %t1
+// RUN: %diff %s.1.expect %t1
+// RUN: %boogie -loopUnroll:2 -logPrefix:-lu2 -proc:ManyIterations LoopUnroll.bpl > %t2
+// RUN: %diff %s.2.expect %t2
+// RUN: %boogie -loopUnroll:3 -logPrefix:-lu3 -proc:ManyIterations LoopUnroll.bpl > %t3
+// RUN: %diff %s.3.expect %t3
 procedure P()
 {
   var x: int;
diff --git a/Test/test16/LoopUnroll.bpl.1.expect b/Test/test16/LoopUnroll.bpl.1.expect
new file mode 100644
index 00000000..e86e03d7
--- /dev/null
+++ b/Test/test16/LoopUnroll.bpl.1.expect
@@ -0,0 +1,7 @@
+LoopUnroll.bpl(62,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    LoopUnroll.bpl(58,5): anon0#1
+    LoopUnroll.bpl(59,3): anon2_LoopHead#1
+    LoopUnroll.bpl(61,5): anon2_LoopBody#1
+
+Boogie program verifier finished with 2 verified, 1 error
diff --git a/Test/test16/LoopUnroll.bpl.2.expect b/Test/test16/LoopUnroll.bpl.2.expect
new file mode 100644
index 00000000..37fad75c
--- /dev/null
+++ b/Test/test16/LoopUnroll.bpl.2.expect
@@ -0,0 +1,2 @@
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/test16/LoopUnroll.bpl.3.expect b/Test/test16/LoopUnroll.bpl.3.expect
new file mode 100644
index 00000000..56794cfc
--- /dev/null
+++ b/Test/test16/LoopUnroll.bpl.3.expect
@@ -0,0 +1,11 @@
+LoopUnroll.bpl(80,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    LoopUnroll.bpl(74,5): anon0#3
+    LoopUnroll.bpl(75,3): anon2_LoopHead#3
+    LoopUnroll.bpl(77,5): anon2_LoopBody#3
+    LoopUnroll.bpl(75,3): anon2_LoopHead#2
+    LoopUnroll.bpl(77,5): anon2_LoopBody#2
+    LoopUnroll.bpl(75,3): anon2_LoopHead#1
+    LoopUnroll.bpl(77,5): anon2_LoopBody#1
+
+Boogie program verifier finished with 0 verified, 1 error
-- 
cgit v1.2.3