mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

remove dead code in qfufbv

Browse source
This commit is contained in:
Nuno Lopes 2016-02-22 10:22:56 +00:00
parent 63c138c08e
commit 12458b1a84
1 changed files with 2 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/tactic/smtlogics/qfufbv_tactic.cpp
View file

@ -124,7 +124,7 @@ private:
};
tactic * mk_qfufbv_preamble1(ast_manager & m, params_ref const & p) {
static tactic * mk_qfufbv_preamble1(ast_manager & m, params_ref const & p) {
params_ref simp2_p = p;
simp2_p.set_bool("pull_cheap_ite", true);
simp2_p.set_bool("push_ite_bv", false);
@ -150,11 +150,7 @@ tactic * mk_qfufbv_preamble1(ast_manager & m, params_ref const & p) {
);
}
tactic * mk_qfufbv_preamble(ast_manager & m, params_ref const & p) {
params_ref main_p;
main_p.set_bool("elim_and", true);
main_p.set_bool("blast_distinct", true);
static tactic * mk_qfufbv_preamble(ast_manager & m, params_ref const & p) {
return and_then(mk_simplify_tactic(m),
mk_propagate_values_tactic(m),
mk_solve_eqs_tactic(m),