Merging complete. Everything looks good *crosses fingers*

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;
+  }
+}