From 859512d937594d3b597c956a7c476e46f3af9f8b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 24 Jul 2019 12:14:02 -0700 Subject: [PATCH] fix #2431 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith_core.h | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index f8edec8f6..7c3512171 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -246,11 +246,11 @@ namespace smt { SASSERT(m->get_num_args() == 2); if (m_util.is_numeral(arg2, _val2)) { numeral val(_val1 + _val2); - if (reflection_enabled()) { - internalize_term_core(to_app(arg1)); - internalize_term_core(to_app(arg2)); - mk_enode(m); - } + if (reflection_enabled()) { + internalize_term_core(to_app(arg1)); + internalize_term_core(to_app(arg2)); + mk_enode(m); + } theory_var v = internalize_numeral(m, val); add_row_entry(r_id, numeral::one(), v); return; @@ -730,7 +730,11 @@ namespace smt { template theory_var theory_arith::internalize_numeral(app * n, numeral const& val) { - SASSERT(!get_context().e_internalized(n)); + + context& ctx = get_context(); + if (ctx.e_internalized(n)) { + return mk_var(ctx.get_enode(n)); + } enode * e = mk_enode(n); // internalizer is marking enodes as interpreted whenever the associated ast is a value and a constant. // e->mark_as_interpreted();