diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp
index b63b84e2ecf..0130676db33 100644
--- a/src/sat/sat_drat.cpp
+++ b/src/sat/sat_drat.cpp
@@ -35,6 +35,7 @@ namespace sat {
             if (s.get_config().m_drat_binary) 
                 std::swap(m_out, m_bout);            
         }
+        m_print_clause = nullptr;
     }
 
     drat::~drat() {
diff --git a/src/sat/sat_drat.h b/src/sat/sat_drat.h
index 838b0879a32..d48833099db 100644
--- a/src/sat/sat_drat.h
+++ b/src/sat/sat_drat.h
@@ -73,6 +73,7 @@ namespace sat {
             watched_clause(clause* c, literal l1, literal l2):
                 m_clause(c), m_l1(l1), m_l2(l2) {}
         };
+        std::function<void(unsigned, literal const*, status)> m_print_clause;
         svector<watched_clause>   m_watched_clauses;
         typedef svector<unsigned> watch;
         solver& s;
@@ -92,7 +93,6 @@ namespace sat {
         bool                    m_trim = false;
         stats                   m_stats;
 
-        std::function<void(unsigned, literal const*, status)> m_print_clause;
 
         void dump_activity();
         void dump(unsigned n, literal const* c, status st);