From 8c92cf1b32aed5a9b2951214680ec0ebba997b1d Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 8 May 2020 22:34:03 -0700 Subject: [PATCH] restore the tactics with nlsat Signed-off-by: Lev Nachmanson --- src/tactic/smtlogics/qfnra_tactic.cpp | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/src/tactic/smtlogics/qfnra_tactic.cpp b/src/tactic/smtlogics/qfnra_tactic.cpp index 4d7c2b28f..7d93abe25 100644 --- a/src/tactic/smtlogics/qfnra_tactic.cpp +++ b/src/tactic/smtlogics/qfnra_tactic.cpp @@ -44,14 +44,12 @@ tactic * mk_qfnra_tactic(ast_manager & m, params_ref const& p) { return and_then(mk_simplify_tactic(m, p), mk_propagate_values_tactic(m, p), - //or_else(//try_for(mk_qfnra_nlsat_tactic(m, p0), 5000), - //try_for(mk_qfnra_nlsat_tactic(m, p1), 10000), - //mk_qfnra_sat_solver(m, p, 4), - //and_then(try_for(mk_smt_tactic(m), 5000), mk_fail_if_undecided_tactic()), - mk_qfnra_sat_solver(m, p, 6) - //mk_qfnra_nlsat_tactic(m, p2) - //) - ); + or_else(try_for(mk_qfnra_nlsat_tactic(m, p0), 5000), + try_for(mk_qfnra_nlsat_tactic(m, p1), 10000), + mk_qfnra_sat_solver(m, p, 4), + and_then(try_for(mk_smt_tactic(m), 5000), mk_fail_if_undecided_tactic()), + mk_qfnra_sat_solver(m, p, 6), + mk_qfnra_nlsat_tactic(m, p2))); }