3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-23 23:42:33 +00:00

parallel solver: suppress bare reason_unknown on stderr at default verbosity (#10182)

`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>
This commit is contained in:
Copilot 2026-07-21 19:48:07 -07:00 committed by GitHub
parent 479ff3476e
commit 35f6b0869a
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

@ -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;