3 files changed, 27 insertions, 2 deletions
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index 3a8634d1e..14e5244b4 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -95,13 +95,16 @@ TESTS =	\
 	qbv-test-invert-bvor.smt2 \
 	qbv-test-invert-bvlshr-0.smt2 \
  	qbv-test-invert-bvurem-1.smt2 \
-	qbv-simple-2vars-vo.smt2 \
 	qbv-test-invert-concat-0.smt2 \
 	qbv-test-invert-concat-1.smt2 \
 	qbv-test-invert-shl.smt2 \
 	qbv-test-invert-udiv-0.smt2 \
 	qbv-test-invert-udiv-1.smt2 \
-	qbv-test-urem-rewrite.smt2
+	qbv-simple-2vars-vo.smt2 \
+	qbv-test-urem-rewrite.smt2 \
+	qbv-inequality2.smt2 \
+	qbv-test-invert-bvult-1.smt2
+ 
 
 # regression can be solved with --finite-model-find --fmf-inst-engine
 # set3.smt2
diff --git a/test/regress/regress0/quantifiers/qbv-inequality2.smt2 b/test/regress/regress0/quantifiers/qbv-inequality2.smt2
new file mode 100644
index 000000000..d53715a2d
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-inequality2.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --cbqi-bv
+; EXPECT: sat
+(set-logic BV)
+(set-info :status sat)
+(declare-fun a () (_ BitVec 32))
+(declare-fun b () (_ BitVec 32))
+
+
+(assert (forall ((x (_ BitVec 32))) (or (bvuge x (bvadd a b)) (bvule x b))))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2 b/test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2
new file mode 100644
index 000000000..d74a6cfea
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --cbqi-bv
+; EXPECT: sat
+(set-logic BV)
+(set-info :status sat)
+(declare-fun a () (_ BitVec 3))
+(declare-fun b () (_ BitVec 3))
+(declare-fun c () (_ BitVec 3))
+
+(assert (forall ((x (_ BitVec 3))) (or (not (= (bvmul x a) b)) (bvuge x c))))
+
+(check-sat)