1 files changed, 52 insertions, 52 deletions
diff --git a/Test/codeexpr/CodeExpr2.bpl b/Test/codeexpr/CodeExpr2.bpl
index 9d8beed7..0edaa8f4 100644
--- a/Test/codeexpr/CodeExpr2.bpl
+++ b/Test/codeexpr/CodeExpr2.bpl
@@ -1,52 +1,52 @@
-// RUN: %boogie "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-type T;
-const zero: T;
-
-function IsProperIndex(i: int, size: int): bool;
-
-procedure P(a: [int]T, n: int)
-  requires (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);
-{
-  call Q(a, n);
-}
-
-procedure Q(a: [int]T, n: int)
-  requires (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);
-{
-  call P(a, n);
-}
-
-procedure A(a: [int]T, n: int)
-{
-  assert
-    (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero)
-    ==>
-    (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);
-}
-
-procedure B(a: [int]T, n: int)
-{
-  assert
-    (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|)
-    ==>
-    (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);
-}
-
-procedure C(a: [int]T, n: int)
-{
-  Start:
-    assume (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);
-    goto Next;
-  Next:
-    assert (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);
-}
-
-procedure D(a: [int]T, n: int)
-{
-  Start:
-    assume (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);
-    goto Next;
-  Next:
-    assert (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);
-}
+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+type T;
+const zero: T;
+
+function IsProperIndex(i: int, size: int): bool;
+
+procedure P(a: [int]T, n: int)
+  requires (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);
+{
+  call Q(a, n);
+}
+
+procedure Q(a: [int]T, n: int)
+  requires (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);
+{
+  call P(a, n);
+}
+
+procedure A(a: [int]T, n: int)
+{
+  assert
+    (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero)
+    ==>
+    (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);
+}
+
+procedure B(a: [int]T, n: int)
+{
+  assert
+    (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|)
+    ==>
+    (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);
+}
+
+procedure C(a: [int]T, n: int)
+{
+  Start:
+    assume (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);
+    goto Next;
+  Next:
+    assert (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);
+}
+
+procedure D(a: [int]T, n: int)
+{
+  Start:
+    assume (forall i : int :: IsProperIndex(i, n) ==> |{ B: return a[i] == zero; }|);
+    goto Next;
+  Next:
+    assert (forall i : int :: IsProperIndex(i, n) ==> a[i] == zero);
+}