From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Tue, 23 Jan 2018 20:02:42 +0000 (-0800)
Subject: Fix MULT handling for CBQI BV. (#1531)
X-Git-Tag: cvc5-1.0.0~5348
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6a84e271abecb437bd74f9df1d796f4972136021;p=cvc5.git

Fix MULT handling for CBQI BV. (#1531)
---

diff --git a/src/theory/quantifiers/bv_inverter.cpp b/src/theory/quantifiers/bv_inverter.cpp
index cf16efbfa..975016d34 100644
--- 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();