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();