diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp
index 532b29f1c..66d660366 100644
--- a/src/sat/sat_config.cpp
+++ b/src/sat/sat_config.cpp
@@ -192,7 +192,7 @@ namespace sat {
         m_drat_check_unsat  = p.drat_check_unsat();
         m_drat_check_sat  = p.drat_check_sat();
         m_drat_file       = p.drat_file();
-        m_drat            = (m_drat_check_unsat || m_drat_file != symbol("") || m_drat_check_sat) && p.threads() == 1;
+        m_drat            = (m_drat_check_unsat || m_drat_file.is_non_empty_string() || m_drat_check_sat) && p.threads() == 1;
         m_drat_binary     = p.drat_binary();
         m_drat_activity   = p.drat_activity();
         m_dyn_sub_res     = p.dyn_sub_res();
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 8ba4ba41b..67fce084d 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -392,6 +392,8 @@ namespace sat {
     }
 
     void solver::drat_log_unit(literal lit, justification j) {
+        if (!m_ext)
+            return;
         extension::scoped_drating _sd(*m_ext.get());
         if (j.get_kind() == justification::EXT_JUSTIFICATION) 
             fill_ext_antecedents(lit, j, false);
diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp
index db6baef9e..f7a204014 100644
--- a/src/sat/smt/q_mbi.cpp
+++ b/src/sat/smt/q_mbi.cpp
@@ -127,6 +127,7 @@ namespace q {
                 proj = solver_project(*mdl1, *qb);
                 if (!proj)
                     break;
+                TRACE("q", tout << "project: " << proj << "\n";);
                 m_qs.add_clause(~qlit, ~ctx.mk_literal(proj));
                 m_solver->assert_expr(m.mk_not(proj));
             }
@@ -136,6 +137,7 @@ namespace q {
             proj = solver_project(*mdl0, *qb);
             if (!proj)
                 return l_undef;
+            TRACE("q", tout << "project-base: " << proj << "\n";);
             m_qs.add_clause(~qlit, ~ctx.mk_literal(proj));
         }
         // TODO: add as top-level clause for relevancy        
@@ -251,7 +253,6 @@ namespace q {
             if (!m_model->eval_expr(bounds, mbounds, true))
                 return;
             mbounds = subst(mbounds, qb.vars);
-            std::cout << "restrict with bounds " << mbounds << " " << vbounds << "\n";
             m_solver->assert_expr(mbounds);
             qb.domain_eqs.push_back(vbounds);
         }
diff --git a/src/sat/smt/sat_dual_solver.cpp b/src/sat/smt/sat_dual_solver.cpp
index e473a4a00..3d0411570 100644
--- a/src/sat/smt/sat_dual_solver.cpp
+++ b/src/sat/smt/sat_dual_solver.cpp
@@ -18,9 +18,15 @@ Author:
 
 namespace sat {
 
+    dual_solver::no_drat_params::no_drat_params() {
+        set_sym("drat.file", symbol());
+    }
+
     dual_solver::dual_solver(reslimit& l):
-        m_solver(params_ref(), l)
-    {}
+        m_solver(m_params, l)
+    {
+        SASSERT(!m_solver.get_config().m_drat);
+    }
 
     void dual_solver::push() {
         m_solver.user_push(); 
diff --git a/src/sat/smt/sat_dual_solver.h b/src/sat/smt/sat_dual_solver.h
index 8dc9e0826..9f27a8306 100644
--- a/src/sat/smt/sat_dual_solver.h
+++ b/src/sat/smt/sat_dual_solver.h
@@ -23,6 +23,10 @@ Author:
 namespace sat {
 
     class dual_solver {
+        struct no_drat_params : public params_ref {
+            no_drat_params();
+        };
+        no_drat_params  m_params;
         solver          m_solver;
         lim_svector<literal> m_units, m_roots;
         lim_svector<bool_var> m_tracked_vars;