1 files changed, 58 insertions, 0 deletions
diff --git a/Test/extractloops/Answer b/Test/extractloops/Answer
new file mode 100644
index 00000000..b3efbe02
--- /dev/null
+++ b/Test/extractloops/Answer
@@ -0,0 +1,58 @@
+----- Running regression test t1.bpl
+t1.bpl(38,5): Error BP5001: This assertion might not hold.
+Execution trace:
+        t1.bpl(19,3): anon0
+        t1.bpl(23,3): anon3_LoopHead
+        Inlined call to procedure foo begins
+            t1.bpl(11,5): anon0
+        Inlined call to procedure foo ends
+        t1.bpl(27,3): anon3_LoopBody
+        t1.bpl(23,3): anon3_LoopHead
+        Inlined call to procedure foo begins
+            t1.bpl(11,5): anon0
+        Inlined call to procedure foo ends
+        t1.bpl(27,3): anon3_LoopBody
+        t1.bpl(23,3): anon3_LoopHead
+        Inlined call to procedure foo begins
+            t1.bpl(11,5): anon0
+        Inlined call to procedure foo ends
+        t1.bpl(33,3): anon3_LoopDone
+        t1.bpl(37,3): anon2
+
+Boogie program verifier finished with 0 verified, 1 error
+-----
+----- Running regression test t2.bpl
+t2.bpl(51,5): Error BP5001: This assertion might not hold.
+Execution trace:
+        t2.bpl(19,3): anon0
+        t2.bpl(23,3): anon3_LoopHead
+        Inlined call to procedure foo begins
+            t2.bpl(11,5): anon0
+        Inlined call to procedure foo ends
+        t2.bpl(27,3): anon3_LoopBody
+        t2.bpl(34,3): lab1_LoopHead
+        t2.bpl(37,3): lab1_LoopBody
+        t2.bpl(34,3): lab1_LoopHead
+        t2.bpl(37,3): lab1_LoopBody
+        t2.bpl(34,3): lab1_LoopHead
+        t2.bpl(42,3): lab1_LoopDone
+        t2.bpl(23,3): anon3_LoopHead
+        Inlined call to procedure foo begins
+            t2.bpl(11,5): anon0
+        Inlined call to procedure foo ends
+        t2.bpl(27,3): anon3_LoopBody
+        t2.bpl(34,3): lab1_LoopHead
+        t2.bpl(37,3): lab1_LoopBody
+        t2.bpl(34,3): lab1_LoopHead
+        t2.bpl(37,3): lab1_LoopBody
+        t2.bpl(34,3): lab1_LoopHead
+        t2.bpl(42,3): lab1_LoopDone
+        t2.bpl(23,3): anon3_LoopHead
+        Inlined call to procedure foo begins
+            t2.bpl(11,5): anon0
+        Inlined call to procedure foo ends
+        t2.bpl(46,3): anon3_LoopDone
+        t2.bpl(50,3): anon2
+
+Boogie program verifier finished with 0 verified, 1 error
+-----