5 files changed, 51 insertions, 13 deletions
diff --git a/Source/VCGeneration/VC.cs b/Source/VCGeneration/VC.cs
index 988d80fd..6a0891b8 100644
--- a/Source/VCGeneration/VC.cs
+++ b/Source/VCGeneration/VC.cs
@@ -1789,13 +1789,15 @@ namespace VC {
       }
       #endregion
 
+      // Recompute the predecessors, but first insert a dummy start node that is sure not to be the target of any goto (because the cutting of back edges
+      // below assumes that the start node has no predecessor)
+      impl.Blocks.Insert(0, new Block(new Token(-17, -4), "0", new CmdSeq(), new GotoCmd(Token.NoToken, new StringSeq(impl.Blocks[0].Label), new BlockSeq(impl.Blocks[0]))));
       ResetPredecessors(impl.Blocks);
       
       #region Convert program CFG into a DAG
 
       #region Use the graph library to figure out where the (natural) loops are
 
-      
       #region Create the graph by adding the source node and each edge
       Graph<Block> g = Program.GraphFromImpl(impl);
       #endregion
diff --git a/Test/smoke/Answer b/Test/smoke/Answer
index 98cff8d2..e2390446 100644
--- a/Test/smoke/Answer
+++ b/Test/smoke/Answer
@@ -5,6 +5,9 @@ implementation b(x: int)
   var y: int;
 
 
+  0:
+    goto anon0;
+
   anon0:
     goto anon3_Then;
 
diff --git a/Test/test15/Answer b/Test/test15/Answer
index 915f63e8..159b3579 100644
--- a/Test/test15/Answer
+++ b/Test/test15/Answer
@@ -1,9 +1,9 @@
 
 -------------------- NullInModel --------------------
 *** MODEL
-%lbl%@45 -> false
+%lbl%@47 -> false
 %lbl%+24 -> true
-%lbl%+35 -> true
+%lbl%+37 -> true
 boolType -> T@T!val!2
 intType -> T@T!val!0
 null -> T@U!val!0
@@ -35,9 +35,9 @@ Boogie program verifier finished with 0 verified, 1 error
 
 -------------------- IntInModel --------------------
 *** MODEL
-%lbl%@37 -> false
+%lbl%@39 -> false
 %lbl%+23 -> true
-%lbl%+27 -> true
+%lbl%+29 -> true
 boolType -> T@T!val!2
 i -> 0
 intType -> T@T!val!0
@@ -62,9 +62,9 @@ Boogie program verifier finished with 0 verified, 1 error
 
 -------------------- ModelTest --------------------
 *** MODEL
-%lbl%@145 -> false
+%lbl%@147 -> false
 %lbl%+64 -> true
-%lbl%+82 -> true
+%lbl%+84 -> true
 boolType -> T@T!val!2
 i@0 -> 1
 intType -> T@T!val!0
@@ -120,11 +120,11 @@ Execution trace:
     CaptureState.bpl(16,5): anon4_Then
     CaptureState.bpl(24,5): anon3
 *** MODEL
-%lbl%@291 -> false
+%lbl%@293 -> false
 %lbl%+112 -> true
 %lbl%+114 -> true
 %lbl%+118 -> true
-%lbl%+146 -> true
+%lbl%+148 -> true
 @MV_state_const -> 6
 boolType -> T@T!val!2
 F -> T@U!val!2
@@ -133,7 +133,7 @@ Heap -> T@U!val!0
 intType -> T@T!val!0
 m -> **m
 m@0 -> -451
-m@2 -> -450
+m@1 -> -450
 m@3 -> -450
 r -> **r
 r@0 -> -900
@@ -155,8 +155,8 @@ type -> {
 }
 @MV_state -> {
   6 0 -> true
-  6 3 -> true
-  6 4 -> true
+  6 1 -> true
+  6 2 -> true
   6 5 -> true
   else -> true
 }
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;
+}