From e820701f9d0fdd7be96057fec6ec8f178aa275e7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 31 Jan 2024 15:38:10 -0800 Subject: [PATCH] fix #7107 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 9a9b9239350..62c7c8ddd10 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -4265,9 +4265,11 @@ namespace smt { SASSERT(num_lits == 1); expr * unit = bool_var2expr(lits[0].var()); bool unit_sign = lits[0].sign(); + while (m.is_not(unit, unit)) + unit_sign = !unit_sign; m_units_to_reassert.push_back(unit); m_units_to_reassert_sign.push_back(unit_sign); - TRACE("reassert_units", tout << "asserting #" << unit->get_id() << " " << unit_sign << " @ " << m_scope_lvl << "\n";); + TRACE("reassert_units", tout << "asserting " << mk_pp(unit, m) << " #" << unit->get_id() << " " << unit_sign << " @ " << m_scope_lvl << "\n";); } m_conflict_resolution->release_lemma_atoms();