mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fix qe for undef scenarios, codeplex issue 130
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
c6683fd6fa
commit
18e77bd539
|
@ -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<expr_replacer> 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<expr_replacer> 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);
|
||||
|
|
Loading…
Reference in a new issue