From 5cf2caa7e9a35705bf78a38a5076b89f3b4790d5 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 12 Nov 2015 14:48:55 +0000 Subject: [PATCH] Added check for QF_BV in QF_UFBV tactic. --- src/tactic/smtlogics/qfufbv_tactic.cpp | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/src/tactic/smtlogics/qfufbv_tactic.cpp b/src/tactic/smtlogics/qfufbv_tactic.cpp index d10b7c1b4..816d69b1f 100644 --- a/src/tactic/smtlogics/qfufbv_tactic.cpp +++ b/src/tactic/smtlogics/qfufbv_tactic.cpp @@ -25,6 +25,7 @@ Notes: #include"max_bv_sharing_tactic.h" #include"bv_size_reduction_tactic.h" #include"reduce_args_tactic.h" +#include"qfbv_tactic.h" tactic * mk_qfufbv_tactic(ast_manager & m, params_ref const & p) { params_ref main_p; @@ -41,13 +42,11 @@ tactic * mk_qfufbv_tactic(ast_manager & m, params_ref const & p) { ); tactic * st = using_params(and_then(preamble_st, - mk_smt_tactic()), + cond(mk_is_qfbv_probe(), + mk_qfbv_tactic(m), + mk_smt_tactic())), main_p); - //cond(is_qfbv(), - // and_then(mk_bit_blaster(m), - // mk_sat_solver(m)), - // mk_smt_solver()) st->updt_params(p); return st; }