diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp index b5ad0707d..14c715eca 100644 --- a/src/cmd_context/tactic_cmds.cpp +++ b/src/cmd_context/tactic_cmds.cpp @@ -197,6 +197,9 @@ public: } virtual void execute(cmd_context & ctx) { + if (!m_tactic) { + throw cmd_exception("check-sat-using needs a tactic argument"); + } params_ref p = ctx.params().merge_default_params(ps()); tactic_ref tref = using_params(sexpr2tactic(ctx, m_tactic), p); tref->set_logic(ctx.get_logic()); diff --git a/src/opt/opt_cmds.cpp b/src/opt/opt_cmds.cpp index 7ca2be4aa..89264a9c8 100644 --- a/src/opt/opt_cmds.cpp +++ b/src/opt/opt_cmds.cpp @@ -96,6 +96,9 @@ public: } virtual void execute(cmd_context & ctx) { + if (!m_formula) { + throw cmd_exception("assert-soft requires a formulas as argument."); + } symbol w("weight"); rational weight = ps().get_rat(symbol("weight"), rational::one()); symbol id = ps().get_sym(symbol("id"), symbol::null);