diff --git a/src/sat/sat_drat.h b/src/sat/sat_drat.h
index e60e8048719..83a29c9eda7 100644
--- a/src/sat/sat_drat.h
+++ b/src/sat/sat_drat.h
@@ -61,7 +61,8 @@ namespace sat {
     class clause;
 
     struct print_clause {
-        virtual void on_clause(unsigned, literal const*, status) = 0;
+        virtual ~print_clause() {}
+        virtual void on_clause(unsigned, literal const*, status) = 0;        
     };
 
     class drat {
@@ -150,12 +151,12 @@ namespace sat {
 
         // support for SMT - connect Boolean variables with AST nodes
         // associate AST node id with Boolean variable v
-        void bool_def(bool_var v, unsigned n);
 
         // declare AST node n with 'name' and arguments arg
         void def_begin(char id, unsigned n, std::string const& name);
         void def_add_arg(unsigned arg);
         void def_end();
+        void bool_def(bool_var v, unsigned n);
 
         // ad-hoc logging until a format is developed
         void log_adhoc(std::function<void(std::ostream&)>& fn);
diff --git a/src/sat/smt/euf_proof.cpp b/src/sat/smt/euf_proof.cpp
index a63efb79b00..f18e112b802 100644
--- a/src/sat/smt/euf_proof.cpp
+++ b/src/sat/smt/euf_proof.cpp
@@ -41,6 +41,11 @@ namespace euf {
         get_drat().def_begin(id, n, name);
     }
 
+    void solver::bool_def(bool_var v, unsigned n) {
+        get_drat().bool_def(v, n);
+    }
+
+
     void solver::drat_log_params(func_decl* f) {
         for (unsigned i = f->get_num_parameters(); i-- > 0; ) {
             auto const& p = f->get_parameter(i);
@@ -59,14 +64,14 @@ namespace euf {
             drat_log_decl(a->get_decl());
             std::stringstream strm;
             strm << mk_ismt2_func(a->get_decl(), m);
-            get_drat().def_begin('e', e->get_id(), strm.str());
+            def_begin('e', e->get_id(), strm.str());
             for (expr* arg : *a)
                 def_add_arg(arg->get_id());
             def_end();
         }
         else if (is_var(e)) {
             var* v = to_var(e);
-            get_drat().def_begin('v', v->get_id(), "" + mk_pp(e->get_sort(), m));
+            def_begin('v', v->get_id(), "" + mk_pp(e->get_sort(), m));
             def_add_arg(v->get_idx());
             def_end();
         }
@@ -77,7 +82,7 @@ namespace euf {
             for (unsigned i = 0; i < q->get_num_decls(); ++i) 
                 strm << " (" << q->get_decl_name(i) << " " << mk_pp(q->get_decl_sort(i), m) << ")";            
             strm << ")";
-            get_drat().def_begin('q', q->get_id(), strm.str());
+            def_begin('q', q->get_id(), strm.str());
             def_add_arg(q->get_expr()->get_id());
             def_end();
         }
@@ -116,7 +121,7 @@ namespace euf {
         if (!use_drat())
             return;
         drat_log_expr(e);
-        get_drat().bool_def(v, e->get_id());
+        bool_def(v, e->get_id());
     }
 
 
@@ -130,7 +135,7 @@ namespace euf {
         std::ostringstream strm;
         smt2_pp_environment_dbg env(m);
         ast_smt2_pp(strm, f, env);
-        get_drat().def_begin('f', f->get_small_id(), strm.str());
+        def_begin('f', f->get_small_id(), strm.str());
         def_end();
     }
 
@@ -200,11 +205,11 @@ namespace euf {
         VERIFY(m.is_eq(eq, a, b));
         drat_log_expr(a);
         drat_log_expr(b);
-        get_drat().def_begin('e', eq->get_id(), std::string("="));
+        def_begin('e', eq->get_id(), std::string("="));
         def_add_arg(a->get_id());
         def_add_arg(b->get_id());
         def_end();
-        get_drat().bool_def(lit.var(), eq->get_id());
+        bool_def(lit.var(), eq->get_id());
     }
 
     void solver::on_clause(unsigned n, literal const* lits, sat::status st) {
diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h
index f77954ded91..ed1ad9b9281 100644
--- a/src/sat/smt/euf_solver.h
+++ b/src/sat/smt/euf_solver.h
@@ -352,6 +352,7 @@ namespace euf {
         void drat_bool_def(sat::bool_var v, expr* n);
         void drat_eq_def(sat::literal lit, expr* eq);
         void drat_log_expr(expr* n);
+        void bool_def(bool_var v, unsigned n);
         bool visit_clause(unsigned n, literal const* lits);
         void display_clause(unsigned n, literal const* lits);
         void visit_expr(expr* e);