diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 1335685ff..624671e2b 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -42,7 +42,6 @@ Notes:
 #include "ast_smt_pp.h"
 #include "filter_model_converter.h"
 #include "ast_pp_util.h"
-#include "inc_sat_solver.h"
 #include "qsat.h"
 
 namespace opt {
@@ -595,6 +594,9 @@ namespace opt {
         if (opt_params(m_params).priority() == symbol("pareto")) {
             return;
         }
+        if (m.proofs_enabled()) {
+            return;
+        }
         m_params.set_bool("minimize_core_partial", true);
         m_params.set_bool("minimize_core", true);
         m_sat_solver = mk_inc_sat_solver(m, m_params);