Enable regressions for CBQI BV and fix inverse for LSHR. (#1234)

This fixes and enables previously added regression tests for CBQI BV. It further removes one of the tests that was obsolete (since it goes through even without --cbqi-bv).

This further fixes the inverse computation for BITVECTOR_LSHR, which was broken due to a mismatching bit-width when creating a shift node.

8 files changed, 14 insertions, 12 deletions

diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp
index 9b84c8ecf..0795c3068 100644
--- a/src/theory/quantifiers/bv_inverter.cpp
+++ b/src/theory/quantifiers/bv_inverter.cpp
@@ -384,9 +384,10 @@ Node BvInverter::solve_bv_constraint(Node sv, Node sv_t, Node t, Kind rk,
            * with w = getSize(t) = getSize(s) and z = 0 with getSize(z) = w  */
           unsigned w = bv::utils::getSize(s);
           Node z = bv::utils::mkZero(w);
-          Node z_o_t =  nm->mkNode(BITVECTOR_CONCAT, z, t);
-          Node zot_shl_s = nm->mkNode(BITVECTOR_SHL, z_o_t, s);
-          Node ext = bv::utils::mkExtract(zot_shl_s, 2*w-1, w);
+          Node z_o_t = nm->mkNode(BITVECTOR_CONCAT, z, t);
+          Node z_o_s = nm->mkNode(BITVECTOR_CONCAT, z, s);
+          Node zot_shl_zos = nm->mkNode(BITVECTOR_SHL, z_o_t, z_o_s);
+          Node ext = bv::utils::mkExtract(zot_shl_zos, 2*w-1, w);
           scl = nm->mkNode(OR,
               nm->mkNode(EQUAL, s, z),
               nm->mkNode(EQUAL, ext, z));
diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am
index e045ad44c..3a8634d1e 100644
--- a/test/regress/regress0/quantifiers/Makefile.am
+++ b/test/regress/regress0/quantifiers/Makefile.am
@@ -91,6 +91,10 @@ TESTS =	\
 	psyco-001-bv.smt2 \
 	bug822.smt2 \
 	qbv-test-invert-mul.smt2 \
+	qbv-test-invert-bvand.smt2 \
+	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 \
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2
index 040bc33c1..d611fcd68 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvand.smt2
@@ -1,4 +1,5 @@
 ; COMMAND-LINE: --cbqi-bv
+; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
 (declare-fun a () (_ BitVec 32))
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 2fb5d9bec..d40e88248 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvlshr-0.smt2
@@ -1,4 +1,5 @@
 ; COMMAND-LINE: --cbqi-bv
+; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
 (declare-fun a () (_ BitVec 32))
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2
index c83b0ca73..287da08c7 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvor.smt2
@@ -1,4 +1,5 @@
 ; COMMAND-LINE: --cbqi-bv
+; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
 (declare-fun a () (_ BitVec 32))
diff --git a/test/regress/regress0/quantifiers/qbv-test-invert-bvult-0.smt2 b/test/regress/regress0/quantifiers/qbv-test-invert-bvult-0.smt2
deleted file mode 100644
index f54abccfd..000000000
--- a/test/regress/regress0/quantifiers/qbv-test-invert-bvult-0.smt2
+++ /dev/null
@@ -1,8 +0,0 @@
-; COMMAND-LINE: --cbqi-bv
-(set-logic BV)
-(set-info :status sat)
-(declare-fun a () (_ BitVec 32))
-
-(assert (forall ((x (_ BitVec 32))) (not (bvult x a) )))
-
-(check-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 a10f2fbea..13c1bf10a 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvult-1.smt2
@@ -1,4 +1,5 @@
 ; COMMAND-LINE: --cbqi-bv
+; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
 (declare-fun a () (_ BitVec 32))
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 6a1987c49..f7fe54e3e 100644
--- a/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1.smt2
+++ b/test/regress/regress0/quantifiers/qbv-test-invert-bvurem-1.smt2
@@ -1,4 +1,5 @@
-; COMMAND-LINE: --cbqi-bv
+; COMMAND-LINE: --cbqi-bv --bv-div-zero-const
+; EXPECT: sat
 (set-logic BV)
 (set-info :status sat)
 (declare-fun a () (_ BitVec 32))