1 files changed, 165 insertions, 165 deletions
diff --git a/Test/test2/Where.bpl b/Test/test2/Where.bpl
index fed05d76..762da163 100644
--- a/Test/test2/Where.bpl
+++ b/Test/test2/Where.bpl
@@ -1,165 +1,165 @@
-// RUN: %boogie -noinfer "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-procedure P0()
-{
-  var x: int where 0 <= x;
-  var y: int where x <= y;
-
-  assert 0 <= x;
-  assert x <= y;
-  assert y < 5;  // error
-}
-
-procedure P1()
-{
-  var x: int where 0 <= x;
-  var y: int where x <= y;
-
-  x := 5;
-  havoc y;
-  assert 5 <= y;
-
-  havoc x;
-  assert 0 <= x;
-  assert x <= y;  // error
-}
-
-procedure P2()
-{
-  var x: int where 0 <= x;
-  var y: int where x <= y;
-
-  havoc y;  // y first
-  havoc x;
-  assert x <= y;  // error
-}
-
-procedure P3()
-{
-  var x: int where 0 <= x;
-  var y: int where x <= y;
-
-  x := 5;
-  havoc x;  // this time, x first
-  havoc y;
-  assert x <= y;  // yeah!
-  assert 5 <= y;  // error
-}
-
-procedure P4()
-{
-  var x: int where 0 <= x;
-  var y: int where x <= y;
-
-  havoc x, y;  // both at the same time
-  assert 0 <= x && x <= y;
-  havoc y, x;  // or in the other order
-  assert 0 <= x && x <= y;
-
-  assert x == 7;  // error
-}
-
-procedure R0() returns (wProc: int where wProc == xProc,
-                        xProc: int where 0 <= xProc,
-                        yProc: int where xProc <= yProc);
-implementation R0() returns (w: int, x: int, y: int)
-{
-  while (*) {
-    assert w == x;
-    assert 0 <= x;
-    assert x <= y;
-  }
-  while (*) {
-    assert w == x;
-    assert 0 <= x;
-    assert x <= y;
-    // the following makes w, x, y loop targets
-    w := w + 1;
-    havoc x;
-    y := w;
-  }
-  assert w == x;
-  assert 0 <= x;
-  assert x <= y;
-}
-
-procedure R1()
-{
-  var a: int;
-  var b: int;
-  var c: int;
-
-  call a, b, c := R0();
-  assert a == b;
-  assert 0 <= b;
-  assert b <= c;
-}
-
-procedure R2()
-{
-  var w: int where w == x;
-  var x: int where 0 <= x;
-  var y: int where x <= y;
-
-  x := 5;
-  y := 10;
-  while (*) {
-    w := w + 1;
-    assert w == 6;
-    y := y + 2;
-    assert 7 <= y;
-  }
-  assert x == 5 && 0 <= y - w;
-  assert y == 10;  // error
-}
-
-procedure R3()
-{
-  var w: int where w == x;
-  var x: int where 0 <= x;
-  var y: int where x <= y;
-
-  // change w and x
-  y := 10;
-  while (*) {
-    w := w;  x := x;
-  }
-  assert w == x;
-  assert 0 <= x;
-  assert y == 10;
-  assert w <= 10;  // error
-}
-
-procedure R4()
-{
-  var w: int where w == x;
-  var x: int where 0 <= x;
-  var y: int where x <= y;
-
-  // change x and y
-  w := 12;
-  while (*) {
-    x := x;  y := y;
-  }
-  assert 0 <= x;
-  assert x <= y;
-  assert w == 12;
-  assert 8 <= y;  // error
-}
-
-procedure R5(K: int)
-{
-  var w: int where w == x;
-  var x: int where 0 <= x;
-  var y: int where x <= y;
-
-  // change w and y
-  x := K;
-  while (*) {
-    w := w;  y := y;
-  }
-  assert w == K;
-  assert K <= y;
-  assert x == K;
-  assert 0 <= x;  // error
-}
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure P0()
+{
+  var x: int where 0 <= x;
+  var y: int where x <= y;
+
+  assert 0 <= x;
+  assert x <= y;
+  assert y < 5;  // error
+}
+
+procedure P1()
+{
+  var x: int where 0 <= x;
+  var y: int where x <= y;
+
+  x := 5;
+  havoc y;
+  assert 5 <= y;
+
+  havoc x;
+  assert 0 <= x;
+  assert x <= y;  // error
+}
+
+procedure P2()
+{
+  var x: int where 0 <= x;
+  var y: int where x <= y;
+
+  havoc y;  // y first
+  havoc x;
+  assert x <= y;  // error
+}
+
+procedure P3()
+{
+  var x: int where 0 <= x;
+  var y: int where x <= y;
+
+  x := 5;
+  havoc x;  // this time, x first
+  havoc y;
+  assert x <= y;  // yeah!
+  assert 5 <= y;  // error
+}
+
+procedure P4()
+{
+  var x: int where 0 <= x;
+  var y: int where x <= y;
+
+  havoc x, y;  // both at the same time
+  assert 0 <= x && x <= y;
+  havoc y, x;  // or in the other order
+  assert 0 <= x && x <= y;
+
+  assert x == 7;  // error
+}
+
+procedure R0() returns (wProc: int where wProc == xProc,
+                        xProc: int where 0 <= xProc,
+                        yProc: int where xProc <= yProc);
+implementation R0() returns (w: int, x: int, y: int)
+{
+  while (*) {
+    assert w == x;
+    assert 0 <= x;
+    assert x <= y;
+  }
+  while (*) {
+    assert w == x;
+    assert 0 <= x;
+    assert x <= y;
+    // the following makes w, x, y loop targets
+    w := w + 1;
+    havoc x;
+    y := w;
+  }
+  assert w == x;
+  assert 0 <= x;
+  assert x <= y;
+}
+
+procedure R1()
+{
+  var a: int;
+  var b: int;
+  var c: int;
+
+  call a, b, c := R0();
+  assert a == b;
+  assert 0 <= b;
+  assert b <= c;
+}
+
+procedure R2()
+{
+  var w: int where w == x;
+  var x: int where 0 <= x;
+  var y: int where x <= y;
+
+  x := 5;
+  y := 10;
+  while (*) {
+    w := w + 1;
+    assert w == 6;
+    y := y + 2;
+    assert 7 <= y;
+  }
+  assert x == 5 && 0 <= y - w;
+  assert y == 10;  // error
+}
+
+procedure R3()
+{
+  var w: int where w == x;
+  var x: int where 0 <= x;
+  var y: int where x <= y;
+
+  // change w and x
+  y := 10;
+  while (*) {
+    w := w;  x := x;
+  }
+  assert w == x;
+  assert 0 <= x;
+  assert y == 10;
+  assert w <= 10;  // error
+}
+
+procedure R4()
+{
+  var w: int where w == x;
+  var x: int where 0 <= x;
+  var y: int where x <= y;
+
+  // change x and y
+  w := 12;
+  while (*) {
+    x := x;  y := y;
+  }
+  assert 0 <= x;
+  assert x <= y;
+  assert w == 12;
+  assert 8 <= y;  // error
+}
+
+procedure R5(K: int)
+{
+  var w: int where w == x;
+  var x: int where 0 <= x;
+  var y: int where x <= y;
+
+  // change w and y
+  x := K;
+  while (*) {
+    w := w;  y := y;
+  }
+  assert w == K;
+  assert K <= y;
+  assert x == K;
+  assert 0 <= x;  // error
+}