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

add lia2card tactic as default #7483

Browse source
This commit is contained in:
Nikolaj Bjorner 2024-12-21 13:11:22 +01:00
parent 4f7b6c794e
commit 8dec84110b
1 changed files with 2 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/tactic/smtlogics/qflia_tactic.cpp
View file

@ -26,6 +26,7 @@ Notes:
#include "tactic/arith/add_bounds_tactic.h"
#include "tactic/arith/pb2bv_tactic.h"
#include "tactic/arith/lia2pb_tactic.h"
#include "tactic/arith/lia2card_tactic.h"
#include "tactic/core/ctx_simplify_tactic.h"
#include "tactic/bv/bit_blaster_tactic.h"
#include "tactic/bv/max_bv_sharing_tactic.h"
@ -198,6 +199,7 @@ tactic * mk_preamble_tactic(ast_manager& m) {
using_params(mk_ctx_simplify_tactic(m), ctx_simp_p),
using_params(mk_simplify_tactic(m), pull_ite_p),
mk_solve_eqs_tactic(m),
mk_lia2card_tactic(m),
mk_elim_uncnstr_tactic(m));
}