From 75981a5d3b3c216142cd69b8c4d4e0a15ecf2e72 Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Sat, 27 Jun 2026 11:22:47 -0700
Subject: [PATCH] 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>
---
 src/math/lp/nra_solver.cpp | 1 -
 1 file changed, 1 deletion(-)

diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp
index f722019e1f..f5cc61ba9e 100644
--- a/src/math/lp/nra_solver.cpp
+++ b/src/math/lp/nra_solver.cpp
@@ -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;
         }