diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index 7c470f552..f776fa3e9 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -188,6 +188,7 @@ public:
     }
 
     lbool mus_solver() {
+        lbool is_sat = l_true;
         init();
         init_local();
         trace();
@@ -198,7 +199,7 @@ public:
                   tout << "\n";
                   display(tout);
                   );
-            lbool is_sat = check_sat_hill_climb(m_asms);
+            is_sat = check_sat_hill_climb(m_asms);
             if (m_cancel) {
                 return l_undef;
             }
@@ -833,9 +834,7 @@ public:
                 s().assert_expr(m_asms[i].get());
             }
         }
-        else {
-            maxsmt_solver_base::commit_assignment();
-        }
+        // else: there is only a single assignment to these soft constraints.
     }
 
     void verify_core(exprs const& core) {
diff --git a/src/opt/maxsmt.cpp b/src/opt/maxsmt.cpp
index 6b518edfa..2d3a60ea8 100644
--- a/src/opt/maxsmt.cpp
+++ b/src/opt/maxsmt.cpp
@@ -159,12 +159,7 @@ 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()) {
-            TRACE("opt", tout << "no constraints\n";);
-            m_msolver = 0;
-            is_sat = s().check_sat(0, 0);
-        }
-        else if (maxsat_engine == symbol("maxres")) {            
+        if (m_soft_constraints.empty() || maxsat_engine == symbol("maxres")) {            
             m_msolver = mk_maxres(m_c, m_weights, m_soft_constraints);
         }
         else if (maxsat_engine == symbol("pd-maxres")) {            
diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp
index 4f810727a..13999222f 100644
--- a/src/smt/smt_internalizer.cpp
+++ b/src/smt/smt_internalizer.cpp
@@ -617,7 +617,15 @@ namespace smt {
                 mk_ite_cnstr(to_app(n));
                 add_ite_rel_watches(to_app(n));
                 break;
+            case OP_TRUE:
+            case OP_FALSE:
+                break;
             case OP_DISTINCT:
+            case OP_IMPLIES:
+            case OP_XOR:
+                UNREACHABLE();
+            case OP_OEQ:
+            case OP_INTERP:            
                 UNREACHABLE();
             default:
                 break;