10 files changed, 62 insertions, 46 deletions
diff --git a/test/regress/regress0/uflra/bug293.cvc b/test/regress/regress0/uflra/bug293.cvc
deleted file mode 100644
index 6da025fbd..000000000
--- a/test/regress/regress0/uflra/bug293.cvc
+++ /dev/null
@@ -1,7 +0,0 @@
-% EXPECT: unsat
-x: REAL;
-f: REAL -> REAL;
-ASSERT NOT (f(1) = f(x));
-ASSERT NOT (f(0) = f(x));
-ASSERT (x = 0) XOR (x = 1);
-CHECKSAT;
-\ No newline at end of file
diff --git a/test/regress/regress0/uflra/bug293.cvc.smt2 b/test/regress/regress0/uflra/bug293.cvc.smt2
new file mode 100644
index 000000000..c3070ed06
--- /dev/null
+++ b/test/regress/regress0/uflra/bug293.cvc.smt2
@@ -0,0 +1,9 @@
+; EXPECT: unsat
+(set-logic ALL)
+(set-option :incremental false)
+(declare-fun x () Real)
+(declare-fun f (Real) Real)
+(assert (not (= (f 1) (f x))))
+(assert (not (= (f 0) (f x))))
+(assert (xor (= x 0) (= x 1)))
+(check-sat)
diff --git a/test/regress/regress0/uflra/simple.01.cvc b/test/regress/regress0/uflra/simple.01.cvc
deleted file mode 100644
index 62e48290e..000000000
--- a/test/regress/regress0/uflra/simple.01.cvc
+++ /dev/null
@@ -1,5 +0,0 @@
-% EXPECT: sat
-x, y: REAL;
-f: REAL -> REAL;
-
-CHECKSAT NOT (f(x) = f(y));
-\ No newline at end of file
diff --git a/test/regress/regress0/uflra/simple.01.cvc.smt2 b/test/regress/regress0/uflra/simple.01.cvc.smt2
new file mode 100644
index 000000000..44c1944c0
--- /dev/null
+++ b/test/regress/regress0/uflra/simple.01.cvc.smt2
@@ -0,0 +1,14 @@
+; EXPECT: sat
+(set-logic ALL)
+(set-option :incremental true)
+(declare-fun x () Real)
+(declare-fun y () Real)
+(declare-fun f (Real) Real)
+(push 1)
+
+(assert (not (= (f x) (f y))))
+
+(check-sat)
+
+(pop 1)
+
diff --git a/test/regress/regress0/uflra/simple.02.cvc b/test/regress/regress0/uflra/simple.02.cvc
deleted file mode 100644
index 8bc20f36a..000000000
--- a/test/regress/regress0/uflra/simple.02.cvc
+++ /dev/null
@@ -1,9 +0,0 @@
-% EXPECT: unsat
-x, y: REAL;
-f: REAL -> REAL;
-
-ASSERT (x <= y);
-ASSERT (y <= x);
-ASSERT NOT (f(x) = f(y));
-
-CHECKSAT;
-\ No newline at end of file
diff --git a/test/regress/regress0/uflra/simple.02.cvc.smt2 b/test/regress/regress0/uflra/simple.02.cvc.smt2
new file mode 100644
index 000000000..a71b7f634
--- /dev/null
+++ b/test/regress/regress0/uflra/simple.02.cvc.smt2
@@ -0,0 +1,10 @@
+; EXPECT: unsat
+(set-logic ALL)
+(set-option :incremental false)
+(declare-fun x () Real)
+(declare-fun y () Real)
+(declare-fun f (Real) Real)
+(assert (<= x y))
+(assert (<= y x))
+(assert (not (= (f x) (f y))))
+(check-sat)
diff --git a/test/regress/regress0/uflra/simple.03.cvc b/test/regress/regress0/uflra/simple.03.cvc
deleted file mode 100644
index 2ecf9b0a8..000000000
--- a/test/regress/regress0/uflra/simple.03.cvc
+++ /dev/null
@@ -1,11 +0,0 @@
-% EXPECT: sat
-x1, y1, z1: REAL;
-x2, y2, z2: REAL;
-f: REAL -> REAL;
-g: (REAL, REAL) -> REAL;
-
-ASSERT (z1 = f(x1));
-ASSERT (z2 = f(y1));
-ASSERT NOT (g(z1, z2) = g(z2, y2));
-
-CHECKSAT;
-\ No newline at end of file
diff --git a/test/regress/regress0/uflra/simple.03.cvc.smt2 b/test/regress/regress0/uflra/simple.03.cvc.smt2
new file mode 100644
index 000000000..1a61a1dc5
--- /dev/null
+++ b/test/regress/regress0/uflra/simple.03.cvc.smt2
@@ -0,0 +1,15 @@
+; EXPECT: sat
+(set-logic ALL)
+(set-option :incremental false)
+(declare-fun x1 () Real)
+(declare-fun y1 () Real)
+(declare-fun z1 () Real)
+(declare-fun x2 () Real)
+(declare-fun y2 () Real)
+(declare-fun z2 () Real)
+(declare-fun f (Real) Real)
+(declare-fun g (Real Real) Real)
+(assert (= z1 (f x1)))
+(assert (= z2 (f y1)))
+(assert (not (= (g z1 z2) (g z2 y2))))
+(check-sat)
diff --git a/test/regress/regress0/uflra/simple.04.cvc b/test/regress/regress0/uflra/simple.04.cvc
deleted file mode 100644
index e363a9606..000000000
--- a/test/regress/regress0/uflra/simple.04.cvc
+++ /dev/null
@@ -1,14 +0,0 @@
-% EXPECT: unsat
-x1, x2: REAL;
-y1, y2: REAL;
-f: REAL -> REAL;
-g: (REAL, REAL) -> REAL;
-
-ASSERT (x1 <= x2) AND (x2 <= x1);
-
-ASSERT NOT (g(x1, y1) = g(x2, y2));
-
-ASSERT (y1 <= f(x1)) AND (f(x1) <= y1);
-ASSERT (y2 <= f(x2)) AND (f(x2) <= y2);
-
-CHECKSAT;
-\ No newline at end of file
diff --git a/test/regress/regress0/uflra/simple.04.cvc.smt2 b/test/regress/regress0/uflra/simple.04.cvc.smt2
new file mode 100644
index 000000000..527746881
--- /dev/null
+++ b/test/regress/regress0/uflra/simple.04.cvc.smt2
@@ -0,0 +1,14 @@
+; EXPECT: unsat
+(set-logic ALL)
+(set-option :incremental false)
+(declare-fun x1 () Real)
+(declare-fun x2 () Real)
+(declare-fun y1 () Real)
+(declare-fun y2 () Real)
+(declare-fun f (Real) Real)
+(declare-fun g (Real Real) Real)
+(assert (and (<= x1 x2) (<= x2 x1)))
+(assert (not (= (g x1 y1) (g x2 y2))))
+(assert (let ((_let_1 (f x1))) (and (<= y1 _let_1) (<= _let_1 y1))))
+(assert (let ((_let_1 (f x2))) (and (<= y2 _let_1) (<= _let_1 y2))))
+(check-sat)