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)

1 files changed, 26 insertions, 0 deletions

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;

+}