From 2f01b5b567cff438b686c4b565130fc1e7f1abfe Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 29 Nov 2023 14:00:17 -0800 Subject: [PATCH] re-enable delayed literal propagation --- src/ast/euf/euf_egraph.cpp | 2 +- src/sat/smt/euf_solver.cpp | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp index 0d820ad8b..d370ceed3 100644 --- a/src/ast/euf/euf_egraph.cpp +++ b/src/ast/euf/euf_egraph.cpp @@ -83,7 +83,7 @@ namespace euf { void egraph::reinsert_equality(enode* p) { SASSERT(p->is_equality()); if (p->value() != l_true && p->get_arg(0)->get_root() == p->get_arg(1)->get_root()) - add_literal(p, nullptr); + queue_literal(p, nullptr); } void egraph::queue_literal(enode* p, enode* ante) { diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index 6a6b43650..d25df5b06 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -1059,6 +1059,7 @@ namespace euf { }; r->m_egraph.copy_from(m_egraph, copy_justification); r->set_solver(s); + r->m_egraph.copy_from(m_egraph, copy_justification); for (euf::enode* n : r->m_egraph.nodes()) { auto b = n->bool_var(); if (b != sat::null_bool_var) {