From 9db4ac434dca40dcfbcefbf8c8d623f03ec2744a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 4 Dec 2024 16:08:50 -0800
Subject: [PATCH] fix unsoundness with what appears to be unit literals but
really are literals that are justified
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/smt/smt_context.cpp | 1 +
src/smt/smt_internalizer.cpp | 4 +++-
2 files changed, 4 insertions(+), 1 deletion(-)
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 4c1ba3da7..24341a624 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -2389,6 +2389,7 @@ namespace smt {
assign(l, b_justification::mk_axiom());
if (is_relevant)
mark_as_relevant(l);
+ verbose_stream() << "reassert " << unit << ": " << mk_bounded_pp(unit, m) << "\n";
TRACE("reassert_units", tout << "reasserting #" << unit->get_id() << " " << sign << " @ " << m_scope_lvl << "\n";);
}
if (at_base_level())
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index a4f8b5a09..b592742f5 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -1438,8 +1438,10 @@ namespace smt {
m_justifications.push_back(j);
assign(unit, j);
inc_ref(unit);
- if (m_scope_lvl > m_search_lvl)
+ if (m_scope_lvl > m_search_lvl && !j) {
+ verbose_stream() << "unit clause " << unit << ": " << mk_bounded_pp(atom, m) << "\n";
m_units_to_reassert.push_back({ expr_ref(atom, m), unit.sign(), is_relevant(unit) });
+ }
return nullptr;
}
case 2: