From f3e71e52fcd033778e5f863e72cfafeb7d03e05f Mon Sep 17 00:00:00 2001 From: Daniel Selsam Date: Sat, 11 Mar 2017 19:09:17 -0800 Subject: [PATCH] feat(frontends/smt2/parser.cpp): allow tracing from the smt tactic --- src/frontends/smt2/parser.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/frontends/smt2/parser.cpp b/src/frontends/smt2/parser.cpp index fe669cbe36..a5eefc2947 100644 --- a/src/frontends/smt2/parser.cpp +++ b/src/frontends/smt2/parser.cpp @@ -482,7 +482,11 @@ private: vm_state state(env(), ios().get_options()); scope_vm_state scope(state); + type_context stctx(env(), ios().get_options(), mctx, lctx()); + scope_trace_env scope_trace(m_env, stctx.get_options(), stctx); + vm_obj result = state.invoke(get_smt_prove_name(), s); + if (optional s_new = tactic::is_success(result)) { mctx = s_new->mctx(); expr proof = mctx.instantiate_mvars(goal_mvar);