mirror of
https://github.com/Z3Prover/z3
synced 2026-07-14 19:15:41 +00:00
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>
This commit is contained in:
Copilot
GitHub
parent
d99b6e7b08
commit
4862a10ffd
2 changed files with 144 additions and 5 deletions
|
|
@ -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) {
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
}
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue