mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

add max conflict throttle to SAT based QFNIA tactic #7329

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-08-03 11:34:28 -07:00
parent 52f8eb21fb
commit 26b8d634a3
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/tactic/smtlogics/qfnia_tactic.cpp
View file

@ -45,6 +45,7 @@ static tactic * mk_qfnia_bv_solver(ast_manager & m, params_ref const & p_ref) {
params_ref mem_p = p; params_ref mem_p = p;
mem_p.set_uint("max_memory", 100); mem_p.set_uint("max_memory", 100);
mem_p.set_uint("max_conflicts", 500);
tactic * r = using_params(and_then(mk_simplify_tactic(m), 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), using_params(mk_simplify_tactic(m), simp2_p),
mk_max_bv_sharing_tactic(m), mk_max_bv_sharing_tactic(m),
using_params(mk_bit_blaster_tactic(m), mem_p), using_params(mk_bit_blaster_tactic(m), mem_p),
mk_sat_tactic(m)), mk_sat_tactic(m, mem_p)),
p); p);
return r; return r;
} }