From b0de6723ecff9ecfc2afe17c234e0ef122f26027 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 5 Jan 2017 13:32:59 -0800 Subject: [PATCH] feat(frontends/lean/tactic_evaluator): better error message --- src/frontends/lean/tactic_evaluator.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/frontends/lean/tactic_evaluator.cpp b/src/frontends/lean/tactic_evaluator.cpp index be21f45fa9..2606027b10 100644 --- a/src/frontends/lean/tactic_evaluator.cpp +++ b/src/frontends/lean/tactic_evaluator.cpp @@ -189,7 +189,10 @@ pair tactic_evaluator::mk_smt_state(tactic_state const & s if (is_tactic_result_success(r)) { return mk_pair(get_tactic_result_value(r), to_tactic_state(get_tactic_result_state(r))); } - throw elaborator_exception(ref, "failed to execute smt_tactic, initial smt_state could not be constructed"); + tactic_exception_info info = *is_tactic_exception(S, r); + throw elaborator_exception(ref, + format("failed to execute smt_tactic, initial smt_state could not be constructed, nested error:") + + line() + std::get<0>(info)); } pair tactic_evaluator::execute_smt_begin_end_core(vm_obj const & ss, tactic_state const & ts, buffer const & tactics, expr const & ref) {