From 8d47a9dc610322406dc4ac7828c66aa1fb279a37 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Thu, 12 Feb 2026 15:30:02 +0000
Subject: [PATCH] Fix sort error with nested quantifiers by adding sort check

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/smt/smt_model_finder.cpp | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp
index c90f14429..fe26a7172 100644
--- a/src/smt/smt_model_finder.cpp
+++ b/src/smt/smt_model_finder.cpp
@@ -2559,7 +2559,10 @@ namespace smt {
             ptr_buffer<expr> eqs;
             for (auto const& kv : inv) {
                 expr* val = kv.m_key;
-                eqs.push_back(m.mk_eq(sk, val));
+                // Only create equality if sorts match
+                if (sk->get_sort() == val->get_sort()) {
+                    eqs.push_back(m.mk_eq(sk, val));
+                }
             }
             expr_ref new_cnstr(m);
             new_cnstr = m.mk_or(eqs);