From 5706df30c6b1f969575954879b8ab32bee35ee0d Mon Sep 17 00:00:00 2001 From: Mikolas Janota Date: Fri, 8 Jan 2016 16:17:34 +0000 Subject: [PATCH] Fixing soft timeout for check-sat-using. --- src/ackr/lackr_tactic.cpp | 1 + src/cmd_context/tactic_cmds.cpp | 4 ++-- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/src/ackr/lackr_tactic.cpp b/src/ackr/lackr_tactic.cpp index 5e2b88e70..27cd12415 100644 --- a/src/ackr/lackr_tactic.cpp +++ b/src/ackr/lackr_tactic.cpp @@ -121,6 +121,7 @@ tactic * mk_lackr_tactic(ast_manager & m, params_ref const & p) { mk_max_bv_sharing_tactic(m), //mk_macro_finder_tactic(m, p), using_params(mk_simplify_tactic(m), simp2_p) + //, mk_simplify_tactic(m) //mk_nnf_tactic(m_m, m_p) ); diff --git a/src/cmd_context/tactic_cmds.cpp b/src/cmd_context/tactic_cmds.cpp index 81bf2136b..1c5da3829 100644 --- a/src/cmd_context/tactic_cmds.cpp +++ b/src/cmd_context/tactic_cmds.cpp @@ -187,8 +187,8 @@ public: tactic_ref tref = using_params(sexpr2tactic(ctx, m_tactic), p); tref->set_logic(ctx.get_logic()); ast_manager & m = ctx.m(); - unsigned timeout = p.get_uint("timeout", UINT_MAX); - unsigned rlimit = p.get_uint("rlimit", 0); + unsigned timeout = p.get_uint("timeout", ctx.params().m_timeout); + unsigned rlimit = p.get_uint("rlimit", ctx.params().m_rlimit); goal_ref g = alloc(goal, m, ctx.produce_proofs(), ctx.produce_models(), ctx.produce_unsat_cores()); assert_exprs_from(ctx, *g); TRACE("check_sat_using", g->display(tout););