From 75a9038aa295c106d53271653ce72f24605b83f9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 16 Jul 2023 16:54:26 -0700 Subject: [PATCH] add missing dependencies in rup Signed-off-by: Nikolaj Bjorner --- src/sat/sat_proof_trim.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/sat/sat_proof_trim.cpp b/src/sat/sat_proof_trim.cpp index d47819921..a9f36b818 100644 --- a/src/sat/sat_proof_trim.cpp +++ b/src/sat/sat_proof_trim.cpp @@ -278,10 +278,13 @@ namespace sat { auto& [clauses, id, in_core] = m_clauses.find(m_clause); in_core = true; m_result.back().second.push_back(id); - if (l != null_literal && s.lvl(l) == 0) { + if (l != null_literal && s.lvl(l) == 0 && m_clause.size() > 1) { m_clause.reset(); m_clause.push_back(l); - m_clauses.insert_if_not_there(m_clause, {{}, 0, true }).m_in_core = true; + auto& [clauses, id, in_core] = m_clauses.insert_if_not_there(m_clause, {{}, 0, true }); + in_core = true; + if (id != 0) + m_result.back().second.push_back(id); } }