From 1b39b0e50f1b92a81eac4951a517f22765480bbd Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <5377127+levnach@users.noreply.github.com>
Date: Tue, 14 Jul 2026 17:08:08 -0700
Subject: [PATCH] Fix SIGSEGV in nlsat from incorrect algebraic number
 comparison (#10129)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

## Problem

A QF_NIA benchmark (`From_T2__ex16.t2__p22243_terminationG_0.smt2`, run
with `-T:200 model_validate=true`) crashes with SIGSEGV inside nlsat.

## Root cause

In `algebraic_numbers::manager::imp::compare_core`, the
interval-separation workaround computed the isolating intervals of `a`
and `b` with:

```cpp
if (get_interval(a, la, ua, precision) &&
    get_interval(b, lb, ub, precision)) { ... }
```

`&&` short-circuits: when `a` is **rational**, `get_interval(a, ...)`
finds the exact root and returns `false`, so `get_interval(b, ...)`
never runs and `b`'s bounds `lb`/`ub` stay **0**. Those bounds are used
*unconditionally* below the `if` (in the `compare(cell_a, u_b)` /
`compare(cell_b, l_a)` checks), so `a` was effectively compared against
`0`, producing an incorrect and self-inconsistent sign (`compare`
returned `+1` while `<`, `=`, `>` were all false).

Concretely, comparing `c = 39017/131072` (rational) with `d ≈
0.297676176` (root of a quadratic) returned `c > d`, though `c < d`.
Downstream, this made nlsat's `interval_set::is_full` miss full coverage
of ℝ, so `pick_in_complement` was invoked on an empty complement and
read `s->m_intervals[UINT_MAX]` — a crash guarded only by a
release-stripped `SASSERT` (`nlsat_interval_set.cpp`).

## Fix

Compute both intervals unconditionally so `b`'s bounds are always valid
before they are used.

## Validation

- The crashing benchmark now returns `unsat` (verified on both macOS and
a Linux `RelWithDebInfo` build where the SIGSEGV was originally
reproduced under gdb).
- Unit tests pass: `algebraic`, `upolynomial`, `polynomial`, `nlsat`.

---------

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 src/math/polynomial/algebraic_numbers.cpp | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/src/math/polynomial/algebraic_numbers.cpp b/src/math/polynomial/algebraic_numbers.cpp
index 945b9023dc..47c4b66983 100644
--- a/src/math/polynomial/algebraic_numbers.cpp
+++ b/src/math/polynomial/algebraic_numbers.cpp
@@ -2066,8 +2066,15 @@ namespace algebraic_numbers {
             scoped_mpbq la(bqm()), ua(bqm());
             scoped_mpbq lb(bqm()), ub(bqm());
             unsigned precision = 10;
-            if (get_interval(a, la, ua, precision) && 
-                get_interval(b, lb, ub, precision)) { 
+            // Important: both intervals must be computed. Do not short-circuit with &&:
+            // the refined bounds la, ua, lb, ub are all used below (and beyond this
+            // if statement, in the interval-separation checks that compare against
+            // the bounds of a and b), so get_interval(b, ...) has to run even when
+            // get_interval(a, ...) returns false (which happens when a is rational
+            // and its exact root is found).
+            bool a_separated = get_interval(a, la, ua, precision);
+            bool b_separated = get_interval(b, lb, ub, precision);
+            if (a_separated && b_separated) {
                 IF_VERBOSE(9, verbose_stream() << "sturm 0\n");
                 if (la > ub) 
                     return sign_pos;