From 4d61c199170c539e5a4b3d477627d3e030d77502 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 4 Dec 2024 15:35:21 -0800 Subject: [PATCH] add code path to reassert units Signed-off-by: Nikolaj Bjorner --- src/smt/smt_internalizer.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index f19144b62..a4f8b5a09 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -1438,7 +1438,8 @@ namespace smt { m_justifications.push_back(j); assign(unit, j); inc_ref(unit); - // m_units_to_reassert.push_back({ expr_ref(atom, m), unit.sign(), is_relevant(unit) }); + if (m_scope_lvl > m_search_lvl) + m_units_to_reassert.push_back({ expr_ref(atom, m), unit.sign(), is_relevant(unit) }); return nullptr; } case 2: