3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-28 03:18:49 +00:00

Remove leaked check-assignment output from debug GCC CMake runs (#9978)

The `Ubuntu build - cmake - debugGcc` job was failing because the solver
could emit an unexpected `check-assignment` line before normal
satisfiability output. This change removes that stray output so debug
GCC runs no longer contaminate expected CLI/results streams.

- **Root cause**
- `src/math/lp/nra_solver.cpp` printed `check-assignment` from
`solver::check_assignment()` via `IF_VERBOSE(0, ...)`.
- Verbosity level `0` made this effectively unconditional in the failing
path, so debug builds could leak internal diagnostics into user-visible
output.

- **Change**
- Remove the `check-assignment` print from the exception path in
`lp::solver::check_assignment()`.
- Preserve all existing control flow and error handling; only the
unintended output side effect is removed.

- **Effect**
  - Debug GCC CMake builds keep their normal `sat`/`unsat` output shape.
- Internal solver diagnostics no longer interfere with output-sensitive
CI checks.

```c++
catch (z3_exception &) {
    statistics &st = m_imp->m_nla_core.lp_settings().stats().m_st;
    m_imp->m_nlsat->collect_statistics(st);
    if (m_imp->m_limit.is_canceled()) {
        return l_undef;
    }
    else {
        throw;
    }
}
```

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This commit is contained in:
Copilot 2026-06-27 11:22:47 -07:00 committed by GitHub
parent 39ea5ce8c0
commit 75981a5d3b
No known key found for this signature in database
GPG key ID: B5690EEEBB952194

View file

@ -969,7 +969,6 @@ lbool solver::check_assignment() {
catch (z3_exception &) {
statistics &st = m_imp->m_nla_core.lp_settings().stats().m_st;
m_imp->m_nlsat->collect_statistics(st);
IF_VERBOSE(0, verbose_stream() << "check-assignment\n");
if (m_imp->m_limit.is_canceled()) {
return l_undef;
}