From 55f59364a3213c85e0e1691e953242e15a830a8d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 6 Jan 2020 14:25:22 -0800 Subject: [PATCH] cap memory consumption on int2bv tactic to 100MB Signed-off-by: Nikolaj Bjorner --- src/tactic/smtlogics/qfnia_tactic.cpp | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/tactic/smtlogics/qfnia_tactic.cpp b/src/tactic/smtlogics/qfnia_tactic.cpp index cd956f3c6..1a22914f6 100644 --- a/src/tactic/smtlogics/qfnia_tactic.cpp +++ b/src/tactic/smtlogics/qfnia_tactic.cpp @@ -43,12 +43,15 @@ static tactic * mk_qfnia_bv_solver(ast_manager & m, params_ref const & p_ref) { simp2_p.set_bool("local_ctx", true); simp2_p.set_uint("local_ctx_limit", 10000000); + params_ref mem_p = p; + mem_p.set_uint("max_memory", 100); + tactic * r = using_params(and_then(mk_simplify_tactic(m), mk_propagate_values_tactic(m), using_params(mk_simplify_tactic(m), simp2_p), mk_max_bv_sharing_tactic(m), - mk_bit_blaster_tactic(m), + using_params(mk_bit_blaster_tactic(m), mem_p), mk_sat_tactic(m)), p); return r;