From 2c9905f46791fed75c10fc8c8bc144fb8fa461f3 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
Date: Wed, 29 May 2013 18:24:12 -0700
Subject: Fixed bug in the cutting of back edges (that manifested itself
 whenever the first block in a procedure was the target of a back edge)

---
 Test/test2/Answer          |  9 ++++++++-
 Test/test2/CutBackEdge.bpl | 26 ++++++++++++++++++++++++++
 2 files changed, 34 insertions(+), 1 deletion(-)

(limited to 'Test/test2')

diff --git a/Test/test2/Answer b/Test/test2/Answer
index 4a7fd32f..b936ef87 100644
--- a/Test/test2/Answer
+++ b/Test/test2/Answer
@@ -153,8 +153,15 @@ CutBackEdge.bpl(10,5): Error BP5005: This loop invariant might not be maintained
 Execution trace:
     CutBackEdge.bpl(5,3): entry
     CutBackEdge.bpl(9,3): block850
+CutBackEdge.bpl(20,5): Error BP5004: This loop invariant might not hold on entry.
+Execution trace:
+CutBackEdge.bpl(26,5): Error BP5001: This assertion might not hold.
+Execution trace:
+    CutBackEdge.bpl(25,3): L
+CutBackEdge.bpl(38,5): Error BP5004: This loop invariant might not hold on entry.
+Execution trace:
 
-Boogie program verifier finished with 0 verified, 1 error
+Boogie program verifier finished with 1 verified, 4 errors
 
 -------------------- False.bpl --------------------
 
diff --git a/Test/test2/CutBackEdge.bpl b/Test/test2/CutBackEdge.bpl
index 934974aa..7294d0f9 100644
--- a/Test/test2/CutBackEdge.bpl
+++ b/Test/test2/CutBackEdge.bpl
@@ -12,3 +12,29 @@ procedure Test()
     goto block850;
 
 }
+
+// The following procedure once exhibited a bug in Boogie's DAG manipulations
+procedure TightLoop0()
+{
+  L:
+    assert !true;  // error
+    goto L;
+}
+procedure TightLoop1()
+{
+  L:
+    assert false;  // error
+    goto L;
+}
+procedure TightLoop2()
+{
+  L:
+    assert true;  // cool
+    goto L;
+}
+procedure TightLoop3(b: bool)
+{
+  L:
+    assert b;  // error
+    goto L;
+}
-- 
cgit v1.2.3