From b5496d823d255fa2c3bfe41fc27ddb28adf44f55 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 22 Apr 2021 23:14:28 -0700 Subject: [PATCH] #5211 --- src/ast/euf/euf_egraph.cpp | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp index 401958546..4ecc8fab0 100644 --- a/src/ast/euf/euf_egraph.cpp +++ b/src/ast/euf/euf_egraph.cpp @@ -281,12 +281,13 @@ namespace euf { VERIFY(n->num_args() == 0 || !n->merge_enabled() || m_table.contains(n)); } - void egraph::set_value(enode* n, lbool value) { - force_push(); - TRACE("euf", tout << bpp(n) << "\n";); - SASSERT(n->value() == l_undef); - n->set_value(value); - m_updates.push_back(update_record(n, update_record::value_assignment())); + void egraph::set_value(enode* n, lbool value) { + if (n->value() == l_undef) { + force_push(); + TRACE("euf", tout << bpp(n) << " := " << value << "\n";); + n->set_value(value); + m_updates.push_back(update_record(n, update_record::value_assignment())); + } } void egraph::set_lbl_hash(enode* n) {