From 0df6fe65f704ccc745b2fe133b12d82ba18964b1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 24 Aug 2024 18:31:59 -0700 Subject: [PATCH] enable multiplier expansion, enable linear move Signed-off-by: Nikolaj Bjorner --- src/ast/sls/sls_arith_base.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp index b63b12ad1..0d9fcd284 100644 --- a/src/ast/sls/sls_arith_base.cpp +++ b/src/ast/sls/sls_arith_base.cpp @@ -558,7 +558,7 @@ namespace sls { if (find_nl_moves(lit)) return true; - if (false && find_lin_moves(lit)) + if (find_lin_moves(lit)) return true; @@ -867,7 +867,7 @@ namespace sls { muls.append(to_app(e)->get_num_args(), to_app(e)->get_args()); for (unsigned j = 0; j < muls.size(); ++j) { expr* arg = muls[j]; - if (false && a.is_mul(arg)) { + if (a.is_mul(arg)) { //verbose_stream() << "nested " << mk_bounded_pp(arg, m) << "\n"; muls.append(to_app(arg)->get_num_args(), to_app(arg)->get_args()); muls[j] = muls.back();