diff options
Diffstat (limited to 'Test/test2/CutBackEdge.bpl')
-rw-r--r-- | Test/test2/CutBackEdge.bpl | 26 |
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;
+}
|