1 files changed, 184 insertions, 184 deletions
diff --git a/Test/test2/Arrays.bpl b/Test/test2/Arrays.bpl
index 5f4bd9c9..2b88be4a 100644
--- a/Test/test2/Arrays.bpl
+++ b/Test/test2/Arrays.bpl
@@ -1,184 +1,184 @@
-// RUN: %boogie -noinfer "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// RUN: %boogie -noinfer -typeEncoding:m "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// --------------------  1-dimensional arrays  --------------------
-
-var A: [ref]int;
-
-procedure P0(o: ref, q: ref, y: int)
-  requires o != q;
-  modifies A;
-  ensures A[o] == old(A[o]) + y;
-  ensures (forall p: ref :: A[p] == old(A[p]) || p == o);
-{
-  var k: int;
-
-  start:
-    k := A[q];
-    A[o] := y + A[o];
-    A[q] := k;
-    return;
-}
-
-procedure P1(o: ref, q: ref, y: int)
-  // This procedure does not have the assumption that o != q.
-  modifies A;
-  // It also does not ensures anything about A[o]
-  ensures (forall p: ref :: A[p] == old(A[p]) || p == o);
-{
-  var k: int;
-
-  start:
-    k := A[q];
-    A[o] := y + A[o];
-    A[q] := k;
-    return;
-}
-
-procedure P2(o: ref, q: ref, y: int)
-  // This procedure does not have the assumption that o != q.
-  modifies A;
-  ensures A[o] == old(A[o]) + y;
-{
-  var k: int;
-
-  start:
-    k := A[q];
-    A[o] := y + A[o];
-    A[q] := k;
-    return;
-}  // error: postcondition violated (if o == q)
-
-// --------------------  2-dimensional arrays  --------------------
-
-var B: [ref,name]int;
-const F: name;
-
-procedure Q0(o: ref, q: ref, y: int, G: name)
-  requires o != q && F != G;
-  modifies B;
-  ensures B[o,F] == old(B[o,F]) + y;
-  ensures (forall p: ref, f: name :: B[p,f] == old(B[p,f]) ||
-                                     (p == o && f == F));
-{
-  var k: int;
-
-  start:
-    k := B[q,G];
-    B[o,F] := y + B[o,F];
-    B[q,G] := k;
-    return;
-}
-
-procedure Q1(o: ref, q: ref, y: int, G: name)
-  // This procedure does not have the assumption that o != q && F != G.
-  modifies B;
-  // It also does not ensures anything about B[o,F]
-  ensures (forall p: ref, f: name :: B[p,f] == old(B[p,f]) ||
-                                     (p == o && f == F));
-{
-  var k: int;
-
-  start:
-    k := B[q,G];
-    B[o,F] := y + B[o,F];
-    B[q,G] := k;
-    return;
-}
-
-procedure Q2(o: ref, q: ref, y: int, G: name)
-  requires F != G;
-  // This procedure does not have the assumption that o != q.
-  modifies B;
-  ensures B[o,F] == old(B[o,F]) + y;
-{
-  var k: int;
-
-  start:
-    k := B[q,G];
-    B[o,F] := y + B[o,F];
-    B[q,G] := k;
-    return;
-}
-
-procedure Q3(o: ref, q: ref, y: int, G: name)
-  requires o != q;
-  // This procedure does not have the assumption that F != G.
-  modifies B;
-  ensures B[o,F] == old(B[o,F]) + y;
-{
-  var k: int;
-
-  start:
-    k := B[q,G];
-    B[o,F] := y + B[o,F];
-    B[q,G] := k;
-    return;
-}
-
-procedure Q4(o: ref, q: ref, y: int, G: name)
-  // This procedure does not have either of the assumptions o != q and F != G.
-  modifies B;
-  ensures B[o,F] == old(B[o,F]) + y;
-{
-  var k: int;
-
-  start:
-    k := B[q,G];
-    B[o,F] := y + B[o,F];
-    B[q,G] := k;
-    return;
-}  // error: postcondition violated
-
-// --------------------  more tests  --------------------
-
-procedure Skip0(o: ref, q: ref, G: name, H: name)
-  modifies A,B;
-  ensures (forall p: ref :: A[p] == old(A[p]));
-  ensures (forall p: ref, g: name :: B[p,g] == old(B[p,g]));
-{
-  start:
-    return;
-}
-
-procedure Skip1(o: ref, q: ref, G: name, H: name)
-  modifies A,B;
-  ensures (forall p: ref :: A[p] == old(A[p]));
-  ensures (forall p: ref, g: name :: B[p,g] == old(B[p,g]));
-{
-  var k: int;
-  var l: int;
-
-  start:
-    k := A[o];
-    l := A[q];
-    goto oneWay, theOtherWay;
-
-  oneWay:
-    A[o] := k;
-    A[q] := l;
-    goto next;
-
-  theOtherWay:
-    A[q] := l;
-    A[o] := k;
-    goto next;
-
-  next:
-    k := B[o,G];
-    l := B[q,H];
-    goto Lx, Ly;
-
-  Lx:
-    B[o,G] := k;
-    B[q,H] := l;
-    return;
-
-  Ly:
-    B[q,H] := l;
-    B[o,G] := k;
-    return;
-}
-
-type name, ref;
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// RUN: %boogie -noinfer -typeEncoding:m "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// --------------------  1-dimensional arrays  --------------------
+
+var A: [ref]int;
+
+procedure P0(o: ref, q: ref, y: int)
+  requires o != q;
+  modifies A;
+  ensures A[o] == old(A[o]) + y;
+  ensures (forall p: ref :: A[p] == old(A[p]) || p == o);
+{
+  var k: int;
+
+  start:
+    k := A[q];
+    A[o] := y + A[o];
+    A[q] := k;
+    return;
+}
+
+procedure P1(o: ref, q: ref, y: int)
+  // This procedure does not have the assumption that o != q.
+  modifies A;
+  // It also does not ensures anything about A[o]
+  ensures (forall p: ref :: A[p] == old(A[p]) || p == o);
+{
+  var k: int;
+
+  start:
+    k := A[q];
+    A[o] := y + A[o];
+    A[q] := k;
+    return;
+}
+
+procedure P2(o: ref, q: ref, y: int)
+  // This procedure does not have the assumption that o != q.
+  modifies A;
+  ensures A[o] == old(A[o]) + y;
+{
+  var k: int;
+
+  start:
+    k := A[q];
+    A[o] := y + A[o];
+    A[q] := k;
+    return;
+}  // error: postcondition violated (if o == q)
+
+// --------------------  2-dimensional arrays  --------------------
+
+var B: [ref,name]int;
+const F: name;
+
+procedure Q0(o: ref, q: ref, y: int, G: name)
+  requires o != q && F != G;
+  modifies B;
+  ensures B[o,F] == old(B[o,F]) + y;
+  ensures (forall p: ref, f: name :: B[p,f] == old(B[p,f]) ||
+                                     (p == o && f == F));
+{
+  var k: int;
+
+  start:
+    k := B[q,G];
+    B[o,F] := y + B[o,F];
+    B[q,G] := k;
+    return;
+}
+
+procedure Q1(o: ref, q: ref, y: int, G: name)
+  // This procedure does not have the assumption that o != q && F != G.
+  modifies B;
+  // It also does not ensures anything about B[o,F]
+  ensures (forall p: ref, f: name :: B[p,f] == old(B[p,f]) ||
+                                     (p == o && f == F));
+{
+  var k: int;
+
+  start:
+    k := B[q,G];
+    B[o,F] := y + B[o,F];
+    B[q,G] := k;
+    return;
+}
+
+procedure Q2(o: ref, q: ref, y: int, G: name)
+  requires F != G;
+  // This procedure does not have the assumption that o != q.
+  modifies B;
+  ensures B[o,F] == old(B[o,F]) + y;
+{
+  var k: int;
+
+  start:
+    k := B[q,G];
+    B[o,F] := y + B[o,F];
+    B[q,G] := k;
+    return;
+}
+
+procedure Q3(o: ref, q: ref, y: int, G: name)
+  requires o != q;
+  // This procedure does not have the assumption that F != G.
+  modifies B;
+  ensures B[o,F] == old(B[o,F]) + y;
+{
+  var k: int;
+
+  start:
+    k := B[q,G];
+    B[o,F] := y + B[o,F];
+    B[q,G] := k;
+    return;
+}
+
+procedure Q4(o: ref, q: ref, y: int, G: name)
+  // This procedure does not have either of the assumptions o != q and F != G.
+  modifies B;
+  ensures B[o,F] == old(B[o,F]) + y;
+{
+  var k: int;
+
+  start:
+    k := B[q,G];
+    B[o,F] := y + B[o,F];
+    B[q,G] := k;
+    return;
+}  // error: postcondition violated
+
+// --------------------  more tests  --------------------
+
+procedure Skip0(o: ref, q: ref, G: name, H: name)
+  modifies A,B;
+  ensures (forall p: ref :: A[p] == old(A[p]));
+  ensures (forall p: ref, g: name :: B[p,g] == old(B[p,g]));
+{
+  start:
+    return;
+}
+
+procedure Skip1(o: ref, q: ref, G: name, H: name)
+  modifies A,B;
+  ensures (forall p: ref :: A[p] == old(A[p]));
+  ensures (forall p: ref, g: name :: B[p,g] == old(B[p,g]));
+{
+  var k: int;
+  var l: int;
+
+  start:
+    k := A[o];
+    l := A[q];
+    goto oneWay, theOtherWay;
+
+  oneWay:
+    A[o] := k;
+    A[q] := l;
+    goto next;
+
+  theOtherWay:
+    A[q] := l;
+    A[o] := k;
+    goto next;
+
+  next:
+    k := B[o,G];
+    l := B[q,H];
+    goto Lx, Ly;
+
+  Lx:
+    B[o,G] := k;
+    B[q,H] := l;
+    return;
+
+  Ly:
+    B[q,H] := l;
+    B[o,G] := k;
+    return;
+}
+
+type name, ref;