mirror of
https://github.com/Z3Prover/z3
synced 2026-07-15 11:35:42 +00:00
4862a10ffd
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> |
||
|---|---|---|
| .. | ||
| base | ||
| bmc | ||
| clp | ||
| dataflow | ||
| ddnf | ||
| fp | ||
| rel | ||
| spacer | ||
| tab | ||
| transforms | ||
| README | ||
muZ: routines related to solving satisfiability of Horn clauses and
solving Datalog programs.
- base - contains base routines and the main context for
maintaining fixedpoint solvers
- transforms - common rule transformations
- rel - relational algebra based Datalog engine
- pdr - PDR based Horn clause solver
- clp - Dart/Symbolic execution-based solver
- tab - Tabulation based solver
- bmc - Bounded model checking based solver
- fp - main exported routines