mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

disable new simplifcation for multiplier until really understood

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-01-08 14:17:49 -08:00
parent fcea32344e
commit 61b90e64b2
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ast/rewriter/bv_rewriter.cpp
View file

@ -2282,7 +2282,7 @@ br_status bv_rewriter::mk_mul_hoist(unsigned num_args, expr * const * args, expr
expr* z = nullptr, *u = nullptr;
for (unsigned i = 0; i < num_args; ++i) {
// ~x = -1 - x
if (m_util.is_bv_not(args[i], z)) {
if (false && m_util.is_bv_not(args[i], z)) {
unsigned sz = m_util.get_bv_size(z);
ptr_vector<expr> new_args(num_args, args);
rational p = rational(2).expt(sz) - 1;