6 files changed, 40 insertions, 1 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 0b8a60495..66112defc 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -14,13 +14,18 @@ TESTS =	\
 	ite_real_valid.smt \
 	let.smt \
 	let2.smt \
-	simple2.smt \
 	simple.smt \
+	simple2.smt \
+        simple-lra.smt \
+        simple-rdl.smt \
 	simple-uf.smt \
 	ite.smt2 \
 	ite2.smt2 \
 	ite3.smt2 \
 	ite4.smt2 \
+        simple-lra.smt2 \
+        simple-rdl.smt2 \
+	simple-uf.smt2 \
 	bug32.cvc \
 	hole6.cvc \
 	logops.01.cvc \
diff --git a/test/regress/regress0/simple-lra.smt b/test/regress/regress0/simple-lra.smt
new file mode 100644
index 000000000..c80632a96
--- /dev/null
+++ b/test/regress/regress0/simple-lra.smt
@@ -0,0 +1,6 @@
+(benchmark simple_lra
+  :logic QF_LRA
+  :status unsat
+  :extrafuns ((x Real) (y Real))
+  :formula (not (implies (and (> x 0) (< (* 2 x) y)) (and (> y 0) (< x y))))
+)
diff --git a/test/regress/regress0/simple-lra.smt2 b/test/regress/regress0/simple-lra.smt2
new file mode 100644
index 000000000..585c62954
--- /dev/null
+++ b/test/regress/regress0/simple-lra.smt2
@@ -0,0 +1,6 @@
+(set-logic QF_LRA)
+(set-info :status unsat)
+(declare-fun x () Real)
+(declare-fun y () Real)
+(assert (not (=> (and (> x 0) (< (* 2 x) y)) (and (> y 0) (< x y)))))
+(check-sat)
diff --git a/test/regress/regress0/simple-rdl.smt b/test/regress/regress0/simple-rdl.smt
new file mode 100644
index 000000000..080c69f93
--- /dev/null
+++ b/test/regress/regress0/simple-rdl.smt
@@ -0,0 +1,6 @@
+(benchmark simple_rdl
+  :logic QF_RDL
+  :status unsat
+  :extrafuns ((x Real) (y Real))
+  :formula (not (implies (< (- x y) 0) (< x y)))
+)
diff --git a/test/regress/regress0/simple-rdl.smt2 b/test/regress/regress0/simple-rdl.smt2
new file mode 100644
index 000000000..d2c0a4cde
--- /dev/null
+++ b/test/regress/regress0/simple-rdl.smt2
@@ -0,0 +1,7 @@
+(set-logic QF_RDL)
+(set-info :status unsat)
+(declare-fun x () Real)
+(declare-fun y () Real)
+(assert (not (=> (< (- x y) 0) (< x y))))
+(check-sat)
+
diff --git a/test/regress/regress0/simple-uf.smt2 b/test/regress/regress0/simple-uf.smt2
new file mode 100644
index 000000000..ef3b3cf86
--- /dev/null
+++ b/test/regress/regress0/simple-uf.smt2
@@ -0,0 +1,9 @@
+(set-logic QF_UF)
+(set-info :status unsat)
+(declare-sort A 0)
+(declare-sort B 0)
+(declare-fun x () A)
+(declare-fun y () A)
+(declare-fun f (A) B)
+(assert (not (=> (= x y) (= (f x) (f y)))))
+(check-sat)