diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 2d0d349d7..1be6fe395 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1235,6 +1235,12 @@ static void restore(ast_manager & m, ptr_vector<expr> & c, unsigned old_sz) {
 }
 
 void cmd_context::restore_assertions(unsigned old_sz) {
+    if (!has_manager()) {
+        // restore_assertions invokes m(), so if cmd_context does not have a manager, it will try to create one.
+        SASSERT(old_sz == m_assertions.size());
+        SASSERT(m_assertions.empty());
+        return;
+    }
     SASSERT(old_sz <= m_assertions.size());
     SASSERT(!m_interactive_mode || m_assertions.size() == m_assertion_strings.size());
     restore(m(), m_assertions, old_sz);
diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp
index 9d06cb115..6b55d4072 100644
--- a/src/cmd_context/pdecl.cpp
+++ b/src/cmd_context/pdecl.cpp
@@ -785,6 +785,7 @@ psort * pdecl_manager::mk_psort_cnst(sort * s) {
 }
 
 psort * pdecl_manager::register_psort(psort * n) {
+    TRACE("register_psort", tout << "registering psort...\n"; n->display(tout); tout << "\n";);
     psort * r = m_table.insert_if_not_there(n);
     if (r != n) {
         del_decl_core(n);
diff --git a/src/solver/solver_na2as.cpp b/src/solver/solver_na2as.cpp
index f6d7414a5..e71a9873b 100644
--- a/src/solver/solver_na2as.cpp
+++ b/src/solver/solver_na2as.cpp
@@ -31,15 +31,20 @@ solver_na2as::~solver_na2as() {
 }
 
 void solver_na2as::assert_expr(expr * t, expr * a) {
-    SASSERT(m_manager != 0);
-    SASSERT(is_uninterp_const(a));
-    SASSERT(m_manager->is_bool(a));
-    TRACE("solver_na2as", tout << "asserting\n" << mk_ismt2_pp(t, *m_manager) << "\n" << mk_ismt2_pp(a, *m_manager) << "\n";);
-    m_manager->inc_ref(a);
-    m_assumptions.push_back(a);
-    expr_ref new_t(*m_manager);
-    new_t = m_manager->mk_implies(a, t);
-    assert_expr(new_t);
+    if (a == 0) {
+        assert_expr(t);
+    }
+    else {
+        SASSERT(m_manager != 0);
+        SASSERT(is_uninterp_const(a));
+        SASSERT(m_manager->is_bool(a));
+        TRACE("solver_na2as", tout << "asserting\n" << mk_ismt2_pp(t, *m_manager) << "\n" << mk_ismt2_pp(a, *m_manager) << "\n";);
+        m_manager->inc_ref(a);
+        m_assumptions.push_back(a);
+        expr_ref new_t(*m_manager);
+        new_t = m_manager->mk_implies(a, t);
+        assert_expr(new_t);
+    }
 }
     
 void solver_na2as::init(ast_manager & m, symbol const & logic) {