From 962f8d5252b3f5ec4d19e0cd2a430934bd55cc6d Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sun, 28 Jun 2015 01:44:30 +0100
Subject: Normalise line endings using a .gitattributes file. Unfortunately
 this required that this commit globally modify most files. If you want to use
 git blame to see the real author of a line use the ``-w`` flag so that
 whitespace changes are ignored.

---
 Test/test13/ErrorTraceTestLoopInvViolationBPL.bpl | 64 +++++++++++------------
 1 file changed, 32 insertions(+), 32 deletions(-)

(limited to 'Test/test13')

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;
+  }
+}
-- 
cgit v1.2.3