diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index a3a2ca9ec..ebf5da767 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -4172,7 +4172,7 @@ namespace smt { update_phase_cache_counter(); return true; } - else if (m_fparams.m_clause_proof) { + else if (m_fparams.m_clause_proof && !m.proofs_enabled()) { m_unsat_proof = m_clause_proof.get_proof(); } else if (m.proofs_enabled()) {