mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

#5518

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-08-31 14:21:10 -07:00
parent 07bbd026ac
commit 34c8f598a5
2 changed files with 4 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/sat/smt/array_solver.h
View file

@ -267,6 +267,6 @@ namespace array {
void after_merge_eh(theory_var r1, theory_var r2, theory_var v1, theory_var v2) {}
void unmerge_eh(theory_var v1, theory_var v2) {}
euf::enode_vector const& parent_selects(euf::enode* n) const { return m_var_data[n->get_th_var(get_id())]->m_parent_selects; }
euf::enode_vector const& parent_selects(euf::enode* n) { return m_var_data[find(n->get_th_var(get_id()))]->m_parent_selects; }
};
}

5
src/sat/smt/euf_model.cpp
View file

@ -63,6 +63,7 @@ namespace euf {
};
void solver::update_model(model_ref& mdl) {
TRACE("model", tout << "create model\n";);
mdl->reset_eval_cache();
for (auto* mb : m_solvers)
mb->init_model();
@ -117,7 +118,7 @@ namespace euf {
for (enode* n : fresh_values)
n->unmark1();
TRACE("euf",
TRACE("model",
for (auto const& d : deps.deps())
if (d.m_value) {
tout << bpp(d.m_key) << ":\n";
@ -254,7 +255,7 @@ namespace euf {
m_values2root.insert(m_values.get(n->get_expr_id()), n);
TRACE("model",
for (auto kv : m_values2root)
tout << mk_pp(kv.m_key, m) << " -> " << bpp(kv.m_value) << "\n";);
tout << mk_bounded_pp(kv.m_key, m) << "\n -> " << bpp(kv.m_value) << "\n";);
return m_values2root;
}