From 0790dfd8766a188cf9850394a7e7df38f988c18b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 14 Jul 2026 15:17:53 -0700 Subject: [PATCH] Fix use-after-free in spacer hypothesis_reducer::reduce_core (#10123) reduce_core looped with while (true) and read p = todo.back() with no empty check, exiting only when it reached a hypothesis-free sub-proof of false. When hypothesis reduction cannot close all hypotheses on the root proof, todo drains and todo.back() reads past the end of the vector, producing a heap-use-after-free (SIGSEGV in Fixedpoint.query with spacer.keep_proxy=false). Whether the root closes depends on search order, making the crash nondeterministic / seed-dependent. Bound the loop by todo emptiness, track the reduced root across cache-hit pops, and return it if the loop drains without hitting the false-subproof early return. Verified on the issue #10123 benchmark: the UAF is eliminated across spacer.random_seed 0/3/7/13/42/99, all returning unsat. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 726c4e71-03ff-45f6-8322-5253254e1d7e --- src/muz/spacer/spacer_proof_utils.cpp | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/src/muz/spacer/spacer_proof_utils.cpp b/src/muz/spacer/spacer_proof_utils.cpp index eb4d780c98..929b4b1f63 100644 --- a/src/muz/spacer/spacer_proof_utils.cpp +++ b/src/muz/spacer/spacer_proof_utils.cpp @@ -615,13 +615,14 @@ namespace spacer { ptr_buffer args; bool dirty = false; - while (true) { + while (!todo.empty()) { proof *p, *tmp, *pp; unsigned todo_sz; p = todo.back(); if (m_cache.find(p, tmp)) { todo.pop_back(); + res = tmp; continue; } @@ -703,8 +704,12 @@ namespace spacer { if (!m_open_mark.is_marked(res) && m.has_fact(res) && m.is_false(m.get_fact(res))) return res; } - UNREACHABLE(); - return nullptr; + // The loop above normally returns when it reaches a hypothesis-free + // sub-proof of false (the reduced root). If hypothesis reduction could + // not close all hypotheses on the root, todo drains without hitting + // that early return; return the reduced root instead of reading past + // the end of todo (which is a use-after-free). + return res; } proof* hypothesis_reducer::mk_lemma_core(proof* premise, expr *fact) {