mirror of
https://github.com/Z3Prover/z3
synced 2026-07-17 20:45:45 +00:00
14e1dc9896
…158) rule_manager::mk_query eliminates gaps in de Bruijn indices caused by unused quantified variables via a substitution that renumbers the remaining variables contiguously. This was done in a single pass, but var_subst applies the rewriter, which can simplify away further variable occurrences (e.g. collapsing ite terms such as (ite true a b) or (ite c x x)), introducing new gaps. The leftover null sort was then dereferenced, asserting in debug and segfaulting in release. Iterate the gap-elimination until the free variables are contiguous. Each iteration either compacts the indices or strictly reduces the set of used variables, so it terminates. Fixes the crash reported for: (assert (forall ((a Bool)(b Bool)(d (_ BitVec 1))(e (_ BitVec 1))(f (_ BitVec 1))(g Bool)) (= (= f (ite a (_ bv0 1) (ite true (_ bv0 1) (ite b e e)))) g))) (check-sat-using horn) Co-authored-by: Copilot <223556219+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