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;