From 12458b1a8404398e6d3aeb08085cb3065006a939 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Mon, 22 Feb 2016 10:22:56 +0000 Subject: [PATCH] remove dead code in qfufbv --- src/tactic/smtlogics/qfufbv_tactic.cpp | 8 ++------ 1 file changed, 2 insertions(+), 6 deletions(-) diff --git a/src/tactic/smtlogics/qfufbv_tactic.cpp b/src/tactic/smtlogics/qfufbv_tactic.cpp index f943b68c9..421a76cc7 100644 --- a/src/tactic/smtlogics/qfufbv_tactic.cpp +++ b/src/tactic/smtlogics/qfufbv_tactic.cpp @@ -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),