mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-15 03:25:43 +00:00
Code Activity

Fix segfault in horn on formulas with unused quantified variables (#6… (#10091)

Browse source 
…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>
This commit is contained in:
Nikolaj Bjorner 2026-07-11 19:17:18 -07:00 • committed by GitHub
parent dfd2f328f6
commit 14e1dc9896
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 5 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/muz/base/dl_rule.cpp
View file

@ -276,7 +276,11 @@ namespace datalog {
// retrieve free variables.
m_free_vars(q);
vars.append(m_free_vars.size(), m_free_vars.data());
if (vars.contains(static_cast<sort*>(nullptr))) {
// Eliminate gaps in the variable indices produced by unused variables.
// A single substitution pass may not suffice: var_subst applies the rewriter,
// which can simplify away variable occurrences (e.g. collapsing ite terms),
// introducing new gaps. Iterate until the free variables are contiguous.
while (vars.contains(static_cast<sort*>(nullptr))) {
var_subst sub(m, false);
expr_ref_vector args(m);
// [s0, 0, s2, ..]