diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h
index 7a267fdec..f9560cb01 100644
--- a/src/smt/smt_context.h
+++ b/src/smt/smt_context.h
@@ -134,7 +134,6 @@ namespace smt {
             enode *                 m_lhs;
             enode *                 m_rhs;
             eq_justification        m_justification;
-            new_eq() {}
             new_eq(enode * lhs, enode * rhs, eq_justification const & js):
                 m_lhs(lhs), m_rhs(rhs), m_justification(js) {}
         };
@@ -143,7 +142,6 @@ namespace smt {
             theory_id  m_th_id;
             theory_var m_lhs;
             theory_var m_rhs;
-            new_th_eq():m_th_id(null_theory_id), m_lhs(null_theory_var), m_rhs(null_theory_var) {}
             new_th_eq(theory_id id, theory_var l, theory_var r):m_th_id(id), m_lhs(l), m_rhs(r) {}
         };
         svector<new_th_eq>          m_th_eq_propagation_queue;
@@ -215,7 +213,7 @@ namespace smt {
         // -----------------------------------
         proto_model_ref            m_proto_model;
         model_ref                  m_model;
-        std::string                m_unknown;
+        const char *               m_unknown;
         void                       mk_proto_model();
         void                       reset_model() { m_model = nullptr; m_proto_model = nullptr; }
 
diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp
index fe86c6811..3925a4e21 100644
--- a/src/smt/smt_context_pp.cpp
+++ b/src/smt/smt_context_pp.cpp
@@ -66,6 +66,7 @@ namespace smt {
     std::string context::last_failure_as_string() const {
         std::string r;
         switch(m_last_search_failure) {
+        case UNKNOWN:
         case OK: r = m_unknown; break;
         case MEMOUT: r = "memout"; break;
         case CANCELED: r = "canceled"; break;
@@ -82,7 +83,6 @@ namespace smt {
         case RESOURCE_LIMIT: r = "(resource limits reached)"; break;
         case QUANTIFIERS: r = "(incomplete quantifiers)"; break;
         case LAMBDAS: r = "(incomplete lambdas)"; break;
-        case UNKNOWN: r = m_unknown; break;
         }
         return r;
     }