From 14e1dc9896949059b6f6722e5087a2c01dd2b200 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 11 Jul 2026 19:17:18 -0700 Subject: [PATCH] =?UTF-8?q?Fix=20segfault=20in=20horn=20on=20formulas=20wi?= =?UTF-8?q?th=20unused=20quantified=20variables=20(#6=E2=80=A6=20(#10091)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit …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> --- src/muz/base/dl_rule.cpp | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp index b23786020c..a8a9d9892a 100644 --- a/src/muz/base/dl_rule.cpp +++ b/src/muz/base/dl_rule.cpp @@ -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(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(nullptr))) { var_subst sub(m, false); expr_ref_vector args(m); // [s0, 0, s2, ..]