From 3eeb59db34172f673d4ea54c1ec9ca191997fb5e Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 14 Nov 2022 19:23:27 -0800
Subject: [PATCH] fix #6451 missing occurrence marking when there is an unsafe
 equality already

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/simplifiers/solve_context_eqs.cpp | 11 +++++++++--
 src/ast/simplifiers/solve_eqs.cpp         |  2 +-
 2 files changed, 10 insertions(+), 3 deletions(-)

diff --git a/src/ast/simplifiers/solve_context_eqs.cpp b/src/ast/simplifiers/solve_context_eqs.cpp
index 37836db27..1ccab0f6c 100644
--- a/src/ast/simplifiers/solve_context_eqs.cpp
+++ b/src/ast/simplifiers/solve_context_eqs.cpp
@@ -154,10 +154,12 @@ namespace euf {
                 return e1.var->get_id() < e2.var->get_id(); });
         unsigned j = 0;
         expr* last_var = nullptr;
+        bool was_unsafe = false;
         for (auto const& eq : eqs) {
 
             SASSERT(!m.is_bool(eq.var));
 
+
             if (eq.var != last_var) {
 
                 m_contains_v.reset();
@@ -167,8 +169,11 @@ namespace euf {
                 mark_occurs(m_todo, eq.var, m_contains_v);
                 SASSERT(m_todo.empty());
                 last_var = eq.var;
-                if (m_contains_v.is_marked(eq.term))
+                was_unsafe = false;
+                if (m_contains_v.is_marked(eq.term)) {
+                    was_unsafe = true;
                     continue;
+                }
 
                 // then mark occurrences
                 for (unsigned i = 0; i < m_fmls.size(); ++i)
@@ -178,7 +183,9 @@ namespace euf {
             }
             else if (m_contains_v.is_marked(eq.term))
                 continue;
-
+            else if (was_unsafe) 
+                continue;
+            
             // subject to occurrences, check if equality is safe
             if (is_safe_eq(eq.orig)) 
                 eqs[j++] = eq;
diff --git a/src/ast/simplifiers/solve_eqs.cpp b/src/ast/simplifiers/solve_eqs.cpp
index 18928dca8..0b6f12160 100644
--- a/src/ast/simplifiers/solve_eqs.cpp
+++ b/src/ast/simplifiers/solve_eqs.cpp
@@ -197,7 +197,7 @@ namespace euf {
         if (!m.inc())
             return;
 
-        if (m_config.m_context_solve && false) {            
+        if (m_config.m_context_solve) {            
             old_fmls.reset();
             m_subst_ids.reset();
             eqs.reset();