From a37d05d54b9ca10d4c613a4bb3a980f1bb0c1c4a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 10 Sep 2018 13:53:44 -0700 Subject: [PATCH] fix #1819 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith_int.h | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_arith_int.h b/src/smt/theory_arith_int.h index ee3bd5e2e..afe527a98 100644 --- a/src/smt/theory_arith_int.h +++ b/src/smt/theory_arith_int.h @@ -396,7 +396,9 @@ namespace smt { for (; it != end; ++it) { if (!it->is_dead() && it->m_var != b && is_free(it->m_var)) { theory_var v = it->m_var; - expr * bound = m_util.mk_ge(get_enode(v)->get_owner(), m_util.mk_numeral(rational::zero(), is_int(v))); + expr* e = get_enode(v)->get_owner(); + bool _is_int = m_util.is_int(e); + expr * bound = m_util.mk_ge(e, m_util.mk_numeral(rational::zero(), _is_int)); context & ctx = get_context(); ctx.internalize(bound, true); ctx.mark_as_relevant(bound);