4 files changed, 22 insertions, 1 deletions
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index 73fa07bf9..89dcc0a26 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -57,7 +57,10 @@ TESTS =	\
 	cbqi-lia-dt-simp.smt2 \
 	is-int.smt2 \
 	floor.smt2 \
-	array-unsat-simp3.smt2
+	array-unsat-simp3.smt2 \
+	mix-simp.smt2 \
+	mix-coeff.smt2  \
+	mix-match.smt2
 
 
 # regression can be solved with --finite-model-find --fmf-inst-engine
diff --git a/test/regress/regress0/quantifiers/mix-coeff.smt2 b/test/regress/regress0/quantifiers/mix-coeff.smt2
new file mode 100644
index 000000000..a20867b1c
--- /dev/null
+++ b/test/regress/regress0/quantifiers/mix-coeff.smt2
@@ -0,0 +1,4 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(assert (forall ((x Int) (y Int) (a Real) (z Int)) (or (> x (+ a (* (/ 2 3) y) (* (/ 4 5) z))) (< x (+ 10 (* 3 a) (* (/ 2 5) y) (* (/ 4 7) z))))))
+(check-sat)
+\ No newline at end of file
diff --git a/test/regress/regress0/quantifiers/mix-match.smt2 b/test/regress/regress0/quantifiers/mix-match.smt2
new file mode 100644
index 000000000..c6ac3b56f
--- /dev/null
+++ b/test/regress/regress0/quantifiers/mix-match.smt2
@@ -0,0 +1,10 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-fun P (Real) Bool)
+(assert (forall ((x Int)) (P x)))
+
+(declare-fun a () Real)
+(assert (is_int a))
+(assert (not (P a)))
+
+(check-sat)
+\ No newline at end of file
diff --git a/test/regress/regress0/quantifiers/mix-simp.smt2 b/test/regress/regress0/quantifiers/mix-simp.smt2
new file mode 100644
index 000000000..0b8c5067d
--- /dev/null
+++ b/test/regress/regress0/quantifiers/mix-simp.smt2
@@ -0,0 +1,4 @@
+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(assert (forall ((x Real)) (exists ((y Int)) (and (>= y x) (< y (+ x 1))))))
+(check-sat)