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 Spacer QE numeral handling and add #3845 regression

Browse source
This commit is contained in:
copilot-swe-agent[bot] 2026-07-12 23:48:30 +00:00 • committed by GitHub
parent 5bbf34c738
commit 5cf1543118
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 144 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

10
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));
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) {

139
src/test/api_datalog.cpp
View file

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