From a3ec6a0f1b9da39999ec8f9d233fbafc36b301f0 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 7 Nov 2025 08:03:37 -0800
Subject: [PATCH] add delayed diseq check

---
 src/smt/theory_lra.cpp | 26 +++++++++++++++++++++++++-
 1 file changed, 25 insertions(+), 1 deletion(-)

diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index db8877654..283bf4ca8 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1012,10 +1012,30 @@ public:
         return true;
     }
 
+    
+    svector<std::pair<theory_var, theory_var>> m_delayed_diseqs;
+
     void new_diseq_eh(theory_var v1, theory_var v2) {
         TRACE(arith, tout << "v" << v1 << " != " << "v" << v2 << "\n";);
+#if 1
+        m_delayed_diseqs.push_back({v1, v2});
+        ctx().push_trail(push_back_vector(m_delayed_diseqs));
+#else
         ++m_stats.m_assert_diseq;
         m_arith_eq_adapter.new_diseq_eh(v1, v2);
+#endif
+    }
+
+    bool check_delayed_diseqs() {
+        bool found_eq = false;
+        for (auto [v1, v2] : m_delayed_diseqs) {
+            if (is_eq(v1, v2)) {
+                found_eq = true;
+                ++m_stats.m_assert_diseq;
+                m_arith_eq_adapter.new_diseq_eh(v1, v2);
+            }
+        }
+        return found_eq;
     }
 
     void apply_sort_cnstr(enode* n, sort*) {
@@ -1666,7 +1686,11 @@ public:
                 TRACE(arith, tout << "check-nra giveup\n";);
                 st = FC_GIVEUP;
                 break;
-            }                        
+            }       
+            
+            if (check_delayed_diseqs())
+                return FC_CONTINUE;
+                        
                         
             if (assume_eqs()) {
                 ++m_stats.m_assume_eqs;