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] 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; }