From 2193e04f6750bc41895b4c5a9df11f2af399807f Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Thu, 12 Feb 2026 15:35:49 +0000 Subject: [PATCH] Improve comment explaining sort check fix Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/smt/smt_model_finder.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index fe26a7172..72fe8b429 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -2559,7 +2559,9 @@ namespace smt { ptr_buffer eqs; for (auto const& kv : inv) { expr* val = kv.m_key; - // Only create equality if sorts match + // When quantifiers are flattened, the instantiation set may contain + // values from nested quantifiers with incompatible sorts. Only create + // equality constraints when sorts match to avoid well-sortedness violations. if (sk->get_sort() == val->get_sort()) { eqs.push_back(m.mk_eq(sk, val)); }