Removed division by constant handling for CBQI BV (unsound). (#1508)

This removes division by constant handling in the BV inverter introduced in #1498.
Division by constant was simplified to:
x / s OP t ---> x = t / s^-1 if s odd and there exists a multiplicative modular inverse s^-1.
This however, is incorrect since
x / s * 1 / s^-1 != x / (s * s^-1)

diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp
index 9559ffc451f5e10e93e2f5b7f279a2b37c2a9480..a96f05a356ca801ce9adf23a9cfc493b946b6624 100644 (file)
--- a/src/theory/quantifiers/bv_inverter.cpp
+++ b/src/theory/quantifiers/bv_inverter.cpp
@@ -2316,11 +2316,8 @@ Node BvInverter::solveBvLit(Node sv,
       {
         t_new = nm->mkNode(BITVECTOR_XOR, t, s);
       }
-      else if (k == BITVECTOR_MULT
-           || (k == BITVECTOR_UDIV_TOTAL && index == 0))
+      else if (k == BITVECTOR_MULT && s.isConst() && bv::utils::getBit(s, 0))
       {
-        if (s.isConst() && bv::utils::getBit(s, 0))
-        {
           unsigned w = bv::utils::getSize(s);
           Integer s_val = s.getConst<BitVector>().toInteger();
           Integer mod_val = Integer(1).multiplyByPow2(w);
@@ -2328,16 +2325,8 @@ Node BvInverter::solveBvLit(Node sv,
               << "Compute inverse : " << s_val << " " << mod_val << std::endl;
           Integer inv_val = s_val.modInverse(mod_val);
           Trace("bv-invert-debug") << "Inverse : " << inv_val << std::endl;
-          Node inv = nm->mkConst(BitVector(w, inv_val));
-          if (k == BITVECTOR_MULT)
-          {
-            t_new = nm->mkNode(BITVECTOR_MULT, inv, t);
-          }
-          else
-          {
-            t_new = nm->mkNode(BITVECTOR_UDIV_TOTAL, t, inv);
-          }
-        }
+          Node inv = bv::utils::mkConst(w, inv_val);
+          t_new = nm->mkNode(BITVECTOR_MULT, inv, t);
       }
 
       if (!t_new.isNull())