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

@@ -615,13 +615,14 @@ namespace spacer {
         ptr_buffer<proof> 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) {