summaryrefslogtreecommitdiff
path: root/Test/test13
diff options
context:
space:
mode:
Diffstat (limited to 'Test/test13')
-rw-r--r--Test/test13/ErrorTraceTestLoopInvViolationBPL.bpl64
1 files changed, 32 insertions, 32 deletions
diff --git a/Test/test13/ErrorTraceTestLoopInvViolationBPL.bpl b/Test/test13/ErrorTraceTestLoopInvViolationBPL.bpl
index 1c27c258..d9723426 100644
--- a/Test/test13/ErrorTraceTestLoopInvViolationBPL.bpl
+++ b/Test/test13/ErrorTraceTestLoopInvViolationBPL.bpl
@@ -1,32 +1,32 @@
-// RUN: %boogie "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// 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;
- }
-}
+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// 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;
+ }
+}