From ab39f06df7833f1f3a47efbac2e7e8db3741c5d3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 14 Dec 2017 17:22:49 -0800 Subject: [PATCH] fix crashes in nlsat Signed-off-by: Nikolaj Bjorner --- src/nlsat/nlsat_solver.cpp | 9 ++++++--- src/tactic/smtlogics/qfnia_tactic.cpp | 4 ++-- 2 files changed, 8 insertions(+), 5 deletions(-) diff --git a/src/nlsat/nlsat_solver.cpp b/src/nlsat/nlsat_solver.cpp index 0ccaa2f2c..0e3bf8c95 100644 --- a/src/nlsat/nlsat_solver.cpp +++ b/src/nlsat/nlsat_solver.cpp @@ -734,8 +734,10 @@ namespace nlsat { void undo_set_updt(interval_set * old_set) { SASSERT(m_xk != null_var); var x = m_xk; - m_ism.dec_ref(m_infeasible[x]); - m_infeasible[x] = old_set; + if (x < m_infeasible.size() && m_infeasible[x]) { + m_ism.dec_ref(m_infeasible[x]); + m_infeasible[x] = old_set; + } } void undo_new_stage() { @@ -757,7 +759,8 @@ namespace nlsat { void undo_updt_eq(atom * a) { SASSERT(m_xk != null_var); - m_var2eq[m_xk] = a; + if (m_var2eq.size() > m_xk) + m_var2eq[m_xk] = a; } template diff --git a/src/tactic/smtlogics/qfnia_tactic.cpp b/src/tactic/smtlogics/qfnia_tactic.cpp index f0a4ceb57..3b890b632 100644 --- a/src/tactic/smtlogics/qfnia_tactic.cpp +++ b/src/tactic/smtlogics/qfnia_tactic.cpp @@ -107,8 +107,8 @@ tactic * mk_qfnia_tactic(ast_manager & m, params_ref const & p) { simp_p.set_bool("som", true); // expand into sums of monomials return and_then(mk_qfnia_premable(m, p), - or_else(mk_qfnia_sat_solver(m, p), - mk_qfnia_nlsat_solver(m, p), + or_else(mk_qfnia_nlsat_solver(m, p), + mk_qfnia_sat_solver(m, p), and_then(using_params(mk_simplify_tactic(m), simp_p), mk_smt_tactic()))); }