diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 86b65f0755..2a85bcc703 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -2007,8 +2007,8 @@ expr parser::parse_tactic(unsigned) {
 
 /** \brief Helper class for creating type context only if needed */
 class lazy_type_context : public abstract_type_context {
-    environment const & m_env;
-    options const & m_opts;
+    environment m_env;
+    options     m_opts;
     std::unique_ptr<type_context> m_ctx;
     type_context & ctx() {
         if (!m_ctx)
diff --git a/tests/lean/server/crash1.input b/tests/lean/server/crash1.input
new file mode 100644
index 0000000000..8b19434204
--- /dev/null
+++ b/tests/lean/server/crash1.input
@@ -0,0 +1,6 @@
+{"command":"sync","file_name":"c:/Users/leonardo/projects/lean/build/debug/tst.lean","content":"def f : nat → nat\n| 0     := 0\n| (n+1) := f n + f n\n\nopen tactic\n\n\n\nmeta def tac : tactic unit :=\ndo x ← target,\n   y ← infer_type x >>= whnf,\n   trace y,\n   return ()\n"}
+{"command":"check"}
+{"command":"sync","file_name":"c:/Users/leonardo/projects/lean/build/debug/tst.lean","content":"def f : nat → nat\n| 0     := 0\n| (n+1) := f n + f n\n\nopen tactic\n\nset_option trace.compiler\n\nmeta def tac : tactic unit :=\ndo x ← target,\n   y ← infer_type x >>= whnf,\n   trace y,\n   return ()\n"}
+{"command":"check"}
+{"command":"sync","file_name":"c:/Users/leonardo/projects/lean/build/debug/tst.lean","content":"def f : nat → nat\n| 0     := 0\n| (n+1) := f n + f n\n\nopen tactic\n\nset_option trace.compiler true\n\nmeta def tac : tactic unit :=\ndo x ← target,\n   y ← infer_type x >>= whnf,\n   trace y,\n   return ()\n"}
+{"command":"check"}