From 33d260a9c3ff5284c84f2850fc170a40fa985c52 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sun, 12 Jul 2026 01:57:59 +0000 Subject: [PATCH] Fix assertion violation in spacer_qe_project.cpp when model evaluation doesn't produce a numeral Replaces VERIFY(a.is_numeral(val, r)) with graceful return false in both arith_project_util::project() overloads. Previously, when the legacy non-native MBP (fp.spacer.native_mbp false) evaluated c*x+t in the model and the result was not a numeral, the code would crash. Fixes #4121 --- src/muz/spacer/spacer_qe_project.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/muz/spacer/spacer_qe_project.cpp b/src/muz/spacer/spacer_qe_project.cpp index 58499c028e..a24395792d 100644 --- a/src/muz/spacer/spacer_qe_project.cpp +++ b/src/muz/spacer/spacer_qe_project.cpp @@ -367,7 +367,7 @@ class arith_project_util { cx = mk_mul(c, m_var->x()); cxt = mk_add(cx, t); val = mdl(cxt); - VERIFY(a.is_numeral(val, r)); + if (!a.is_numeral(val, r)) return false; SASSERT(r > rational::zero() || r < rational::zero()); if (r > rational::zero()) { c = -c; @@ -473,7 +473,7 @@ class arith_project_util { cx = mk_mul(c, m_var->x()); cxt = mk_add(cx, t); val = mdl(cxt); - VERIFY(a.is_numeral(val, r)); + if (!a.is_numeral(val, r)) return false; if (is_eq) { TRACE(qe, tout << "equality term\n";);