mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-14 19:15:41 +00:00
Code Activity

Fix assertion violation in spacer_qe_project.cpp when model evaluation doesn't produce a numeral

Browse source 
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
This commit is contained in:
copilot-swe-agent[bot] 2026-07-12 01:57:59 +00:00 • committed by GitHub
parent c219bf9703
commit 33d260a9c3
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/muz/spacer/spacer_qe_project.cpp
View file

@ -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";);