Parallel solver writes the bare reason_unknown string to stderr at verbosity 0 (parallel_tactical.cpp:2186)

[ChaiTRex]

Version: Z3 5.0.0 (official release binary, macOS arm64 / Apple M1; also reproduced through the Rust z3 crate binding the same libz3). Still present on master as of commit 1f306e1 (2026-07-18): src/solver/parallel_tactical.cpp there is byte-identical to the z3-5.0.0 tag, so the cited line numbers apply to master too.

In Z3 5.0.0, when the parallel solver returns l_undef with a nonempty worker reason, this handler writes the bare reason string to the default verbose stream (stderr) at verbosity 0, with no prefix — applications embedding libz3 get stray sat.max.conflicts lines interleaved into their own stderr during normal operation. (Not every parallel unknown routes through this handler — e.g. rlimit=1 returns unknown with a nonempty reason and no stderr output — but the common conflict-budget give-up does.)

Repro

; repro.smt2 — UNSAT (2^64 - 59 is prime), multiplier-hard
(set-logic QF_BV)
(declare-const x (_ BitVec 64))
(declare-const y (_ BitVec 64))
(assert (= (bvmul ((_ zero_extend 64) x) ((_ zero_extend 64) y))
           (_ bv18446744073709551557 128)))
(assert (bvult (_ bv1 64) x))
(assert (bvult (_ bv1 64) y))
(assert (bvule x y))
(check-sat)
(get-info :reason-unknown)

$ z3 --version
Z3 version 5.0.0 - 64 bit
$ z3 parallel.enable=true parallel.threads.max=2 repro.smt2 >stdout.txt 2>stderr.txt
$ cat stdout.txt
unknown
(:reason-unknown "sat.max.conflicts")
$ cat stderr.txt
sat.max.conflicts

(~0.6 s with parallel.threads.max=2; also reproduces without that setting, ~1.4 s on
8 threads.)

Cause

src/solver/parallel_tactical.cpp line 2186 (tag z3-5.0.0), in the tactic's l_undef
result handling:

std::string reason = ps.reason_unknown();
if (!reason.empty()) {
    g->set_reason_unknown(reason);
    IF_VERBOSE(0, verbose_stream() << reason << "\n");
}

IF_VERBOSE(0, ...) fires at the default verbosity level, and verbose_stream() is stderr. For comparison, 4.16.0's parallel tactic printed only give-up-class reasons ((incomplete…, (sat.giveup…) at level 0; 5.0.0 prints every nonempty l_undef reason through this handler, including routine conflict-budget give-ups, and every other diagnostic in the file is level ≥ 1 or carries a prefix.

Fix (verified locally)

Raising the level to IF_VERBOSE(1, ...) and rebuilding (macOS arm64, clang 21): the same repro now returns unknown with zero stderr output at default verbosity — the reason remains available via (get-info :reason-unknown) and via set_reason_unknown — and the line still appears under -v:1. Nothing is lost at level 0.

Related: the unknown itself is premature — filed separately as a reason-string mismatch that skips the cube-budget escalation (see #10161).

Acknowledgements

I received help with the minimization, diagnosis, and write-up from the AI models Fable 5 and Sol 5.6.