mirror of
https://github.com/Z3Prover/z3
synced 2026-03-07 13:54:53 +00:00
5c56e5fb0a
Bug fix: m_axioms and m_axiom_set were not restored on pop_scope, causing axioms from a previous push/pop context to leak into subsequent contexts with the same variable names, producing non-termination in incremental solving (push/check-sat/pop sequences). Fix: track m_axioms_size_at_push on the trail stack and truncate m_axioms + remove corresponding m_axiom_set entries on pop. Optimization: propagate_ground_split directly sets variable values when one side is a pure ground string and all variables have known lengths. Optimization: explicit len(z) = len(head) - len(var) axioms for Skolem terms in var-vs-var splits to help arithmetic termination. Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> |
||
|---|---|---|
| .. | ||
| ackermannization | ||
| api | ||
| ast | ||
| cmd_context | ||
| math | ||
| model | ||
| muz | ||
| nlsat | ||
| opt | ||
| params | ||
| parsers | ||
| qe | ||
| sat | ||
| shell | ||
| smt | ||
| solver | ||
| tactic | ||
| test | ||
| util | ||
| CMakeLists.txt | ||