From 472ac6a97a3aa45268cd90aac589a7554f7fe9f0 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Thu, 12 Feb 2026 15:11:13 +0000 Subject: [PATCH 1/4] Initial plan 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 2/4] 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 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); 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 3/4] 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)); } From f39e4625342cdba8feb327f634a1b69d52bf6eec Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Thu, 12 Feb 2026 15:37:28 +0000 Subject: [PATCH 4/4] Add check for empty equality list to prevent asserting false Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/smt/smt_model_finder.cpp | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/src/smt/smt_model_finder.cpp b/src/smt/smt_model_finder.cpp index 72fe8b429..eccc89c0f 100644 --- a/src/smt/smt_model_finder.cpp +++ b/src/smt/smt_model_finder.cpp @@ -2566,11 +2566,14 @@ namespace smt { eqs.push_back(m.mk_eq(sk, val)); } } - expr_ref new_cnstr(m); - new_cnstr = m.mk_or(eqs); - TRACE(model_finder, tout << "assert_restriction:\n" << mk_pp(new_cnstr, m) << "\n";); - aux_ctx->assert_expr(new_cnstr); - asserted_something = true; + // Only assert a constraint if we have at least one valid equality + if (!eqs.empty()) { + expr_ref new_cnstr(m); + new_cnstr = m.mk_or(eqs); + TRACE(model_finder, tout << "assert_restriction:\n" << mk_pp(new_cnstr, m) << "\n";); + aux_ctx->assert_expr(new_cnstr); + asserted_something = true; + } } return asserted_something; }