1 files changed, 5 insertions, 3 deletions
diff --git a/Test/aitest1/Linear5.bpl b/Test/aitest1/Linear5.bpl
index 4f04999c..199cb6f2 100644
--- a/Test/aitest1/Linear5.bpl
+++ b/Test/aitest1/Linear5.bpl
@@ -8,14 +8,16 @@ procedure p()
 {
   A:
     assume -1 <= x;
-    goto B;
+    goto B, E;
   B:
     assume x < y;
-    goto C;
+    goto C, E;
   C:
     x := x*x;
-    goto D;
+    goto D, E;
   D:
     x := y;
     return;
+  E:
+    return;
 }