From 59b7845c7dc765a9c19074c43d288daccd753d68 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 17 Nov 2022 17:36:21 +0900
Subject: [PATCH] reset visited (fast mark) to not clash with occurs

---
 src/ast/euf/euf_egraph.cpp             |  6 +++---
 src/ast/euf/euf_egraph.h               |  2 +-
 src/ast/simplifiers/euf_completion.cpp | 22 +++++++++++++---------
 src/ast/simplifiers/solve_eqs.cpp      |  3 ++-
 4 files changed, 19 insertions(+), 14 deletions(-)

diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp
index c8605b297c2..666a7fad690 100644
--- a/src/ast/euf/euf_egraph.cpp
+++ b/src/ast/euf/euf_egraph.cpp
@@ -451,7 +451,7 @@ namespace euf {
             add_literal(n1, false);
         if (n1->is_equality() && n1->value() == l_false)
             new_diseq(n1);
-        remove_parents(r1, r2);
+        remove_parents(r1);
         push_eq(r1, n1, r2->num_parents());
         merge_justification(n1, n2, j);
         for (enode* c : enode_class(n1)) 
@@ -464,8 +464,8 @@ namespace euf {
             cb(r2, r1);
     }
 
-    void egraph::remove_parents(enode* r1, enode* r2) {
-        for (enode* p : enode_parents(r1)) {
+    void egraph::remove_parents(enode* r) {
+        for (enode* p : enode_parents(r)) {
             if (p->is_marked1())
                 continue;
             if (p->merge_enabled()) {
diff --git a/src/ast/euf/euf_egraph.h b/src/ast/euf/euf_egraph.h
index 53aaf481ada..d6bcb9cd31c 100644
--- a/src/ast/euf/euf_egraph.h
+++ b/src/ast/euf/euf_egraph.h
@@ -220,7 +220,7 @@ namespace euf {
         void merge_th_eq(enode* n, enode* root);
         void merge_justification(enode* n1, enode* n2, justification j);
         void reinsert_parents(enode* r1, enode* r2);
-        void remove_parents(enode* r1, enode* r2);
+        void remove_parents(enode* r);
         void unmerge_justification(enode* n1);
         void reinsert_equality(enode* p);
         void update_children(enode* n);
diff --git a/src/ast/simplifiers/euf_completion.cpp b/src/ast/simplifiers/euf_completion.cpp
index 9860b48b2bf..ac1ecc47aad 100644
--- a/src/ast/simplifiers/euf_completion.cpp
+++ b/src/ast/simplifiers/euf_completion.cpp
@@ -80,18 +80,22 @@ namespace euf {
         };
 
         for (unsigned i = m_qhead; i < sz; ++i) {
-            auto [f,d] = m_fmls[i]();
-            auto* n = mk_enode(f);
-            if (m.is_eq(f)) {
-                m_egraph.merge(n->get_arg(0), n->get_arg(1), d);
-                add_children(n->get_arg(0));
-                add_children(n->get_arg(1));
+            expr* x, * y;
+            auto [f, d] = m_fmls[i]();
+            if (m.is_eq(f, x, y)) {
+                enode* a = mk_enode(x);
+                enode* b = mk_enode(y);
+                m_egraph.merge(a, b, d);
+                add_children(a);
+                add_children(b);
             }
-            if (m.is_not(f)) {
-                m_egraph.merge(n->get_arg(0), m_ff, d);
-                add_children(n->get_arg(0));
+            else if (m.is_not(f, f)) {
+                enode* n = mk_enode(f);
+                m_egraph.merge(n, m_ff, d);
+                add_children(n);
             }
             else {
+                enode* n = mk_enode(f);
                 m_egraph.merge(n, m_tt, d);
                 add_children(n);
             }
diff --git a/src/ast/simplifiers/solve_eqs.cpp b/src/ast/simplifiers/solve_eqs.cpp
index f66f64b6d85..5090e1b438c 100644
--- a/src/ast/simplifiers/solve_eqs.cpp
+++ b/src/ast/simplifiers/solve_eqs.cpp
@@ -129,7 +129,8 @@ namespace euf {
                             todo.push_back(var2id(e));
                     }
                     m_todo.reset();
-                    
+                    visited.reset();
+
                     if (!is_safe) {
                         todo.shrink(todo_sz);
                         continue;