From 4862a10ffd942e7f0c99ac639701a3329e73cca5 Mon Sep 17 00:00:00 2001 From: Copilot <198982749+Copilot@users.noreply.github.com> Date: Sun, 12 Jul 2026 18:52:44 -0700 Subject: [PATCH] Spacer QE: avoid assertion on extended arithmetic model values and add #3845 regression (#10096) Spacer crashed in quantifier-elimination projection on certain HORN inputs when model evaluation produced arithmetic expressions that were not plain numerals. The failure was an assertion in `spacer_qe_project.cpp` during sign/offset computation for projected literals. - **Projection robustness in Spacer arithmetic QE** - Updated numeral extraction in `src/muz/spacer/spacer_qe_project.cpp` from `is_numeral` to `is_extended_numeral` at all model-evaluation sites used by projection. - This covers evaluated arithmetic forms (e.g., normalized arithmetic expressions) that are semantically numeric but not syntactic numerals, preventing assertion failures in disequality/equality handling and bound selection. - **Regression coverage for the crashing HORN shape** - Added a focused regression in `src/test/api_datalog.cpp` that evaluates the reported Spacer/HORN input pattern through `Z3_eval_smtlib2_string`. - The test exercises the exact QE/projection path that previously triggered the assertion. ```cpp // Before VERIFY(a.is_numeral(val, r)); // After VERIFY(a.is_extended_numeral(val, r)); ``` --------- Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com> --- src/muz/spacer/spacer_qe_project.cpp | 10 +- src/test/api_datalog.cpp | 139 +++++++++++++++++++++++++++ 2 files changed, 144 insertions(+), 5 deletions(-) diff --git a/src/muz/spacer/spacer_qe_project.cpp b/src/muz/spacer/spacer_qe_project.cpp index 58499c028e..70db71bdbd 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)); + VERIFY(a.is_extended_numeral(val, r)); 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)); + VERIFY(a.is_extended_numeral(val, r)); if (is_eq) { TRACE(qe, tout << "equality term\n";); @@ -711,7 +711,7 @@ class arith_project_util { cx = mk_mul(m_coeffs[max_t], m_var->x()); cxt = mk_add(cx, m_terms.get(max_t)); val = mdl(cxt); - VERIFY(a.is_numeral(val, r)); + VERIFY(a.is_extended_numeral(val, r)); // get the offset from the smallest/largest possible value for x // literal smallest/largest val of x @@ -771,13 +771,13 @@ class arith_project_util { // evaluate x in mdl rational r_x; val = mdl(m_var->x()); - VERIFY(a.is_numeral(val, r_x)); + VERIFY(a.is_extended_numeral(val, r_x)); for (unsigned i = 0; i < m_terms.size(); ++i) { rational const &ac = m_coeffs[i]; if (!m_eq[i] && ac.is_pos() == do_pos) { val = mdl(m_terms.get(i)); - VERIFY(a.is_numeral(val, r)); + VERIFY(a.is_extended_numeral(val, r)); r /= abs(ac); // skip the literal if false in the model if (do_pos) { diff --git a/src/test/api_datalog.cpp b/src/test/api_datalog.cpp index 6e88a8aded..3b0011a4b3 100644 --- a/src/test/api_datalog.cpp +++ b/src/test/api_datalog.cpp @@ -90,5 +90,144 @@ void tst_api_datalog() { ENSURE(Z3_get_error_code(ctx) == Z3_OK); } + // Regression test for assertion violation in Spacer QE projection (#3845) + { + char const* chc = R"( +(set-logic HORN) +(set-option :fp.xform.inline_eager false) +(set-option :fp.spacer.native_mbp false) +(set-option :fp.spacer.reach_dnf false) +(declare-fun a (Int Bool Int Bool) Bool) +(declare-fun c (Int Int Bool Bool Int Int Int Int Bool Bool Bool Int Int Bool Bool Int Int Int Int Bool Bool Bool) Bool) +(declare-fun d (Bool Bool Bool Int Bool Int Int Bool Bool Int Int Int Int Bool Bool Bool Int Int Bool Bool Int Int Int Int Bool Bool Bool) Bool) +(declare-fun e (Int Int Bool Bool Int Int Int Int Bool Bool Bool Bool) Bool) +(assert (forall ((ef Int) (eaa Int) (eabacad Bool) (eabacg Bool)) (=> eabacad (a eaa eabacg ef eabacad)))) +(assert + (forall ((no Int) + (naf Int) + (nphl Bool) + (nphiacg Bool) + (nphq Bool) + (nphiacad Bool) + (nrsag Int) + (nrsah Int) + (nrst Int) + (nrsai Int) + (nrsuacg Bool) + (nrsv Int) + (nrsw Int) + (nrsx Int) + (nrsaj Int) + (nrsuacad Bool) + (nyacad Bool) + (nzeaa Int) + (nzeabacg Bool) + (nzef Int) + (nzeabacad Bool) + (nyacg Bool)) + (=> (a nzeaa nzeabacg nzef nzeabacad) + (c naf nzeaa nzeabacg nyacg nrsag nrsah nrst nrsai nrsuacg nphl nphiacg no nzef + nzeabacad nyacad nrsv nrsw nrsx nrsaj nrsuacad nphq nphiacad)))) +(assert + (forall ((nak Bool) + (nal Bool) + (nam Bool) + (nphl Bool) + (nphiacg Bool) + (ninit_invalid_s Int) + (nao Bool) + (nphae Bool) + (nphiacj Bool) + (nrsag Int) + (nrsah Int) + (nrst Int) + (nrsai Int) + (nrsuacg Bool) + (nap Int) + (nrsaq Int) + (nrsar Int) + (nrsas Int) + (nrs__synapse_5_x Int) + (nrsuacj Bool) + (nyacg Bool) + (nyacj Bool) + (naf Int) + (nat Int) + (nzeaa Int) + (nzeabacg Bool) + (nau Int) + (nzeav Int) + (nzeabacj Bool) + (naw Bool)) + (let ((ax (=> nao (< nap 0 nau)))) + (let ((ay (= naw ax))) + (=> ay (d nak nal nam ninit_invalid_s naw naf nzeaa nzeabacg nyacg nrsag nrsah nrst nrsai + nrsuacg nphl nphiacg nat nzeav nzeabacj nyacj nrsaq nrsar nrsas nrs__synapse_5_x nrsuacj nphae nphiacj)))))) +(assert + (forall ((naf Int) + (nzeaa Int) + (nzeabacg Bool) + (nyacg Bool) + (nrsag Int) + (nrsah Int) + (nrst Int) + (nrsai Int) + (nrsuacg Bool) + (nphl Bool) + (nphiacg Bool) + (no Int) + (nzef Int) + (nzeabacad Bool) + (nyacad Bool) + (nrsv Int) + (nrsw Int) + (nrsx Int) + (nrsaj Int) + (nrsuacad Bool) + (nphq Bool) + (nphiacad Bool) + (nak Bool) + (nal Bool) + (nam Bool) + (ninit_invalid_s Int) + (naw Bool) + (nat Int) + (nzeav Int) + (nzeabacj Bool) + (nyacj Bool) + (nrsaq Int) + (nrsar Int) + (nrsas Int) + (nrs__synapse_5_x Int) + (nrsuacj Bool) + (nphae Bool) + (nphiacj Bool)) + (=> (c naf nzeaa nzeabacg nyacg nrsag nrsah nrst nrsai nrsuacg nphl nphiacg no nzef nzeabacad + nyacad nrsv nrsw nrsx nrsaj nrsuacad nphq nphiacad) + (d nak nal nam ninit_invalid_s naw no nzef nzeabacad nyacad nrsv nrsw nrsx nrsaj nrsuacad nphq + nphiacad nat nzeav nzeabacj nyacj nrsaq nrsar nrsas nrs__synapse_5_x nrsuacj nphae nphiacj) + (e nat nzeav nzeabacj nyacj nrsaq nrsar nrsas nrs__synapse_5_x nrsuacj nphae nphiacj naw)))) +(assert + (forall ((naw Bool) + (nat Int) + (nzeav Int) + (nzeabacj Bool) + (nyacj Bool) + (nrsaq Int) + (nrsar Int) + (nrsas Int) + (nrs__synapse_5_x Int) + (nrsuacj Bool) + (nphae Bool) + (nphiacj Bool)) + (not (e nat nzeav nzeabacj nyacj nrsaq nrsar nrsas nrs__synapse_5_x nrsuacj nphae nphiacj naw)))) +(check-sat) +)"; + + Z3_string response = Z3_eval_smtlib2_string(ctx, chc); + ENSURE(response != nullptr); + ENSURE(Z3_get_error_code(ctx) == Z3_OK); + } + Z3_del_context(ctx); }