Add explicit disequality handling when generating side condition for CBQI BV. (#1447)

This refactors solveBvLit to support explicit handling of disequalities (and, in the next step, inequalities) when generating side conditions.

43 files changed, 301 insertions, 114 deletions

diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index c59570651..bb43d6c1c 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -90,25 +90,38 @@ TESTS =	\
 	qbv-simp.smt2 \
 	psyco-001-bv.smt2 \
 	bug822.smt2 \
-	qbv-test-invert-mul.smt2 \
+	qbv-disequality3.smt2 \
+	qbv-inequality2.smt2 \
+	qbv-simple-2vars-vo.smt2 \
+	qbv-test-invert-bvadd-neq.smt2 \
 	qbv-test-invert-bvand.smt2 \
-	qbv-test-invert-bvcomp.smt2 \
-	qbv-test-invert-bvor.smt2 \
-	qbv-test-invert-bvlshr-0.smt2 \
+	qbv-test-invert-bvand-neq.smt2 \
 	qbv-test-invert-bvashr-0.smt2 \
+	qbv-test-invert-bvashr-0-neq.smt2 \
+	qbv-test-invert-bvashr-1.smt2 \
+	qbv-test-invert-bvashr-1-neq.smt2 \
+	qbv-test-invert-bvlshr-0.smt2 \
+	qbv-test-invert-bvlshr-0-neq.smt2 \
+	qbv-test-invert-bvlshr-1.smt2 \
+	qbv-test-invert-bvlshr-1-neq.smt2 \
+	qbv-test-invert-bvmul.smt2 \
+	qbv-test-invert-bvmul-neq.smt2 \
+	qbv-test-invert-bvor.smt2 \
+	qbv-test-invert-bvor-neq.smt2 \
+	qbv-test-invert-bvshl-0.smt2 \
+	qbv-test-invert-bvudiv-0.smt2 \
+	qbv-test-invert-bvudiv-0-neq.smt2 \
+	qbv-test-invert-bvudiv-1.smt2 \
+	qbv-test-invert-bvudiv-1-neq.smt2 \
+	qbv-test-invert-bvult-1.smt2 \
  	qbv-test-invert-bvurem-1.smt2 \
+	qbv-test-invert-bvurem-1-neq.smt2 \
+	qbv-test-invert-bvxor.smt2 \
+	qbv-test-invert-bvxor-neq.smt2 \
 	qbv-test-invert-concat-0.smt2 \
 	qbv-test-invert-concat-1.smt2 \
-	qbv-test-invert-disequality.smt2 \
-	qbv-test-invert-shl.smt2 \
-	qbv-test-invert-udiv-0.smt2 \
-	qbv-test-invert-udiv-1.smt2 \
 	qbv-test-invert-sign-extend.smt2 \
-	qbv-test-invert-bvxor.smt2 \
-	qbv-simple-2vars-vo.smt2 \
 	qbv-test-urem-rewrite.smt2 \
-	qbv-inequality2.smt2 \
-	qbv-test-invert-bvult-1.smt2 \
 	intersection-example-onelane.proof-node22337.smt2 \
  	nested9_true-unreach-call.i_575.smt2 \
  	small-pipeline-fixpoint-3.smt2 \
@@ -127,6 +140,8 @@ TESTS =	\
 # regression can be solved with --finite-model-find --fmf-inst-engine
 # set3.smt2
 
+# disabled since bvcomp handling is currently disabled
+# qbv-test-invert-bvcomp.smt2
 
 # removed because they take more than 20s
 #		javafe.ast.ArrayInit.35.smt2
diff --git a/test/regress/regress0/quantifiers/qbv-disequality3.smt2 b/test/regress/regress0/quantifiers/qbv-disequality3.smt2
new file mode 100644
index 000000000..d16157509
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-disequality3.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; EXPECT: sat
+(set-logic BV)
+(set-info :status sat)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+
+(assert (forall ((x (_ BitVec 8))) (= (bvmul (bvadd x b) a)  b)))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-inequality2.smt2 b/test/regress/regress0/quantifiers/qbv-inequality2.smt2
index d53715a2d..1486e176d 100644
--- a/test/regress/regress0/quantifiers/qbv-inequality2.smt2
+++ b/test/regress/regress0/quantifiers/qbv-inequality2.smt2
@@ -1,11 +1,10 @@
-; COMMAND-LINE: --cbqi-bv
+; COMMAND-LINE: --cbqi-bv --no-cbqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
-(declare-fun a () (_ BitVec 32))
-(declare-fun b () (_ BitVec 32))
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
 
-
-(assert (forall ((x (_ BitVec 32))) (or (bvuge x (bvadd a b)) (bvule x b))))
+(assert (forall ((x (_ BitVec 8))) (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
index d74a6cfea..3c4f93243 100644
--- a/test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2
+++ b/test/regress/regress0/quantifiers/qbv-multi-lit-uge.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv
+; COMMAND-LINE: --cbqi-bv --no-cbqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress0/quantifiers/qbv-simp.smt2 b/test/regress/regress0/quantifiers/qbv-simp.smt2
index 1f72d44e4..ec4626f52 100644
--- a/test/regress/regress0/quantifiers/qbv-simp.smt2
+++ b/test/regress/regress0/quantifiers/qbv-simp.smt2
@@ -1,9 +1,11 @@
+; COMMAND-LINE: --cbqi-bv --no-cbqi-full
+; EXPECT: unsat
 (set-logic BV)
 (set-info :status unsat)
 (assert
    (forall
-    ((A (_ BitVec 32)) (B (_ BitVec 32)) (C (_ BitVec 32)) (D (_ BitVec 32)))
+    ((A (_ BitVec 8)) (B (_ BitVec 8)) (C (_ BitVec 8)) (D (_ BitVec 8)))
       (or (and (= A B) (= C D)) (and (= A C) (= B D)))))
-      
+
 (check-sat)
-      
+
diff --git a/test/regress/regress0/quantifiers/qbv-simple-2vars-vo.smt2 b/test/regress/regress0/quantifiers/qbv-simple-2vars-vo.smt2
index b6ae95fec..c36322aac 100644
--- a/test/regress/regress0/quantifiers/qbv-simple-2vars-vo.smt2
+++ b/test/regress/regress0/quantifiers/qbv-simple-2vars-vo.smt2
@@ -1,16 +1,16 @@
-; COMMAND-LINE: --cbqi-bv
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
-(declare-fun a () (_ BitVec 32))
-(declare-fun b () (_ BitVec 32))
-(declare-fun c () (_ BitVec 32))
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+(declare-fun c () (_ BitVec 8))
 
-(assert (not (= a #x00000000)))
+(assert (not (= a #x00)))
 
-(assert (forall ((x (_ BitVec 32)) (y (_ BitVec 32))) (or 
-(not (= (bvmul x y) #x0000000A))
-(not (= (bvadd y a) #x00000010))
+(assert (forall ((x (_ BitVec 8)) (y (_ BitVec 8))) (or 
+(not (= (bvmul x y) #x0A))
+(not (= (bvadd y a) #x10))
 )))
 
 (check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvadd-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvadd-neq.smt2
new file mode 100644
index 000000000..216a98531
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvadd-neq.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; EXPECT: unsat
+(set-logic BV)
+(set-info :status unsat)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+
+(assert (forall ((x (_ BitVec 8))) (= (bvadd x a) b)))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvand-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvand-neq.smt2
new file mode 100644
index 000000000..ad3b9a9e5
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvand-neq.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; EXPECT: sat
+(set-logic BV)
+(set-info :status sat)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+
+(assert (forall ((x (_ BitVec 8))) (= (bvand x a) b)))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2
index d611fcd68..8dd50b1be 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2
@@ -1,10 +1,10 @@
-; COMMAND-LINE: --cbqi-bv
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
-(declare-fun a () (_ BitVec 32))
-(declare-fun b () (_ BitVec 32))
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
 
-(assert (forall ((x (_ BitVec 32))) (not (= (bvand x a) b))))
+(assert (forall ((x (_ BitVec 8))) (not (= (bvand x a) b))))
 
 (check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0-neq.smt2
new file mode 100644
index 000000000..e05c3446d
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0-neq.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; EXPECT: unsat
+(set-logic BV)
+(set-info :status unsat)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+
+(assert (forall ((x (_ BitVec 8))) (= (bvashr x a) b)))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0.smt2
index db7725896..30e7c2f8b 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-0.smt2
@@ -1,10 +1,10 @@
-; COMMAND-LINE: --cbqi-bv
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
-(declare-fun a () (_ BitVec 32))
-(declare-fun b () (_ BitVec 32))
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
 
-(assert (forall ((x (_ BitVec 32))) (not (= (bvashr x a) b))))
+(assert (forall ((x (_ BitVec 8))) (not (= (bvashr x a) b))))
 
 (check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1-neq.smt2
new file mode 100644
index 000000000..2835e5956
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1-neq.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; EXPECT: sat
+(set-logic BV)
+(set-info :status sat)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+
+(assert (forall ((x (_ BitVec 8))) (= (bvashr a x) b)))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1.smt2
new file mode 100644
index 000000000..c3de64c4c
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvashr-1.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; EXPECT: sat
+(set-logic BV)
+(set-info :status sat)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+
+(assert (forall ((x (_ BitVec 8))) (not (= (bvashr a x) b))))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvcomp.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvcomp.smt2
index e8f7c25db..3b55c0b9a 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-bvcomp.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvcomp.smt2
@@ -1,11 +1,11 @@
-; COMMAND-LINE: --cbqi-bv
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
 ; EXPECT: unsat
 (set-logic BV)
 (set-info :status sat)
-(declare-fun a () (_ BitVec 32))
-(declare-fun b () (_ BitVec 32))
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
 (declare-fun c () (_ BitVec 1))
 
-(assert (forall ((x (_ BitVec 32))) (not (= (bvcomp x a) (bvcomp x b)))))
+(assert (forall ((x (_ BitVec 8))) (not (= (bvcomp x a) ((_ extract 7 7) (bvmul a b))))))
 
 (check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0-neq.smt2
new file mode 100644
index 000000000..e05c3446d
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0-neq.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; EXPECT: unsat
+(set-logic BV)
+(set-info :status unsat)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+
+(assert (forall ((x (_ BitVec 8))) (= (bvashr x a) b)))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2
index db7725896..1018ce72c 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2
@@ -1,10 +1,10 @@
-; COMMAND-LINE: --cbqi-bv
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
-(declare-fun a () (_ BitVec 32))
-(declare-fun b () (_ BitVec 32))
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
 
-(assert (forall ((x (_ BitVec 32))) (not (= (bvashr x a) b))))
+(assert (forall ((x (_ BitVec 8))) (not (= (bvlshr x a) b))))
 
 (check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1-neq.smt2
new file mode 100644
index 000000000..503bc9852
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1-neq.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; EXPECT: sat
+(set-logic BV)
+(set-info :status sat)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+
+(assert (forall ((x (_ BitVec 8))) (= (bvlshr a x) b)))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1.smt2
new file mode 100644
index 000000000..08479d90e
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-1.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; EXPECT: sat
+(set-logic BV)
+(set-info :status sat)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+
+(assert (forall ((x (_ BitVec 8))) (not (= (bvlshr a x) b))))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvmul-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvmul-neq.smt2
new file mode 100644
index 000000000..9dc9f98ac
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvmul-neq.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; EXPECT: sat
+(set-logic BV)
+(set-info :status sat)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+
+(assert (forall ((x (_ BitVec 8))) (= (bvmul x a) b)))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvmul.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvmul.smt2
new file mode 100644
index 000000000..f3dad679b
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvmul.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; EXPECT: sat
+(set-logic BV)
+(set-info :status sat)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+
+(assert (forall ((x (_ BitVec 8))) (not (= (bvmul x a) b))))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvor-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvor-neq.smt2
new file mode 100644
index 000000000..74c2891cf
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvor-neq.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; EXPECT: sat
+(set-logic BV)
+(set-info :status sat)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+
+(assert (forall ((x (_ BitVec 8))) (= (bvor x a) b)))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2
index 287da08c7..4145c68b1 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2
@@ -1,10 +1,10 @@
-; COMMAND-LINE: --cbqi-bv
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
-(declare-fun a () (_ BitVec 32))
-(declare-fun b () (_ BitVec 32))
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
 
-(assert (forall ((x (_ BitVec 32))) (not (= (bvor x a) b))))
+(assert (forall ((x (_ BitVec 8))) (not (= (bvor x a) b))))
 
 (check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0-neq.smt2
new file mode 100644
index 000000000..e85ecc7de
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0-neq.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; EXPECT: sat
+(set-logic BV)
+(set-info :status sat)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+
+(assert (forall ((x (_ BitVec 8))) (= (bvshl x a) b)))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0.smt2
new file mode 100644
index 000000000..abef84da2
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvshl-0.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; EXPECT: sat
+(set-logic BV)
+(set-info :status sat)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+
+(assert (forall ((x (_ BitVec 8))) (not (= (bvshl x a) b))))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-0-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-0-neq.smt2
new file mode 100644
index 000000000..3748eca24
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-0-neq.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; EXPECT: unsat
+(set-logic BV)
+(set-info :status unsat)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+
+(assert (distinct a b (_ bv0 8)))
+(assert (forall ((x (_ BitVec 8))) (= (bvudiv x a) b)))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-0.smt2
new file mode 100644
index 000000000..2cabb502e
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-0.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; EXPECT: sat
+(set-logic BV)
+(set-info :status sat)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+
+(assert (distinct a b (_ bv0 8)))
+(assert (forall ((x (_ BitVec 8))) (not (= (bvudiv x a) b))))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-1-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-1-neq.smt2
new file mode 100644
index 000000000..a0e1b62c2
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-1-neq.smt2
@@ -0,0 +1,11 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full --bv-div-zero-const
+; EXPECT: unsat
+(set-logic BV)
+(set-info :status unsat)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+
+(assert (distinct a b (_ bv0 8)))
+(assert (forall ((x (_ BitVec 8))) (= (bvudiv a x) b)))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-udiv-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-1.smt2
index bf69a8b4a..2690a0ac9 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-udiv-1.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvudiv-1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --bv-div-zero-const
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full --bv-div-zero-const
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2
index 13c1bf10a..a1dca469a 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2
@@ -1,9 +1,9 @@
-; COMMAND-LINE: --cbqi-bv
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
-(declare-fun a () (_ BitVec 32))
+(declare-fun a () (_ BitVec 8))
 
-(assert (forall ((x (_ BitVec 32))) (not (bvult a x))))
+(assert (forall ((x (_ BitVec 8))) (not (bvult a x))))
 
 (check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1-neq.smt2
new file mode 100644
index 000000000..871df4827
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1-neq.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; EXPECT: sat
+(set-logic BV)
+(set-info :status sat)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
+
+(assert (forall ((x (_ BitVec 8))) (= (bvurem a x) b)))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1.smt2
index f7fe54e3e..22bd306ee 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1.smt2
@@ -1,10 +1,10 @@
-; COMMAND-LINE: --cbqi-bv --bv-div-zero-const
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
-(declare-fun a () (_ BitVec 32))
-(declare-fun b () (_ BitVec 32))
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 8))
 
-(assert (forall ((x (_ BitVec 32))) (not (= (bvurem a x) b))))
+(assert (forall ((x (_ BitVec 8))) (not (= (bvurem a x) b))))
 
 (check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvxor-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvxor-neq.smt2
new file mode 100644
index 000000000..4f9c6edc3
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvxor-neq.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; EXPECT: unsat
+(set-logic BV)
+(set-info :status unsat)
+(declare-fun a () (_ BitVec 8))
+
+(assert (forall ((x (_ BitVec 8))) (not (= (bvxor x a) (bvmul a a)))))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2
index eec40a425..ef41eecdd 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvxor.smt2
@@ -1,9 +1,9 @@
-; COMMAND-LINE: --cbqi-bv
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
 ; EXPECT: unsat
 (set-logic BV)
 (set-info :status sat)
-(declare-fun a () (_ BitVec 32))
+(declare-fun a () (_ BitVec 8))
 
-(assert (forall ((x (_ BitVec 32))) (not (= (bvxor x a) (bvmul a a)))))
+(assert (forall ((x (_ BitVec 8))) (not (= (bvxor x a) (bvmul a a)))))
 
 (check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-concat-0-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-concat-0-neq.smt2
new file mode 100644
index 000000000..769854f6f
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-concat-0-neq.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; EXPECT: unsat
+(set-logic BV)
+(set-info :status unsat)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 16))
+
+(assert (forall ((x (_ BitVec 8))) (= (concat x a) b)))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-concat-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-concat-0.smt2
index f4e19fc52..7b66bd859 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-concat-0.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-concat-0.smt2
@@ -1,10 +1,10 @@
-; COMMAND-LINE: --cbqi-bv
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
-(declare-fun a () (_ BitVec 32))
-(declare-fun b () (_ BitVec 64))
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 16))
 
-(assert (forall ((x (_ BitVec 32))) (not (= (concat x a) b))))
+(assert (forall ((x (_ BitVec 8))) (not (= (concat x a) b))))
 
 (check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-concat-1-neq.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-concat-1-neq.smt2
new file mode 100644
index 000000000..7dab5637e
--- /dev/null
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-concat-1-neq.smt2
@@ -0,0 +1,10 @@
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
+; EXPECT: unsat
+(set-logic BV)
+(set-info :status unsat)
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 16))
+
+(assert (forall ((x (_ BitVec 8))) (= (concat a x) b)))
+
+(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-concat-1.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-concat-1.smt2
index 827e74605..13fb3e1c2 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-concat-1.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-concat-1.smt2
@@ -1,10 +1,10 @@
-; COMMAND-LINE: --cbqi-bv
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
-(declare-fun a () (_ BitVec 32))
-(declare-fun b () (_ BitVec 64))
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 16))
 
-(assert (forall ((x (_ BitVec 32))) (not (= (concat a x) b))))
+(assert (forall ((x (_ BitVec 8))) (not (= (concat a x) b))))
 
 (check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-disequality.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-disequality.smt2
deleted file mode 100644
index 6ba782597..000000000
--- a/test/regress/regress0/quantifiers/qbv-test-invert-disequality.smt2
+++ /dev/null
@@ -1,10 +0,0 @@
-; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep
-; EXPECT: sat
-(set-logic BV)
-(set-info :status sat)
-(declare-fun a () (_ BitVec 32))
-(declare-fun b () (_ BitVec 32))
-
-(assert (forall ((x (_ BitVec 32))) (= (bvand x a) b)))
-
-(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-mul.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-mul.smt2
deleted file mode 100644
index 84e9fa7ce..000000000
--- a/test/regress/regress0/quantifiers/qbv-test-invert-mul.smt2
+++ /dev/null
@@ -1,10 +0,0 @@
-; 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))) (not (= (bvmul x a) b))))
-
-(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-shl.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-shl.smt2
deleted file mode 100644
index 97a0662eb..000000000
--- a/test/regress/regress0/quantifiers/qbv-test-invert-shl.smt2
+++ /dev/null
@@ -1,10 +0,0 @@
-; 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))) (not (= (bvshl x a) b))))
-
-(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-sign-extend.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-sign-extend.smt2
index 21aa519ad..43019c4cb 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-sign-extend.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-sign-extend.smt2
@@ -1,10 +1,10 @@
-; COMMAND-LINE: --cbqi-bv
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
-(declare-fun a () (_ BitVec 32))
-(declare-fun b () (_ BitVec 64))
+(declare-fun a () (_ BitVec 8))
+(declare-fun b () (_ BitVec 16))
 
-(assert (forall ((x (_ BitVec 32))) (not (= ((_ sign_extend 32) x) b))))
+(assert (forall ((x (_ BitVec 8))) (not (= ((_ sign_extend 8) x) b))))
 
 (check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-udiv-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-udiv-0.smt2
deleted file mode 100644
index becfc5315..000000000
--- a/test/regress/regress0/quantifiers/qbv-test-invert-udiv-0.smt2
+++ /dev/null
@@ -1,11 +0,0 @@
-; COMMAND-LINE: --cbqi-bv --bv-div-zero-const
-; EXPECT: sat
-(set-logic BV)
-(set-info :status sat)
-(declare-fun a () (_ BitVec 16))
-(declare-fun b () (_ BitVec 16))
-
-(assert (distinct a b (_ bv0 16)))
-(assert (forall ((x (_ BitVec 16))) (not (= (bvudiv x a) b))))
-
-(check-sat)
diff --git a/test/regress/regress0/quantifiers/qbv-test-urem-rewrite.smt2 b/test/regress/regress0/quantifiers/qbv-test-urem-rewrite.smt2
index 6df69d80b..e57352b8f 100644
--- a/test/regress/regress0/quantifiers/qbv-test-urem-rewrite.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-urem-rewrite.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cbqi-bv --bv-div-zero-const
+; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=keep --no-cbqi-full
 ; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)