From 1d6f53c31026ea80679cccc12932f8ba986d7f7b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 7 Sep 2017 05:32:07 -0700 Subject: [PATCH] fix #1248, fix #1249 Signed-off-by: Nikolaj Bjorner --- src/cmd_context/tactic_cmds.cpp | 3 +++ src/opt/opt_cmds.cpp | 3 +++ 2 files changed, 6 insertions(+) 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);