From bb7b3c510f59ec1502e90d2ab8f3b41b2c92bfa7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 26 Jul 2017 19:52:05 -0700 Subject: [PATCH] fix for #1161 Signed-off-by: Nikolaj Bjorner --- src/cmd_context/tactic_cmds.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp index 2b60486f7..119deec8c 100644 --- a/src/cmd_context/tactic_cmds.cpp +++ b/src/cmd_context/tactic_cmds.cpp @@ -308,6 +308,9 @@ public: } virtual void execute(cmd_context & ctx) { + if (!m_tactic) { + throw cmd_exception("apply needs a tactic argument"); + } params_ref p = ctx.params().merge_default_params(ps()); tactic_ref tref = using_params(sexpr2tactic(ctx, m_tactic), p); {