From 8dec84110bcd3b17458a237ef350209e69b803b4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 21 Dec 2024 13:11:22 +0100 Subject: [PATCH] add lia2card tactic as default #7483 --- src/tactic/smtlogics/qflia_tactic.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/tactic/smtlogics/qflia_tactic.cpp b/src/tactic/smtlogics/qflia_tactic.cpp index e72a63087..981127fab 100644 --- a/src/tactic/smtlogics/qflia_tactic.cpp +++ b/src/tactic/smtlogics/qflia_tactic.cpp @@ -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)); }