mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 06:03:23 +00:00
Code Activity

fix qe on undef

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-10-05 18:33:20 -07:00
parent c706e91019
commit 0ccd56b847
1 changed files with 17 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

23
src/qe/qe.cpp
View file

@ -1450,10 +1450,18 @@ namespace qe {
m_solver.assert_expr(m_fml); m_solver.assert_expr(m_fml);
if (assumption) m_solver.assert_expr(assumption); if (assumption) m_solver.assert_expr(assumption);
bool is_sat = false; bool is_sat = false;
while (l_true == m_solver.check()) { lbool res = l_true;
is_sat = true; while (res == l_true) {
res = m_solver.check();
if (res == l_true) is_sat = true;
final_check(); final_check();
} }
if (res == l_undef) {
free_vars.append(num_vars, vars);
reset();
m_solver.pop(1);
return;
}
if (!is_sat) { if (!is_sat) {
fml = m.mk_false(); fml = m.mk_false();
@ -1484,12 +1492,13 @@ namespace qe {
); );
free_vars.append(m_free_vars); 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()) { if (m_fml.get() != m_subfml.get()) {
scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m); scoped_ptr<expr_replacer> rp = mk_default_expr_replacer(m);
rp->apply_substitution(to_app(m_subfml.get()), fml, m_fml); rp->apply_substitution(to_app(m_subfml.get()), fml, m_fml);
fml = m_fml; fml = m_fml;
}
} }
reset(); reset();
m_solver.pop(1); m_solver.pop(1);