diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 248d2161e..71a6dde2b 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -3988,6 +3988,12 @@ END_MLAPI_EXCLUDE
 
     /**
         \brief Return a unique identifier for \c t.
+        The identifier is unique up to structural equality. Thus, two ast nodes
+        created by the same context and having the same children and same function symbols
+        have the same identifiers. Ast nodes created in the same context, but having
+        different children or different functions have different identifiers.
+        Variables and quantifiers are also assigned different identifiers according to
+        their structure.        
         \mlonly \remark Implicitly used by [Pervasives.compare] for values of type [ast], [app], [sort], [func_decl], and [pattern]. \endmlonly
 
         def_API('Z3_get_ast_id', UINT, (_in(CONTEXT), _in(AST)))
@@ -3996,6 +4002,8 @@ END_MLAPI_EXCLUDE
 
     /**
        \brief Return a hash code for the given AST.
+       The hash code is structural. You can use Z3_get_ast_id interchangably with 
+       this function.
        \mlonly \remark Implicitly used by [Hashtbl.hash] for values of type [ast], [app], [sort], [func_decl], and [pattern]. \endmlonly
 
        def_API('Z3_get_ast_hash', UINT, (_in(CONTEXT), _in(AST)))
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 731608524..7fa2dc53f 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -314,8 +314,9 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l):
     m_numeral_as_real(false),
     m_ignore_check(false),
     m_exit_on_error(false),
-    m_manager(m),
+    m_manager(m),   
     m_own_manager(m == 0),
+    m_manager_initialized(false),
     m_pmanager(0),
     m_sexpr_manager(0),
     m_regular("stdout", std::cout),
@@ -326,8 +327,6 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l):
     install_core_tactic_cmds(*this);
     install_interpolant_cmds(*this);
     SASSERT(m != 0 || !has_manager());
-    if (m)
-        init_external_manager();
     if (m_main_ctx) { 
         set_verbose_stream(diagnostic_stream());
     }
@@ -620,12 +619,22 @@ void cmd_context::init_manager_core(bool new_manager) {
 }
 
 void cmd_context::init_manager() {
-    SASSERT(m_manager == 0);
-    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);
+    if (m_manager_initialized) {
+        // no-op
+    }
+    else if (m_manager) {
+        SASSERT(!m_own_manager);
+        init_external_manager();
+        m_manager_initialized = true;
+    }
+    else {
+        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;
+    }
 }
 
 void cmd_context::init_external_manager() {
@@ -1211,8 +1220,7 @@ void cmd_context::assert_expr(symbol const & name, expr * t) {
 
 void cmd_context::push() {
     m_check_sat_result = 0;
-    if (!has_manager())
-        init_manager();
+    init_manager();
     m_scopes.push_back(scope());
     scope & s = m_scopes.back();
     s.m_func_decls_stack_lim   = m_func_decls_stack.size();
@@ -1332,8 +1340,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
         return;
     IF_VERBOSE(100, verbose_stream() << "(started \"check-sat\")" << std::endl;);
     TRACE("before_check_sat", dump_assertions(tout););
-    if (!has_manager())
-        init_manager();
+    init_manager();
     if (m_solver) {
         m_check_sat_result = m_solver.get(); // solver itself stores the result.
         m_solver->set_progress_callback(this);
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 8ad07e8cc..7c42f41cf 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -149,6 +149,7 @@ protected:
 
     ast_manager *                m_manager;
     bool                         m_own_manager;
+    bool                         m_manager_initialized;
     pdecl_manager *              m_pmanager;
     sexpr_manager *              m_sexpr_manager;
     check_logic                  m_check_logic;