mirror of
https://github.com/Z3Prover/z3
synced 2025-04-10 03:07:07 +00:00
This commit is contained in:
parent
c6f0afa008
commit
bdf6a17b89
|
@ -175,7 +175,7 @@ namespace array {
|
|||
ptr_buffer<expr> sel1_args, sel2_args;
|
||||
unsigned num_args = select->get_num_args();
|
||||
|
||||
if (expr2enode(select->get_arg(0))->get_root() == expr2enode(store)->get_root())
|
||||
if (select->get_arg(0) != store && expr2enode(select->get_arg(0))->get_root() == expr2enode(store)->get_root())
|
||||
return false;
|
||||
bool has_diff = false;
|
||||
for (unsigned i = 1; i < num_args; i++)
|
||||
|
|
|
@ -73,6 +73,7 @@ namespace euf {
|
|||
values2model(deps, mdl);
|
||||
for (auto* mb : m_solvers)
|
||||
mb->finalize_model(*mdl);
|
||||
TRACE("model", tout << "created model " << *mdl << "\n";);
|
||||
validate_model(*mdl);
|
||||
}
|
||||
|
||||
|
|
|
@ -106,8 +106,8 @@ namespace euf {
|
|||
|
||||
TRACE("euf",
|
||||
for (enode* n : m_egraph.nodes())
|
||||
if (is_relevant(n))
|
||||
tout << "relevant " << mk_bounded_pp(n->get_expr(), m) << "\n";);
|
||||
return true;
|
||||
if (is_relevant(n))
|
||||
tout << "relevant " << n->get_expr_id() << " [r" << n->get_root_id() << "]: " << mk_bounded_pp(n->get_expr(), m) << "\n";);
|
||||
return true;
|
||||
}
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue