From 020620aadd5aca05547aaa51b7f66122932283a6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 23 Jun 2015 14:05:49 +0200 Subject: [PATCH] disable qf-ufnra tactic from default for testing Signed-off-by: Nikolaj Bjorner --- src/tactic/portfolio/default_tactic.cpp | 4 ++-- src/tactic/portfolio/smt_strategic_solver.cpp | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/src/tactic/portfolio/default_tactic.cpp b/src/tactic/portfolio/default_tactic.cpp index 72c486c24..4f5eb5ed0 100644 --- a/src/tactic/portfolio/default_tactic.cpp +++ b/src/tactic/portfolio/default_tactic.cpp @@ -44,8 +44,8 @@ tactic * mk_default_tactic(ast_manager & m, params_ref const & p) { cond(mk_is_nra_probe(), mk_nra_tactic(m), cond(mk_is_lira_probe(), mk_lira_tactic(m, p), cond(mk_is_qffp_probe(), mk_qffp_tactic(m, p), - cond(mk_is_qfufnra_probe(), mk_qfufnra_tactic(m, p), - mk_smt_tactic())))))))))))), + //cond(mk_is_qfufnra_probe(), mk_qfufnra_tactic(m, p), + mk_smt_tactic()))))))))))), p); return st; } diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index 27d7433e8..c868fdcb9 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -86,8 +86,8 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const return mk_qffpbv_tactic(m, p); else if (logic=="HORN") return mk_horn_tactic(m, p); - else if (logic=="QF_UFNRA") - return mk_qfufnra_tactic(m, p); + //else if (logic=="QF_UFNRA") + // return mk_qfufnra_tactic(m, p); else return mk_default_tactic(m, p); }