From 3774d6d405761781432b00226024a07c96008e9a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 26 Jan 2020 17:59:52 -0800 Subject: [PATCH] fix #2890 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith_core.h | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 08c060f89..ef930c8a0 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -65,7 +65,9 @@ namespace smt { e = m_util.mk_power0(n->get_arg(0), n->get_arg(1)); } if (e) { - ctx.assign(mk_eq(e, n, false), nullptr); + literal lit = mk_eq(e, n, false); + ctx.mark_as_relevant(lit); + ctx.assign(lit, nullptr); } }