From 48f1676f2bb3042bd519e0a336b7ea3efcbe71d8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 23 Jul 2026 10:43:37 -0700 Subject: [PATCH] Fix drain_backtrack to pop trail scopes and compile The drain_backtrack destructor added in d247df72a called m_backtrack.pop(), which does not exist on ptr_vector (breaking the build) and, even as pop_back(), would only drop the work item without popping the backtracking trail scope it owns - reintroducing the trail-scope leak that #10196 fixed. Use backtrack(), which pops the trail scope for in_scope items and then removes the item. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> Copilot-Session: 96a14756-2ffe-4cc3-87e7-49fda1b6113a --- src/ast/euf/ho_matcher.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/euf/ho_matcher.cpp b/src/ast/euf/ho_matcher.cpp index cc063be951..334487bf20 100644 --- a/src/ast/euf/ho_matcher.cpp +++ b/src/ast/euf/ho_matcher.cpp @@ -128,7 +128,7 @@ namespace euf { drain_backtrack(ho_matcher &m) : m(m) {} ~drain_backtrack() { while (!m.m_backtrack.empty()) { - m.m_backtrack.pop(); + m.backtrack(); } } };