Added division by constant handling for CBQI BV. (#1498)

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