Enabled lit loop unrolling test

5 files changed, 38 insertions, 12 deletions

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