diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 5129cf710e..81247613cf 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -166,6 +166,7 @@ parser::parser(environment const & env, io_state const & ios,
     m_imports_parsed(false),
     m_snapshot_vector(sv) {
     m_next_inst_idx = 1;
+    m_ignore_noncomputable = false;
     if (s) {
         m_env                = s->m_env;
         m_ios.set_options(s->m_options);
@@ -176,10 +177,10 @@ parser::parser(environment const & env, io_state const & ios,
         m_variables          = s->m_vars;
         m_include_vars       = s->m_include_vars;
         m_imports_parsed     = s->m_imports_parsed;
+        m_ignore_noncomputable = s->m_noncomputable_theory;
         m_parser_scope_stack = s->m_parser_scope_stack;
         m_next_inst_idx      = s->m_next_inst_idx;
     }
-    m_ignore_noncomputable = false;
     m_profile     = ios.get_options().get_bool("profiler", false);
     m_in_quote = false;
     m_in_pattern = false;
@@ -2385,7 +2386,7 @@ void parser::save_snapshot(scope_message_context & smc, pos_info p) {
         m_snapshot_vector->push_back(std::make_shared<snapshot>(
                 m_env, smc.get_sub_buckets(), m_local_level_decls, m_local_decls,
                 m_level_variables, m_variables, m_include_vars,
-                m_ios.get_options(), m_imports_parsed, m_parser_scope_stack, m_next_inst_idx, p,
+                m_ios.get_options(), m_imports_parsed, m_ignore_noncomputable, m_parser_scope_stack, m_next_inst_idx, p,
                 m_required_successes));
     }
 }
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index 5e3d745392..ee86c43b3a 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -64,16 +64,17 @@ struct snapshot {
     name_set           m_include_vars; // subset of m_eds that must be included
     options            m_options;
     bool               m_imports_parsed;
+    bool               m_noncomputable_theory;
     parser_scope_stack m_parser_scope_stack;
     unsigned           m_next_inst_idx;
     pos_info           m_pos;
     list<generic_task_result> m_required_successes;
     snapshot(environment const & env, name_set const & sub_buckets, local_level_decls const & lds,
              local_expr_decls const & eds, name_set const & lvars, name_set const & vars,
-             name_set const & includes, options const & opts, bool imports_parsed, parser_scope_stack const & pss,
+             name_set const & includes, options const & opts, bool imports_parsed, bool noncomputable_theory, parser_scope_stack const & pss,
              unsigned next_inst_idx, pos_info const & pos, list<generic_task_result> const & required_successes):
         m_env(env), m_sub_buckets(sub_buckets), m_lds(lds), m_eds(eds), m_lvars(lvars), m_vars(vars), m_include_vars(includes),
-        m_options(opts), m_imports_parsed(imports_parsed), m_parser_scope_stack(pss), m_next_inst_idx(next_inst_idx), m_pos(pos),
+        m_options(opts), m_imports_parsed(imports_parsed), m_noncomputable_theory(noncomputable_theory), m_parser_scope_stack(pss), m_next_inst_idx(next_inst_idx), m_pos(pos),
         m_required_successes(required_successes) {}
 };