From e1a0a2e53600154082fe9c204f90c06ce2d7a2f6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 7 Jul 2020 22:38:21 -0700 Subject: [PATCH] give up on addition subterms in monomial decomposition caused by disabling rewriter.flat seems to be corner case exercised in #4532. Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith_nl.h | 24 +++++++++++++----------- 1 file changed, 13 insertions(+), 11 deletions(-) diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index 917ba4fd4..1d9584b2f 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -1122,27 +1122,29 @@ bool theory_arith::get_polynomial_info(buffer const & p, sbuffe varinfo.reset(); m_var2num_occs.reset(); -#define ADD_OCC(VAR) if (has_var(VAR) && !is_fixed(expr2var(VAR))) { \ - TRACE("nl_info", tout << "adding occ: " << mk_bounded_pp(VAR, get_manager()) << "\n";); \ - unsigned occs = 0; \ - m_var2num_occs.find(VAR, occs); \ - occs++; \ - m_var2num_occs.insert(VAR, occs); \ - } + auto add_occ = [&](expr* v) { + if (has_var(v) && !is_fixed(expr2var(v))) { + TRACE("nl_info", tout << "adding occ: " << mk_bounded_pp(v, get_manager()) << "\n";); + unsigned occs = 0; + m_var2num_occs.find(v, occs); + m_var2num_occs.insert(v, 1 + occs); + } + }; for (auto const& ce : p) { expr * m = ce.second; if (m_util.is_numeral(m)) { continue; } - else if (ctx.e_internalized(m) && !is_pure_monomial(m)) { - ADD_OCC(m); - } + else if (m_util.is_add(m)) + return false; + else if (ctx.e_internalized(m) && !is_pure_monomial(m)) + add_occ(m); else { buffer vp; decompose_monomial(m, vp); for (auto const& p : vp) { - ADD_OCC(p.first); + add_occ(p.first); } } }