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););