diff options
| -rw-r--r-- | src/theory/bv/theory_bv_rewrite_rules_simplification.h | 13 | ||||
| -rw-r--r-- | test/regress/regress0/bv/Makefile.am | 3 | ||||
| -rw-r--r-- | test/regress/regress0/bv/bug_extract_mult_leading_bit.smt2 | 7 |
3 files changed, 15 insertions, 8 deletions
diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index d84a07780..6ef591760 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -802,7 +802,7 @@ bool RewriteRule<ExtractMultLeadingBit>::applies(TNode node) { return false; unsigned low = utils::getExtractLow(node); node = node[0]; - + if (node.getKind() != kind::BITVECTOR_MULT || node.getNumChildren() != 2 || utils::getSize(node) <= 64) @@ -818,15 +818,14 @@ bool RewriteRule<ExtractMultLeadingBit>::applies(TNode node) { // count number of leading zeroes const Integer& int1 = node[0][0].getConst<BitVector>().toInteger(); const Integer& int2 = node[1][0].getConst<BitVector>().toInteger(); - unsigned zeroes1 = int1.isZero()? utils::getSize(node[0][0]) : - int1.length(); - - unsigned zeroes2 = int2.isZero()? utils::getSize(node[1][0]) : - int2.length(); + size_t int1_size = utils::getSize(node[0][0]); + size_t int2_size = utils::getSize(node[1][0]); + unsigned zeroes1 = int1.isZero() ? int1_size : int1_size - int1.length(); + unsigned zeroes2 = int2.isZero() ? int2_size : int2_size - int2.length(); // first k bits are not zero in the result unsigned k = 2 * n - (zeroes1 + zeroes2); - + if (k > low) return false; diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am index b3c7250ff..2caaea799 100644 --- a/test/regress/regress0/bv/Makefile.am +++ b/test/regress/regress0/bv/Makefile.am @@ -112,7 +112,8 @@ CVC_TESTS = bvsimple.cvc sizecheck.cvc BUG_TESTS = \ bug260a.smt \ bug260b.smt \ - bug440.smt + bug440.smt \ + bug_extract_mult_leading_bit.smt2 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(BUG_TESTS) diff --git a/test/regress/regress0/bv/bug_extract_mult_leading_bit.smt2 b/test/regress/regress0/bv/bug_extract_mult_leading_bit.smt2 new file mode 100644 index 000000000..8e3728587 --- /dev/null +++ b/test/regress/regress0/bv/bug_extract_mult_leading_bit.smt2 @@ -0,0 +1,7 @@ +(set-logic QF_BV) +(set-info :status sat) +(declare-fun x1 () (_ BitVec 15)) +(declare-fun x2 () (_ BitVec 15)) +(assert (not (= ((_ extract 64 60) (bvmul (concat #b00000000000000000000000000000000000000000000000000 x1) (concat #b10000000000000000000000000000000000000000000000000 x2))) #b00000))) +(check-sat) +(exit) |