Fix MULT handling for CBQI BV. (#1531)

diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp
index cf16efbfa3db04e424d87091e8158df57466ea4f..975016d34b6ee136f50e441f025bcc2f25ee4637 100644 (file)
--- a/src/theory/quantifiers/bv_inverter.cpp
+++ b/src/theory/quantifiers/bv_inverter.cpp
@@ -2897,7 +2897,8 @@ Node BvInverter::solveBvLit(Node sv,
     {
       t = nm->mkNode(BITVECTOR_XOR, t, s);
     }
-    else if (k == BITVECTOR_MULT && s.isConst() && bv::utils::getBit(s, 0))
+    else if (litk == EQUAL && k == BITVECTOR_MULT
+             && s.isConst() && bv::utils::getBit(s, 0))
     {
       unsigned w = bv::utils::getSize(s);
       Integer s_val = s.getConst<BitVector>().toInteger();