From d827713ce3e8e2be64b8d19ec9641735432db4bb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 22 Dec 2014 15:40:02 -0800 Subject: [PATCH] revert to SMT tactic on bv1_blaster_tactic - equalities are not removed, and conjunctions are not converted to NNF (or/not), so the formula still isn't sufficiently blasted Signed-off-by: Nikolaj Bjorner --- src/tactic/smtlogics/qfbv_tactic.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp index 916ae1386..b63cfcad3 100644 --- a/src/tactic/smtlogics/qfbv_tactic.cpp +++ b/src/tactic/smtlogics/qfbv_tactic.cpp @@ -105,7 +105,7 @@ tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat, tacti cond(mk_is_qfbv_probe(), cond(mk_is_qfbv_eq_probe(), and_then(mk_bv1_blaster_tactic(m), - using_params(sat, solver_p)), + using_params(smt, solver_p)), and_then(mk_bit_blaster_tactic(m), when(mk_lt(mk_memory_probe(), mk_const_probe(MEMLIMIT)), and_then(using_params(and_then(mk_simplify_tactic(m),