mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-22 16:40:29 +00:00
Code Activity

a couple more bugfixes about leases

Browse source
This commit is contained in:
Ilana Shapiro 2026-06-21 17:43:17 -07:00
parent e45683de4b
commit 5abf942c75
2 changed files with 32 additions and 18 deletions
Download patch file Download diff file Expand all files Collapse all files

25
src/smt/smt_parallel.cpp
View file

@ -1409,14 +1409,21 @@ namespace smt {
SASSERT(lease != nullptr || targets != nullptr);
bool did_backtrack = false;
if (lease && !m_search_tree.is_lease_canceled(lease->leased_node)) {
// we close/backtrack regardless of whether this lease is stale or not, as long as the lease isn't canceled
// i.e. worker 1 splits this node, but then worker 2 determines UNSAT --> worker 2 is stale but we still close this node and backtrack
did_backtrack = true;
IF_VERBOSE(1, verbose_stream() << "Batch manager backtracking.\n");
node* leased_node = lease->leased_node;
release_worker_lease_unlocked(worker_id, *lease);
m_search_tree.backtrack(leased_node, g_core);
if (lease) {
if (!m_search_tree.is_lease_canceled(lease->leased_node)) {
// we close/backtrack regardless of whether this lease is stale or not, as long as the lease isn't canceled
// i.e. worker 1 splits this node, but then worker 2 determines UNSAT --> worker 2 is stale but we still close this node and backtrack
did_backtrack = true;
IF_VERBOSE(1, verbose_stream() << "Batch manager backtracking.\n");
node* leased_node = lease->leased_node;
release_worker_lease_unlocked(worker_id, *lease);
m_search_tree.backtrack(leased_node, g_core);
}
else {
// the lease was canceled by another worker. don't backtrack on this node with whatever new core we just found with this thread
// however, we do proceed to external targets, since the new code may have exposed new external targets we can close/backtrack
attempt_release_canceled_lease_unlocked(worker_id, *lease);
}
}
if (targets) {
for (auto const& target : *targets) {
@ -1461,6 +1468,8 @@ namespace smt {
lit = l2g(atom);
nlit = mk_not(m, lit);
node* leased_node = lease.leased_node;
VERIFY(!leased_node->path_contains_atom(lit));
VERIFY(!leased_node->path_contains_atom(nlit));
bool did_split = m_search_tree.try_split(leased_node, lit, nlit, effort);
release_worker_lease_unlocked(worker_id, lease);

25
src/solver/parallel_tactical2.cpp
View file

@ -424,16 +424,21 @@ class parallel_solver {
SASSERT(lease != nullptr || targets != nullptr);
bool did_backtrack = false;
if (lease && !m_search_tree.is_lease_canceled(lease->leased_node)) {
// we close/backtrack regardless of whether this lease is stale or not, as long as the lease isn't canceled
// i.e. worker 1 splits this node, but then worker 2 determines UNSAT --> worker 2 is stale but we still close this node and backtrack
auto* leased_node = lease->leased_node;
did_backtrack = true;
release_worker_lease_unlocked(worker_id, *lease);
m_search_tree.backtrack(leased_node, g_core);
}
else if (lease) {
attempt_release_canceled_lease_unlocked(worker_id, *lease);
if (lease) {
if (!m_search_tree.is_lease_canceled(lease->leased_node)) {
// we close/backtrack regardless of whether this lease is stale or not, as long as the lease isn't canceled
// i.e. worker 1 splits this node, but then worker 2 determines UNSAT --> worker 2 is stale but we still close this node and backtrack
did_backtrack = true;
IF_VERBOSE(1, verbose_stream() << "Batch manager backtracking.\n");
auto* leased_node = lease->leased_node;
release_worker_lease_unlocked(worker_id, *lease);
m_search_tree.backtrack(leased_node, g_core);
}
else {
// the lease was canceled by another worker. don't backtrack on this node with the new, arbitrary core we just found with this thread
// however, we do proceed to external targets, since the new code may have exposed new external targets we can close/backtrack
attempt_release_canceled_lease_unlocked(worker_id, *lease);
}
}
if (targets) {
for (auto const& target : *targets) {