#5528

Z3Prover · Sep 2, 2021 · 6907d30 · 6907d30
1 parent a74c01c
commit 6907d30
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
@@ -489,7 +489,8 @@ namespace euf {
 
     bool solver::merge_shared_bools() {
         bool merged = false;
-        for (euf::enode* n : m_egraph.nodes()) {
+        for (unsigned i = m_egraph.nodes().size(); i-- > 0; ) {
+            euf::enode* n = m_egraph.nodes()[i];
             if (!is_shared(n) || !m.is_bool(n->get_expr()))
                 continue;
             if (n->value() == l_true && !m.is_true(n->get_root()->get_expr())) {