From 98975e518715b60722df294487df6e105935ef9f Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 27 May 2015 14:47:24 +0100 Subject: [PATCH] Reordered the default qflia probe to be checked before the more permissive qfauflia. --- src/tactic/portfolio/default_tactic.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/tactic/portfolio/default_tactic.cpp b/src/tactic/portfolio/default_tactic.cpp index ad811cc70..72c486c24 100644 --- a/src/tactic/portfolio/default_tactic.cpp +++ b/src/tactic/portfolio/default_tactic.cpp @@ -35,9 +35,9 @@ Notes: tactic * mk_default_tactic(ast_manager & m, params_ref const & p) { tactic * st = using_params(and_then(mk_simplify_tactic(m), cond(mk_is_qfbv_probe(), mk_qfbv_tactic(m), - cond(mk_is_qfaufbv_probe(), mk_qfaufbv_tactic(m), - cond(mk_is_qfauflia_probe(), mk_qfauflia_tactic(m), + cond(mk_is_qfaufbv_probe(), mk_qfaufbv_tactic(m), cond(mk_is_qflia_probe(), mk_qflia_tactic(m), + cond(mk_is_qfauflia_probe(), mk_qfauflia_tactic(m), cond(mk_is_qflra_probe(), mk_qflra_tactic(m), cond(mk_is_qfnra_probe(), mk_qfnra_tactic(m), cond(mk_is_qfnia_probe(), mk_qfnia_tactic(m),