#6116

fix unsoundness issue due to book-keeping changes for whether the solver uses assumptions.
Z3Prover · Aug 18, 2022 · 8e167aa · 8e167aa
1 parent 1a5503c
commit 8e167aa
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
@@ -2416,7 +2416,7 @@ namespace sat {
         m_conflict_lvl = get_max_lvl(m_not_l, m_conflict, unique_max);        
         justification js = m_conflict;
 
-        if (m_conflict_lvl <= 1 && tracking_assumptions()) {
+        if (m_conflict_lvl <= 1 && (!m_assumptions.empty() || !m_user_scope_literals.empty())) {
             TRACE("sat", tout << "unsat core\n";);
             resolve_conflict_for_unsat_core();
             return l_false;