From e055e0b47cd97d4f4e9af2bb9ee3a93047d004aa Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 7 Dec 2012 10:41:50 -0800 Subject: [PATCH] Fixed other parameter setting problems Signed-off-by: Leonardo de Moura --- src/smt/tactic/smt_tactic.cpp | 1 + src/tactic/ufbv/ufbv_tactic.cpp | 3 +-- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/tactic/smt_tactic.cpp b/src/smt/tactic/smt_tactic.cpp index 2c7d58b1a..95b150a8c 100644 --- a/src/smt/tactic/smt_tactic.cpp +++ b/src/smt/tactic/smt_tactic.cpp @@ -139,6 +139,7 @@ public: ast_manager & m = in->m(); TRACE("smt_tactic", tout << this << "\nAUTO_CONFIG: " << fparams().m_auto_config << " HIDIV0: " << fparams().m_hi_div0 << " " << " PREPROCESS: " << fparams().m_preprocess << "\n"; + tout << "RELEVANCY: " << fparams().m_relevancy_lvl << "\n"; tout << "fail-if-inconclusive: " << m_fail_if_inconclusive << "\n"; tout << "params_ref: " << m_params_ref << "\n";); TRACE("smt_tactic_detail", in->display(tout);); diff --git a/src/tactic/ufbv/ufbv_tactic.cpp b/src/tactic/ufbv/ufbv_tactic.cpp index 80d403b67..9d16d7f9a 100644 --- a/src/tactic/ufbv/ufbv_tactic.cpp +++ b/src/tactic/ufbv/ufbv_tactic.cpp @@ -62,9 +62,8 @@ tactic * mk_ufbv_preprocessor_tactic(ast_manager & m, params_ref const & p) { tactic * mk_ufbv_tactic(ast_manager & m, params_ref const & p) { params_ref main_p(p); main_p.set_bool("mbqi", true); - main_p.set_uint("mbqi_max_iterations", -1); + main_p.set_uint("mbqi.max_iterations", UINT_MAX); main_p.set_bool("elim_and", true); - main_p.set_bool("solver", true); tactic * t = and_then(repeat(mk_ufbv_preprocessor_tactic(m, main_p), 2), mk_smt_tactic_using(false, main_p));