mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 01:24:08 +00:00
deal with cancellation in qe for #6500
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
ecf25a4fe2
commit
603597a22e
|
@ -1437,13 +1437,12 @@ namespace qe {
|
|||
res = m_solver.check();
|
||||
if (res == l_true && has_uninterpreted(m, m_fml))
|
||||
res = l_undef;
|
||||
if (res == l_true) {
|
||||
if (res == l_true)
|
||||
res = final_check();
|
||||
if (res == l_true)
|
||||
is_sat = true;
|
||||
final_check();
|
||||
}
|
||||
else {
|
||||
else
|
||||
break;
|
||||
}
|
||||
}
|
||||
if (res == l_undef) {
|
||||
free_vars.append(num_vars, vars);
|
||||
|
@ -1501,30 +1500,33 @@ namespace qe {
|
|||
|
||||
private:
|
||||
|
||||
void final_check() {
|
||||
model_ref model;
|
||||
lbool final_check() {
|
||||
model_ref model;
|
||||
m_solver.get_model(model);
|
||||
if (!model)
|
||||
return l_undef;
|
||||
scoped_ptr<model_evaluator> model_eval = alloc(model_evaluator, *model);
|
||||
|
||||
while (true) {
|
||||
while (m.inc()) {
|
||||
TRACE("qe", model_v2_pp(tout, *model););
|
||||
while (can_propagate_assignment(*model_eval)) {
|
||||
while (can_propagate_assignment(*model_eval))
|
||||
propagate_assignment(*model_eval);
|
||||
}
|
||||
VERIFY(CHOOSE_VAR == update_current(*model_eval, true));
|
||||
SASSERT(m_current->fml());
|
||||
if (l_true != m_solver.check()) {
|
||||
return;
|
||||
return l_true;
|
||||
}
|
||||
m_solver.get_model(model);
|
||||
model_eval = alloc(model_evaluator, *model);
|
||||
search_tree* st = m_current;
|
||||
update_current(*model_eval, false);
|
||||
if (st == m_current) {
|
||||
if (st == m_current)
|
||||
break;
|
||||
}
|
||||
}
|
||||
pop(*model_eval);
|
||||
}
|
||||
if (!m.inc())
|
||||
return l_undef;
|
||||
pop(*model_eval);
|
||||
return l_true;
|
||||
}
|
||||
|
||||
ast_manager& get_manager() override { return m; }
|
||||
|
|
Loading…
Reference in a new issue