From 35f6b0869a0a0d0fa033a6855d24b66d4724bf7a Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Tue, 21 Jul 2026 19:48:07 -0700
Subject: [PATCH] parallel solver: suppress bare reason_unknown on stderr at
 default verbosity (#10182)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

`IF_VERBOSE(0, ...)` in the parallel tactic's `l_undef` handler caused
the raw reason string (e.g. `sat.max.conflicts`) to be written
unconditionally to stderr, polluting output for any application
embedding libz3 that hits the conflict-budget give-up path.

## Change

- **`src/solver/parallel_tactical.cpp:2186`** — raise verbosity
threshold from `0` to `1`:

```cpp
// Before: fires at default verbosity, writes bare string to stderr
IF_VERBOSE(0, verbose_stream() << reason << "\n");

// After: only fires under -v:1
IF_VERBOSE(1, verbose_stream() << reason << "\n");
```

The reason string remains fully accessible via `(get-info
:reason-unknown)` and `set_reason_unknown` regardless of verbosity.

---------

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 803f54eb74..4ba1b59d3e 100644
--- a/src/solver/parallel_tactical.cpp
+++ b/src/solver/parallel_tactical.cpp
@@ -2183,7 +2183,7 @@ public:
                 std::string reason = ps.reason_unknown();
                 if (!reason.empty()) {
                     g->set_reason_unknown(reason);
-                    IF_VERBOSE(0, verbose_stream() << reason << "\n");
+                    IF_VERBOSE(1, verbose_stream() << reason << "\n");
                 }
             }
             break;