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

#5211

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-04-22 23:14:28 -07:00
parent d2f15d1b1a
commit b5496d823d
1 changed files with 7 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/ast/euf/euf_egraph.cpp
View file

@ -281,12 +281,13 @@ namespace euf {
VERIFY(n->num_args() == 0 || !n->merge_enabled() || m_table.contains(n)); VERIFY(n->num_args() == 0 || !n->merge_enabled() || m_table.contains(n));
} }
void egraph::set_value(enode* n, lbool value) { void egraph::set_value(enode* n, lbool value) {
force_push(); if (n->value() == l_undef) {
TRACE("euf", tout << bpp(n) << "\n";); force_push();
SASSERT(n->value() == l_undef); TRACE("euf", tout << bpp(n) << " := " << value << "\n";);
n->set_value(value); n->set_value(value);
m_updates.push_back(update_record(n, update_record::value_assignment())); m_updates.push_back(update_record(n, update_record::value_assignment()));
}
} }
void egraph::set_lbl_hash(enode* n) { void egraph::set_lbl_hash(enode* n) {