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

drain backtrack trail using scoped guarantees

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-07-23 10:19:20 -07:00
parent c9d3dc959d
commit d247df72a2
1 changed files with 11 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

29
src/ast/euf/ho_matcher.cpp
View file

@ -49,13 +49,6 @@ Author:
namespace euf { 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 { namespace {
struct scoped_trail_level { struct scoped_trail_level {
trail_stack& m_trail; trail_stack& m_trail;
@ -130,6 +123,17 @@ namespace euf {
void ho_matcher::search() { void ho_matcher::search() {
IF_VERBOSE(10, display(verbose_stream())); IF_VERBOSE(10, display(verbose_stream()));
struct drain_backtrack {
ho_matcher &m;
drain_backtrack(ho_matcher &m) : m(m) {}
~drain_backtrack() {
while (!m.m_backtrack.empty()) {
m.m_backtrack.pop();
}
}
};
drain_backtrack _drain(*this);
unsigned budget = m_max_iterations; unsigned budget = m_max_iterations;
while (m.inc()) { while (m.inc()) {
@ -147,17 +151,6 @@ namespace euf {
break; 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")); IF_VERBOSE(10, display(verbose_stream() << "ho_matcher: done\n"));
} }