Merging complete. Everything looks good *crosses fingers*

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;
+}