diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 7fa2dc53f..5d24977b5 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -623,17 +623,17 @@ void cmd_context::init_manager() {
         // no-op
     }
     else if (m_manager) {
+        m_manager_initialized = true;
         SASSERT(!m_own_manager);
         init_external_manager();
-        m_manager_initialized = true;
     }
     else {
+        m_manager_initialized = true;
         SASSERT(m_pmanager == 0);
         m_check_sat_result = 0;
         m_manager  = m_params.mk_ast_manager();
         m_pmanager = alloc(pdecl_manager, *m_manager);
         init_manager_core(true);
-        m_manager_initialized = true;
     }
 }
 
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 7c42f41cf..c4aa34c61 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -294,7 +294,7 @@ public:
     std::string reason_unknown() const;
 
     bool has_manager() const { return m_manager != 0; }
-    ast_manager & m() const { if (!m_manager) const_cast<cmd_context*>(this)->init_manager(); return *m_manager; }
+    ast_manager & m() const { const_cast<cmd_context*>(this)->init_manager(); return *m_manager; }
     virtual ast_manager & get_ast_manager() { return m(); }
     pdecl_manager & pm() const { if (!m_pmanager) const_cast<cmd_context*>(this)->init_manager(); return *m_pmanager; }
     sexpr_manager & sm() const { if (!m_sexpr_manager) const_cast<cmd_context*>(this)->m_sexpr_manager = alloc(sexpr_manager); return *m_sexpr_manager; }