From 26b8d634a318b3aa0bacbcbaadbf8e5234d21034 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 3 Aug 2024 11:34:28 -0700 Subject: [PATCH] add max conflict throttle to SAT based QFNIA tactic #7329 Signed-off-by: Nikolaj Bjorner --- src/tactic/smtlogics/qfnia_tactic.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/tactic/smtlogics/qfnia_tactic.cpp b/src/tactic/smtlogics/qfnia_tactic.cpp index 0dad56a19..25dc34d9c 100644 --- a/src/tactic/smtlogics/qfnia_tactic.cpp +++ b/src/tactic/smtlogics/qfnia_tactic.cpp @@ -45,6 +45,7 @@ static tactic * mk_qfnia_bv_solver(ast_manager & m, params_ref const & p_ref) { params_ref mem_p = p; mem_p.set_uint("max_memory", 100); + mem_p.set_uint("max_conflicts", 500); tactic * r = using_params(and_then(mk_simplify_tactic(m), @@ -52,7 +53,7 @@ static tactic * mk_qfnia_bv_solver(ast_manager & m, params_ref const & p_ref) { using_params(mk_simplify_tactic(m), simp2_p), mk_max_bv_sharing_tactic(m), using_params(mk_bit_blaster_tactic(m), mem_p), - mk_sat_tactic(m)), + mk_sat_tactic(m, mem_p)), p); return r; }