From 528efbb535c997e8febdadb4e7d74ba47bdc8633 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 16 Feb 2025 13:41:17 -0800
Subject: [PATCH] fixes to failure conditions for unification

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/qe/mbp/mbp_euf.cpp | 19 +++++++++++++------
 1 file changed, 13 insertions(+), 6 deletions(-)

diff --git a/src/qe/mbp/mbp_euf.cpp b/src/qe/mbp/mbp_euf.cpp
index 9c54e11f6..1c85e9e21 100644
--- a/src/qe/mbp/mbp_euf.cpp
+++ b/src/qe/mbp/mbp_euf.cpp
@@ -214,7 +214,8 @@ namespace mbp {
                 expr* x = a->get_arg(i);
                 expr* y = b->get_arg(i);
                 todo.push_back({x, y});
-            }            
+            }
+            bool failed = false;
             while (!todo.empty()) {
                 auto [x, y] = todo.back();
                 todo.pop_back();
@@ -223,8 +224,10 @@ namespace mbp {
                 SASSERT(ry);
                 if (rx == ry) 
                     continue;
-                if (rx)
-                    break; // fail
+                if (rx) {
+                    failed = true;
+                    break;
+                }
                 if (m_parents[x].size() > 1)
                     // a crude safey hatch to preserve models
                     // we could require that every parent of x
@@ -233,16 +236,20 @@ namespace mbp {
                     break;
                 expr* s = nullptr;
                 if (soln.find(x, s)) {
-                    if (s != ry)
+                    if (s != ry) {
+                        failed = true;
                         break;
+                    }
                     continue;
                 }
                 if (is_var(x)) {
                     soln.insert(x, ry);
                     continue;
                 }
-                if (!same_decl(x, y))
+                if (!same_decl(x, y)) {
+                    failed = true;
                     break;
+                }
                 app* ax = to_app(x);
                 app* ay = to_app(y);
                 for (unsigned i = 0; i < ax->get_num_args(); ++i) 
@@ -257,7 +264,7 @@ namespace mbp {
                   );
 
 
-            if (todo.empty() && !soln.empty()) {
+            if (!failed && todo.empty() && !soln.empty()) {
                 for (auto [key, value] : soln) {
                     vars.erase(to_app(key));
                     defs.push_back( { expr_ref(key, m), expr_ref(value, m) });