From 18bec88a8af07410c8b0e3bec9e89aa5d54556c6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 10 Sep 2018 15:52:02 -0700 Subject: [PATCH] purify non-constant terms by default to enforce theory #1820 Signed-off-by: Nikolaj Bjorner --- src/opt/opt_context.cpp | 6 +----- 1 file changed, 1 insertion(+), 5 deletions(-) diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 5d4eb3fc5..b1296f71e 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -1084,11 +1084,7 @@ namespace opt { } term = m_arith.mk_add(args.size(), args.c_ptr()); } - else if (m_arith.is_arith_expr(term) && !is_mul_const(term)) { - TRACE("opt", tout << "Purifying " << term << "\n";); - term = purify(fm, term); - } - else if (m.is_ite(term)) { + else if (m.is_ite(term) || !is_mul_const(term)) { TRACE("opt", tout << "Purifying " << term << "\n";); term = purify(fm, term); }