1 files changed, 30 insertions, 0 deletions
diff --git a/Test/test13/ErrorTraceTestLoopInvViolationBPL.bpl b/Test/test13/ErrorTraceTestLoopInvViolationBPL.bpl
new file mode 100644
index 00000000..f1be4414
--- /dev/null
+++ b/Test/test13/ErrorTraceTestLoopInvViolationBPL.bpl
@@ -0,0 +1,30 @@
+// simple assert
+procedure asserting() {
+  var x: int;
+
+  x := 0;
+
+  assert x == 1;
+}
+
+// invariant failing initially
+procedure loopInvInitiallyViolated(y: int) {
+  var x: int;
+
+  x := y;
+
+  while (true) invariant (x == 1); {
+    x := 1;
+  }
+}
+
+// invariant failing after iteration
+procedure loopInvMaintenanceViolated() {
+  var x: int;
+
+  x := 0;
+
+  while (true)  invariant x == 0; {
+    x := 1;
+  }
+}