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); } }