From 61b90e64b25629d14811921d0198079d96bf6b63 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 8 Jan 2023 14:17:49 -0800 Subject: [PATCH] disable new simplifcation for multiplier until really understood Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/bv_rewriter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp index a308cffc4..894286a02 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -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 new_args(num_args, args); rational p = rational(2).expt(sz) - 1;