From c9d3dc959df640d3f5a79f4dbe4117134945e4b0 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 23 Jul 2026 10:05:28 -0700
Subject: [PATCH] Fix trail-scope leak in ho_matcher on early exit (#10196)

The higher-order matcher shares the solver's trail stack. On early-exit
paths (resource/rlimit reached via m.inc(), or search budget exhausted)
work items were left on m_backtrack with their pushed scopes never popped,
leaking a trail scope. This desynchronized the trail scope count from the
solver scope level and later tripped SASSERT(ilvl <= m_scope_lvl) /
unsound backtracking in smt::context::reinit_clauses.

Restore the trail before exit on every path using an RAII guard
(scoped_trail_level) and drain the backtrack stack after the main search
loop so m_backtrack is left empty for the next call. This avoids wrapping
large blocks in try/catch (which would mask underlying bugs such as
creating non-well-sorted expressions) while still guaranteeing the trail
is restored on both normal and exceptional exits. The sort-mismatch check
and UNREACHABLE() in refine_ho_match are preserved so ill-sorted terms
remain surfaced rather than silently discarded.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
Copilot-Session: 96a14756-2ffe-4cc3-87e7-49fda1b6113a
---
 src/ast/euf/ho_matcher.cpp | 36 +++++++++++++++++++++++++++++-------
 1 file changed, 29 insertions(+), 7 deletions(-)

diff --git a/src/ast/euf/ho_matcher.cpp b/src/ast/euf/ho_matcher.cpp
index c85914e8f1..e2e2160c6e 100644
--- a/src/ast/euf/ho_matcher.cpp
+++ b/src/ast/euf/ho_matcher.cpp
@@ -49,6 +49,22 @@ Author:
 
 namespace euf {
 
+    // RAII guard that restores the shared trail stack to the scope level
+    // captured at construction. The matcher shares the solver's trail stack, so
+    // leaking a scope on an early or exceptional exit desynchronizes the trail
+    // scope count from the solver scope level and later trips an assertion /
+    // unsound backtracking in smt::context::reinit_clauses. Using a guard
+    // restores the trail before exit on every path without wrapping large blocks
+    // of code in exception handlers that would mask underlying bugs.
+    namespace {
+        struct scoped_trail_level {
+            trail_stack& m_trail;
+            unsigned     m_base;
+            scoped_trail_level(trail_stack& t) : m_trail(t), m_base(t.get_num_scopes()) {}
+            ~scoped_trail_level() { m_trail.pop_scope(m_trail.get_num_scopes() - m_base); }
+        };
+    }
+
     expr_ref_vector const &ho_subst::get_binding(quantifier *q) {
         ast_manager &m = m_subst.get_manager();
         m_binding.reset();
@@ -102,13 +118,13 @@ namespace euf {
     }
 
     void ho_matcher::operator()(expr* pat, expr* t, unsigned num_bound, unsigned num_vars) {               
+        scoped_trail_level _restore(m_trail);
         m_trail.push_scope();
         m_subst.resize(0);
         m_subst.resize(num_vars);
         m_goals.reset();
         m_goals.push(0, num_bound, pat, t); 
         search();
-        m_trail.pop_scope(1);
     }
 
     void ho_matcher::search() {
@@ -119,8 +135,6 @@ namespace euf {
         while (m.inc()) {
             if (budget-- == 0) {
                 IF_VERBOSE(2, verbose_stream() << "ho_matcher: search budget exhausted\n");
-                while (!m_backtrack.empty())
-                    backtrack();
                 break;
             }
             // Q, B -> Q', B'. Push work on the backtrack stack and new work items
@@ -133,6 +147,17 @@ namespace euf {
                 break;
         }
 
+        // Drain any remaining work items so that every backtracking scope pushed
+        // in consume_work is popped again and m_backtrack is left empty for the
+        // next call. The loop above can exit early - budget exhausted, or
+        // m.inc() reporting that the resource limit has been reached - with items
+        // still on the backtrack stack. Because the matcher shares the solver's
+        // trail stack, leaking a scope here would desynchronize the trail scope
+        // count from the solver scope level and later trigger an assertion
+        // failure / unsound backtracking in smt::context::reinit_clauses.
+        while (!m_backtrack.empty())
+            backtrack();
+
         IF_VERBOSE(10, display(verbose_stream() << "ho_matcher: done\n"));
     }
 
@@ -947,7 +972,7 @@ namespace euf {
                    auto& abs = m_pat2abs[fo_pat];
                    verbose_stream() << "  m_pat2abs size: " << abs.size() << "\n";
                    for (auto [v, pat] : abs) verbose_stream() << "    v=" << v << " pat=" << mk_pp(pat, m) << "\n";);
-        unsigned base_scope = m_trail.get_num_scopes();
+        scoped_trail_level _restore(m_trail);
         m_trail.push_scope();
         m_subst.resize(0);
         m_subst.resize(s.size());
@@ -974,7 +999,6 @@ namespace euf {
             // higher-order pattern. Discard this refinement candidate (produce
             // no instance) instead of aborting the whole solve.
             if (!subst_sorts_match(m, pat, s, true)) {
-                m_trail.pop_scope(1);
                 IF_VERBOSE(0, verbose_stream() << "refine_ho_match: sorts do not match for " << mk_pp(pat, m) << " and "
                                                << s << "\n";);
                 UNREACHABLE();
@@ -988,8 +1012,6 @@ namespace euf {
             m_goals.push(level, num_bound, pat_refined, m_subst.get(v));
         }
         search();
-        
-        m_trail.pop_scope(1);
     }
 
     bool ho_matcher::subst_sorts_match(ast_manager& m, expr* t, expr_ref_vector const& s, bool std_order) {