From 4abce8e0c3700259f82cd20da30eb5b13ff26c8c Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 30 Oct 2012 17:09:09 +0000 Subject: [PATCH] UFBV performance fix Signed-off-by: Christoph M. Wintersteiger --- src/tactic/ufbv/ufbv_tactic.cpp | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/tactic/ufbv/ufbv_tactic.cpp b/src/tactic/ufbv/ufbv_tactic.cpp index de8ac875b..85ec506aa 100644 --- a/src/tactic/ufbv/ufbv_tactic.cpp +++ b/src/tactic/ufbv/ufbv_tactic.cpp @@ -66,11 +66,8 @@ tactic * mk_ufbv_tactic(ast_manager & m, params_ref const & p) { main_p.set_bool(":elim-and", true); main_p.set_bool(":solver", true); - params_ref smt_p(p); - smt_p.set_bool(":auto-config", false); - tactic * t = and_then(repeat(mk_ufbv_preprocessor_tactic(m, main_p), 2), - using_params(mk_smt_tactic(smt_p), main_p)); + mk_smt_tactic_using(false, main_p)); t->updt_params(p);