1 files changed, 51 insertions, 51 deletions
diff --git a/Test/test2/FormulaTerm2.bpl b/Test/test2/FormulaTerm2.bpl
index 14ae5dab..8a2b0ceb 100644
--- a/Test/test2/FormulaTerm2.bpl
+++ b/Test/test2/FormulaTerm2.bpl
@@ -1,51 +1,51 @@
-// RUN: %boogie -noinfer "%s" > "%t"
-// RUN: %diff "%s.expect" "%t"
-// This file has been created to test some of the formula/term issues in Zap.
-// However, the test harness does not specify any particular prover to be used,
-// since these tests should pass regardless of which prover is used.
-
-procedure P()
-{
-  var a: int, b: int, t: bool;
-
-  start:
-    assume a == b;
-    t := a == b;
-    assert t;
-    return;
-}
-
-function f(bool) returns (int);
-const A: int;
-const B: int;
-
-axiom f(A < B) == 5;
-
-procedure Q()
-{
-  start:
-    assume A < B;
-    assert f(true) == 5;
-    return;
-}
-
-// ----- and now some erroneous procedures
-
-procedure PX()
-{
-  var a: int, b: int, t: bool;
-
-  start:
-    assume a == b;
-    t := a == b;
-    assert !t;  // error
-    return;
-}
-
-procedure QX()
-{
-  start:
-    assume A < B;
-    assert f(true) < 2;  // error
-    return;
-}
+// RUN: %boogie -noinfer "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+// This file has been created to test some of the formula/term issues in Zap.
+// However, the test harness does not specify any particular prover to be used,
+// since these tests should pass regardless of which prover is used.
+
+procedure P()
+{
+  var a: int, b: int, t: bool;
+
+  start:
+    assume a == b;
+    t := a == b;
+    assert t;
+    return;
+}
+
+function f(bool) returns (int);
+const A: int;
+const B: int;
+
+axiom f(A < B) == 5;
+
+procedure Q()
+{
+  start:
+    assume A < B;
+    assert f(true) == 5;
+    return;
+}
+
+// ----- and now some erroneous procedures
+
+procedure PX()
+{
+  var a: int, b: int, t: bool;
+
+  start:
+    assume a == b;
+    t := a == b;
+    assert !t;  // error
+    return;
+}
+
+procedure QX()
+{
+  start:
+    assume A < B;
+    assert f(true) < 2;  // error
+    return;
+}