From a21d701fa1066d34d906b06d0bcd2f5b8d975f0f Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 13 Jul 2016 15:36:21 +0100 Subject: [PATCH] tabs --- src/tactic/ufbv/ufbv_tactic.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/tactic/ufbv/ufbv_tactic.cpp b/src/tactic/ufbv/ufbv_tactic.cpp index 9d16d7f9a..b5a4ca3a3 100644 --- a/src/tactic/ufbv/ufbv_tactic.cpp +++ b/src/tactic/ufbv/ufbv_tactic.cpp @@ -40,12 +40,12 @@ tactic * mk_ufbv_preprocessor_tactic(ast_manager & m, params_ref const & p) { no_elim_and.set_bool("elim_and", false); return and_then( - mk_trace_tactic("ufbv_pre"), + mk_trace_tactic("ufbv_pre"), and_then(mk_simplify_tactic(m, p), mk_propagate_values_tactic(m, p), and_then(using_params(mk_macro_finder_tactic(m, no_elim_and), no_elim_and), - mk_simplify_tactic(m, p)), - and_then(mk_snf_tactic(m, p), mk_simplify_tactic(m, p)), + mk_simplify_tactic(m, p)), + and_then(mk_snf_tactic(m, p), mk_simplify_tactic(m, p)), mk_elim_and_tactic(m, p), mk_solve_eqs_tactic(m, p), and_then(mk_der_fp_tactic(m, p), mk_simplify_tactic(m, p)), @@ -56,7 +56,7 @@ tactic * mk_ufbv_preprocessor_tactic(ast_manager & m, params_ref const & p) { and_then(mk_quasi_macros_tactic(m, p), mk_simplify_tactic(m, p)), and_then(mk_der_fp_tactic(m, p), mk_simplify_tactic(m, p)), mk_simplify_tactic(m, p)), - mk_trace_tactic("ufbv_post")); + mk_trace_tactic("ufbv_post")); } tactic * mk_ufbv_tactic(ast_manager & m, params_ref const & p) {