From c798213d87ece10718582d8adba6fbb7fc179f2f Mon Sep 17 00:00:00 2001 From: Ilana Shapiro Date: Sat, 20 Jun 2026 22:08:58 -0700 Subject: [PATCH] restore invalid atom case: Path atoms now get rejected in the retry loop and removed from the candidate pool, same as global backbone/negation rejections. --- src/solver/parallel_tactical2.cpp | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/solver/parallel_tactical2.cpp b/src/solver/parallel_tactical2.cpp index 4e96594cf..15a9282a3 100644 --- a/src/solver/parallel_tactical2.cpp +++ b/src/solver/parallel_tactical2.cpp @@ -708,7 +708,7 @@ class parallel_solver { if (m_search_tree.is_lease_canceled(lease.leased_node)) return false; - expr_ref _atom(l2g(atom), m); + expr_ref _atom(l2g(atom), m); return lease.leased_node->path_contains_atom(_atom); } @@ -1117,6 +1117,13 @@ class parallel_solver { continue; if (m.is_true(lit) || m.is_false(lit)) continue; + if (b.path_contains_atom(m_l2g, lease, lit)) { + expr* atom = lit; + m.is_not(lit, atom); + rejected_atoms.insert(atom); + rejected = true; + continue; + } if (m_config.m_global_backbones && b.is_global_backbone_or_negation(m_l2g, lit)) { expr* atom = lit; m.is_not(lit, atom);