diff --git a/src/ast/datatype_decl_plugin.cpp b/src/ast/datatype_decl_plugin.cpp
index 66ce1a3ba..ce183ce6b 100644
--- a/src/ast/datatype_decl_plugin.cpp
+++ b/src/ast/datatype_decl_plugin.cpp
@@ -717,6 +717,8 @@ namespace datatype {
                 todo.pop_back();
                 continue;
             }
+            if (!is_declared(s))
+                return true;
             already_found.insert(datatype_name(s), GRAY);
             def const& d = get_def(s);
             bool can_process       = true;
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index e5fd2ef70..51f2c3d98 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -342,9 +342,7 @@ namespace sat {
     clause* solver::mk_clause(unsigned num_lits, literal * lits, sat::status st) {
         m_model_is_current = false;
             
-        for (unsigned i = 0; i < num_lits; i++) 
-            VERIFY(!was_eliminated(lits[i]));
-        
+
         DEBUG_CODE({
                 for (unsigned i = 0; i < num_lits; i++) {
                     CTRACE("sat", was_eliminated(lits[i]), tout << lits[i] << " was eliminated\n";);
diff --git a/src/sat/smt/sat_dual_solver.cpp b/src/sat/smt/sat_dual_solver.cpp
index 599caf6e5..86d73a2d8 100644
--- a/src/sat/smt/sat_dual_solver.cpp
+++ b/src/sat/smt/sat_dual_solver.cpp
@@ -22,6 +22,7 @@ namespace sat {
         m_solver(m_params, l)
     {
         SASSERT(!m_solver.get_config().m_drat);
+        m_solver.set_incremental(true);
     }
 
     void dual_solver::flush() {
@@ -104,10 +105,10 @@ namespace sat {
             root = ext2lit(clause[0]);
         else {
             root = literal(m_solver.mk_var(), false);
-            m_solver.set_external(root.var());
             for (unsigned i = 0; i < sz; ++i)
                 m_solver.mk_clause(root, ~ext2lit(clause[i]), status::input());
-        }
+        }        
+        m_solver.set_external(root.var());
         m_roots.push_back(~root);
         TRACE("dual", tout << "root: " << ~root << " => " << literal_vector(sz, clause) << "\n";);
     }
diff --git a/src/sat/smt/sat_dual_solver.h b/src/sat/smt/sat_dual_solver.h
index d0465ac32..08a31084e 100644
--- a/src/sat/smt/sat_dual_solver.h
+++ b/src/sat/smt/sat_dual_solver.h
@@ -23,7 +23,13 @@ Author:
 namespace sat {
 
     class dual_solver {
-        no_drat_params  m_params;
+        class dual_params : public no_drat_params {
+        public:
+            dual_params() {
+                set_bool("core.minimize", false);
+            }
+        };
+        dual_params     m_params;
         solver          m_solver;
         lim_svector<literal> m_units, m_roots;
         lim_svector<bool_var> m_tracked_vars;