From ae190b8b8880bb29f9cad777abcb55e9ef287a72 Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Tue, 21 Jul 2026 19:48:55 -0700
Subject: [PATCH] fix: parallel mode exits unknown immediately for QF_BV due to
 reason-string mismatch (#10183)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Under `parallel.enable=true`, QF_BV workers that exhaust their per-cube
conflict budget (1000) are misclassified as unrecoverably incomplete,
causing the portfolio to return `unknown` in ~1 second instead of
escalating the budget and continuing.

## Root cause

`parallel_tactical.cpp` only recognizes `"max-conflicts-reached"` (the
`smt::context` spelling) as a signal to escalate the conflict budget.
SAT-core-backed solvers — which QF_BV workers use — report the same
condition as `"sat.max.conflicts"` (from
`sat_solver::reached_max_conflicts()`). The mismatch causes every QF_BV
cube attempt to fall through to `b.set_unknown()` instead of
`update_max_thread_conflicts()`.

## Fix

```diff
- if (reason != "max-conflicts-reached") {
+ if (reason != "max-conflicts-reached" && reason != "sat.max.conflicts") {
```

Both spellings now correctly route to the budget-escalation path. The
parallel `smt_parallel.cpp` path is unaffected — it owns `smt::context`
workers, which can only produce `"max-conflicts-reached"`.

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
---
 src/solver/parallel_tactical.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/solver/parallel_tactical.cpp b/src/solver/parallel_tactical.cpp
index 4ba1b59d3e..753cd15496 100644
--- a/src/solver/parallel_tactical.cpp
+++ b/src/solver/parallel_tactical.cpp
@@ -1250,7 +1250,7 @@ class parallel_solver {
                     // re-checking the same cube would spin forever. Record a sound
                     // 'unknown' verdict and stop working this branch instead.
                     std::string reason = s->reason_unknown();
-                    if (reason != "max-conflicts-reached") {
+                    if (reason != "max-conflicts-reached" && reason != "sat.max.conflicts") {
                         LOG_WORKER(1, " undef cube is not conflict-limited (" << reason << "); reporting unknown\n");
                         b.set_unknown(reason);
                         return;