diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
index a0dd2aed1..1ad2a09be 100644
--- a/src/opt/maxsmt.cpp
+++ b/src/opt/maxsmt.cpp
@@ -156,20 +156,19 @@ namespace opt {
         symbol const& maxsat_engine = m_c.maxsat_engine();
         IF_VERBOSE(1, verbose_stream() << "(maxsmt)\n";);
         TRACE("opt", tout << "maxsmt\n";);
-        if (m_soft_constraints.empty() || maxsat_engine == symbol("maxres")) {            
+        if (m_soft_constraints.empty() || maxsat_engine == symbol("maxres") || maxsat_engine == symbol::null) {            
             m_msolver = mk_maxres(m_c, m_index, m_weights, m_soft_constraints);
         }
         else if (maxsat_engine == symbol("pd-maxres")) {            
             m_msolver = mk_primal_dual_maxres(m_c, m_index, m_weights, m_soft_constraints);
         }
-        else {
-            if (maxsat_engine != symbol::null && maxsat_engine != symbol("wmax")) {
-                warning_msg("solver %s is not recognized, using default 'wmax'", 
-                            maxsat_engine.str().c_str());
-            }
-            std::cout << "wmax\n";
+        else if (maxsat_engine == symbol("wmax")) {
             m_msolver = mk_wmax(m_c, m_weights, m_soft_constraints);
         }
+        else {
+            warning_msg("solver %s is not recognized, using default 'maxres'", maxsat_engine.str().c_str());
+            m_msolver = mk_maxres(m_c, m_index, m_weights, m_soft_constraints);
+        }
 
         if (m_msolver) {
             m_msolver->updt_params(m_params);
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 4eafb93f2..aad034130 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -35,6 +35,7 @@ Notes:
 #include "model_smt2_pp.h"
 #include "card2bv_tactic.h"
 #include "eq2bv_tactic.h"
+#include "dt2bv_tactic.h"
 #include "inc_sat_solver.h"
 #include "bv_decl_plugin.h"
 #include "pb_decl_plugin.h"
@@ -688,21 +689,19 @@ namespace opt {
                      // NB: mk_elim_uncstr_tactic(m) is not sound with soft constraints
                      mk_simplify_tactic(m));   
         opt_params optp(m_params);
-        tactic_ref tac2, tac3, tac4;
+        tactic_ref tac1, tac2, tac3, tac4;
         if (optp.elim_01()) {
+            tac1 = mk_dt2bv_tactic(m);
             tac2 = mk_elim01_tactic(m);
             tac3 = mk_lia2card_tactic(m);
             tac4 = mk_eq2bv_tactic(m);
             params_ref lia_p;
             lia_p.set_bool("compile_equality", optp.pb_compile_equality());
             tac3->updt_params(lia_p);
-            set_simplify(and_then(tac0.get(), tac2.get(), tac3.get(), tac4.get(), mk_simplify_tactic(m)));
+            set_simplify(and_then(tac0.get(), tac1.get(), tac2.get(), tac3.get(), tac4.get(), mk_simplify_tactic(m)));
         }
         else {
-            tactic_ref tac1 = 
-                and_then(tac0.get(),
-                         mk_simplify_tactic(m));            
-            set_simplify(tac1.get());
+            set_simplify(tac0.get());
         }
         proof_converter_ref pc;
         expr_dependency_ref core(m);
diff --git a/src/smt/theory_wmaxsat.cpp b/src/smt/theory_wmaxsat.cpp
index e52475d06..b572d8e69 100644
--- a/src/smt/theory_wmaxsat.cpp
+++ b/src/smt/theory_wmaxsat.cpp
@@ -35,7 +35,8 @@ theory_wmaxsat::theory_wmaxsat(ast_manager& m, filter_model_converter& mc):
     m_zmin_cost(m_mpz),
     m_found_optimal(false),
     m_propagate(false),
-    m_normalize(false)
+    m_normalize(false),
+    m_den(1)
 {}
 
 theory_wmaxsat::~theory_wmaxsat() {