3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-26 17:02:38 +00:00

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
This commit is contained in:
Nikolaj Bjorner 2026-07-23 10:43:37 -07:00
parent 44c221b690
commit 48f1676f2b

View file

@ -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();
}
}
};