1 files changed, 49 insertions, 0 deletions
diff --git a/Test/test2/FormulaTerm2.bpl b/Test/test2/FormulaTerm2.bpl
new file mode 100644
index 00000000..6c5e4bf3
--- /dev/null
+++ b/Test/test2/FormulaTerm2.bpl
@@ -0,0 +1,49 @@
+// 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;
+}