1 files changed, 35 insertions, 35 deletions
diff --git a/Test/test20/PolyProcs0.bpl b/Test/test20/PolyProcs0.bpl
index 698e2f12..cc0ba491 100644
--- a/Test/test20/PolyProcs0.bpl
+++ b/Test/test20/PolyProcs0.bpl
@@ -1,35 +1,35 @@
-// RUN: %boogie -noVerify "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-
-
-type Field a;
-
-function FieldAccessFun<b>(heap : <a>[ref, Field a]a, obj : ref, f : Field b)
-         returns (res:b);
-
-procedure FieldAccess<b>(heap : <a>[ref, Field a]a, obj : ref, f : Field b)
-          returns (res:b) {
-  start:
-    res := heap[f, obj];    // error: wrong argument order
-    res := heap[obj, f];
-    assert res == FieldAccessFun(heap, obj, f);
-    return;
-}
-
-procedure UseHeap(heap : <a>[ref, Field a]a) {
-  var f1 : Field int; var f2 : Field bool; var obj : ref;
-  var x : int; var y : bool;
-
-  call x := FieldAccess(heap, f1, obj);  // error: wrong argument order
-  call x := FieldAccess(heap, obj, f1);
-  call y := FieldAccess(heap, obj, f2);
-
-  call y := FieldAccess(heap, obj, f1);  // error: wrong result type
-  call x := FieldAccess(heap, obj, obj); // error: wrong argument type
-}
-
-procedure injective<b>(heap : <a>[ref, Field a]a, obj0 : ref, obj1 : ref, f : Field b);
-   requires obj0 != obj1;
-   ensures heap[obj0, f] != heap[obj1, f];
-
-type ref;
+// RUN: %boogie -noVerify "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+
+
+type Field a;
+
+function FieldAccessFun<b>(heap : <a>[ref, Field a]a, obj : ref, f : Field b)
+         returns (res:b);
+
+procedure FieldAccess<b>(heap : <a>[ref, Field a]a, obj : ref, f : Field b)
+          returns (res:b) {
+  start:
+    res := heap[f, obj];    // error: wrong argument order
+    res := heap[obj, f];
+    assert res == FieldAccessFun(heap, obj, f);
+    return;
+}
+
+procedure UseHeap(heap : <a>[ref, Field a]a) {
+  var f1 : Field int; var f2 : Field bool; var obj : ref;
+  var x : int; var y : bool;
+
+  call x := FieldAccess(heap, f1, obj);  // error: wrong argument order
+  call x := FieldAccess(heap, obj, f1);
+  call y := FieldAccess(heap, obj, f2);
+
+  call y := FieldAccess(heap, obj, f1);  // error: wrong result type
+  call x := FieldAccess(heap, obj, obj); // error: wrong argument type
+}
+
+procedure injective<b>(heap : <a>[ref, Field a]a, obj0 : ref, obj1 : ref, f : Field b);
+   requires obj0 != obj1;
+   ensures heap[obj0, f] != heap[obj1, f];
+
+type ref;