From 0ccd56b8470b6535368175eadb8dfbb4e3f5d4cc Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 5 Oct 2014 18:33:20 -0700 Subject: [PATCH] fix qe on undef Signed-off-by: Nikolaj Bjorner --- src/qe/qe.cpp | 25 +++++++++++++++++-------- 1 file changed, 17 insertions(+), 8 deletions(-) diff --git a/src/qe/qe.cpp b/src/qe/qe.cpp index 17a1ccb1d..7275ff71f 100644 --- a/src/qe/qe.cpp +++ b/src/qe/qe.cpp @@ -1449,11 +1449,19 @@ namespace qe { m_solver.assert_expr(m_fml); if (assumption) m_solver.assert_expr(assumption); - bool is_sat = false; - while (l_true == m_solver.check()) { - is_sat = true; + bool is_sat = false; + lbool res = l_true; + while (res == l_true) { + res = m_solver.check(); + if (res == l_true) is_sat = true; final_check(); } + if (res == l_undef) { + free_vars.append(num_vars, vars); + reset(); + m_solver.pop(1); + return; + } if (!is_sat) { fml = m.mk_false(); @@ -1484,12 +1492,13 @@ namespace qe { ); free_vars.append(m_free_vars); - SASSERT(!m_free_vars.empty() || m_solver.inconsistent()); + if (!m_free_vars.empty() || m_solver.inconsistent()) { - if (m_fml.get() != m_subfml.get()) { - scoped_ptr rp = mk_default_expr_replacer(m); - rp->apply_substitution(to_app(m_subfml.get()), fml, m_fml); - fml = m_fml; + if (m_fml.get() != m_subfml.get()) { + scoped_ptr rp = mk_default_expr_replacer(m); + rp->apply_substitution(to_app(m_subfml.get()), fml, m_fml); + fml = m_fml; + } } reset(); m_solver.pop(1);