projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: bc23785) | patch
Remove wrong `ExtractMultLeadingBit` rule
authorAndres Notzli <andres.noetzli@gmail.com>
Wed, 30 Nov 2016 01:30:54 +0000 (17:30 -0800)
committerAndres Notzli <andres.noetzli@gmail.com>
Wed, 30 Nov 2016 23:33:35 +0000 (15:33 -0800)
commit05c7d36e7a4844ac1c8a14035776fbba6e00704b
tree1c9a5919a9ce461f64b9f8b7c26c26cf54c1b4d3tree
parentbc2378517a2f4100ba614cd44b3aa047089c82c8commit | diff
Remove wrong `ExtractMultLeadingBit` rule

The rule `ExtractMultLeadingBit` estimated the number of leading zeros
wrong: when there were ones in the leading constant parts of the
factors, it was using the length of the non-zero part instead of the
length of the zero part. This commit includes an example for which the
previous version of the rule would cause a wrong answer.
src/theory/bv/theory_bv_rewrite_rules_simplification.h diff | blob | history
test/regress/regress0/bv/Makefile.am diff | blob | history
test/regress/regress0/bv/bug_extract_mult_leading_bit.smt2 [new file with mode: 0644] blob