From 059ccd67bb019e47c983bd11afd1dbf8f5e09864 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 24 Aug 2024 13:27:09 -0700 Subject: [PATCH] disable nested mul Signed-off-by: Nikolaj Bjorner --- src/ast/sls/sls_arith_base.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/sls/sls_arith_base.cpp b/src/ast/sls/sls_arith_base.cpp index aa6d1065d..c16d44c4b 100644 --- a/src/ast/sls/sls_arith_base.cpp +++ b/src/ast/sls/sls_arith_base.cpp @@ -850,7 +850,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 (a.is_mul(arg)) { + if (false && 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();