1 files changed, 36 insertions, 36 deletions
diff --git a/Test/test2/ContractEvaluationOrder.bpl b/Test/test2/ContractEvaluationOrder.bpl
index 8719dcfa..4115c4b0 100644
--- a/Test/test2/ContractEvaluationOrder.bpl
+++ b/Test/test2/ContractEvaluationOrder.bpl
@@ -1,36 +1,36 @@
-// RUN: %boogie "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-procedure P() returns (x, y: int)
-  ensures x == y;  // ensured by the body
-  ensures x == 0;  // error: not ensured by the body
-  ensures y == 0;  // follows from the previous two ensures clauses (provided they are
-                   // indeed evaluated in this order, which they are supposed to be)
-{
-  x := y;
-}
-
-procedure Q() returns (x, y: int)
-{
-  x := y;
-
-  assert x == y;  // ensured by the body
-  assert x == 0;  // error: not ensured by the body
-  assert y == 0;  // follows from the previous two asserts (provided they are
-                  // indeed evaluated in this order, which they are supposed to be)
-}
-
-procedure R()
-{
-  var a, b: int;
-  a := b;
-  call S(a, b);
-}
-
-procedure S(x, y: int)
-                    // In the call from R:
-  requires x == y;  // ensured by the body of R
-  requires x == 0;  // error: not ensured by the body of R
-  requires y == 0;  // follows from the previous two requires clauses (provided they are
-                    // indeed evaluated in this order, which they are supposed to be)
-{
-}
+// RUN: %boogie "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+procedure P() returns (x, y: int)
+  ensures x == y;  // ensured by the body
+  ensures x == 0;  // error: not ensured by the body
+  ensures y == 0;  // follows from the previous two ensures clauses (provided they are
+                   // indeed evaluated in this order, which they are supposed to be)
+{
+  x := y;
+}
+
+procedure Q() returns (x, y: int)
+{
+  x := y;
+
+  assert x == y;  // ensured by the body
+  assert x == 0;  // error: not ensured by the body
+  assert y == 0;  // follows from the previous two asserts (provided they are
+                  // indeed evaluated in this order, which they are supposed to be)
+}
+
+procedure R()
+{
+  var a, b: int;
+  a := b;
+  call S(a, b);
+}
+
+procedure S(x, y: int)
+                    // In the call from R:
+  requires x == y;  // ensured by the body of R
+  requires x == 0;  // error: not ensured by the body of R
+  requires y == 0;  // follows from the previous two requires clauses (provided they are
+                    // indeed evaluated in this order, which they are supposed to be)
+{
+}