From d4aa850412308d4290aee4c8fd86a8bee55d158f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 30 Mar 2020 14:09:47 -0700
Subject: [PATCH] fix #3572

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_context.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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()) {