Fix nra_solver regression: unknown instead of sat for satisfiable NL arithmetic problems

[Copilot]

Commit 7395152 introduced a performance regression in the NRA (nonlinear real arithmetic) solver path: satisfiable problems with nonlinear constraints started returning unknown instead of sat.

Root Cause

check() was changed to use setup_solver_poly(), which performs polynomial elaboration — substituting monic/term variable definitions directly into constraints. For example, given monic v = x1 * x2, a linear constraint v >= 5 becomes the nonlinear atom x1*x2 - 5 >= 0. This silently promotes many linear constraints into nonlinear polynomial ones, making the underlying nlsat solver work substantially harder and causing it to time out.

Fix

Revert check() to call setup_solver_terms() instead of setup_solver_poly(). Both produce a logically equivalent nlsat problem, but setup_solver_terms() preserves linearity where possible by encoding monic and term definitions as separate equality clauses rather than substituting them in:

• Linear constraint on monic var: v - 5 >= 0 (linear atom)
• Monic definition: x1*x2 - v = 0 (nonlinear, but isolated)

setup_solver_poly() remains in the codebase but is no longer called from the main check() path.

Original prompt

---

This section details on the original issue you should resolve

<issue_title>Z3 Regression: solver.check() returns 'unknown' instead of 'sat'</issue_title>
<issue_description>Z3-solver versions 4.15.8+ return unknown instead of sat for the attached satisfiable constraint problem. Versions 4.13.0-4.15.4 correctly return sat with 700+ solutions.

Reproduction

# Working version
pip install z3-solver==4.15.4.0
z3 group_conv_constraint_set_0.smt2
# Output: sat

# Broken version
pip install z3-solver==4.16.0.0
z3 group_conv_constraint_set_0.smt2
# Output: unknown

Satisfying Assignment (from z3 4.15.4)

intrinsic_k = 16
intrinsic_mn = 16
k0 = 3
m0 = 2
m1 = 8
m2 = 32
n0 = 16
sg_m_cnt = 8
sg_n_cnt = 1
subgroup_m0 = 2
subgroup_m1 = 1
subgroup_m2 = 2
subgroup_n0 = 1
subgroup_size = 64
wg_x = 512
wg_y = 1
wg_z = 1

Verification: cvc5 v1.3.2 also returns sat on the exact same SMT2 file, confirming this is a genuine z3 regression.

Version Info

• Working: 4.13.0, 4.14.0, 4.15.0, 4.15.4
• Broken: 4.15.8, 4.16.0

SMT2 Problem

; benchmark generated from python API
(set-info :status unknown)
(declare-fun intrinsic_k () Int)
(declare-fun intrinsic_mn () Int)
(declare-fun n0 () Int)
(declare-fun k0 () Int)
(declare-fun m2 () Int)
(declare-fun m1 () Int)
(declare-fun m0 () Int)
(declare-fun subgroup_size () Int)
(declare-fun sg_n_cnt () Int)
(declare-fun sg_m_cnt () Int)
(declare-fun wg_x () Int)
(declare-fun subgroup_n0 () Int)
(declare-fun subgroup_m2 () Int)
(declare-fun subgroup_m1 () Int)
(declare-fun subgroup_m0 () Int)
(declare-fun wg_z () Int)
(declare-fun wg_y () Int)
(assert
 (let (($x24 (= intrinsic_k 16)))
(let (($x23 (= intrinsic_mn 16)))
(let ((?x185 (* intrinsic_k (+ (* 2 (* k0 m0 m1 m2)) (* 2 (* k0 n0))))))
(let (($x186 (<= ?x185 65536)))
(let (($x179 (= wg_x (* sg_m_cnt sg_n_cnt subgroup_size))))
(let ((?x117 (* sg_m_cnt sg_n_cnt)))
(let (($x120 (<= ?x117 10)))
(let (($x118 (>= ?x117 1)))
(let (($x176 (= n0 (* intrinsic_mn sg_n_cnt subgroup_n0))))
(let ((?x147 (* m0 m1 m2)))
(let (($x174 (= ?x147 (* intrinsic_mn sg_m_cnt subgroup_m0 subgroup_m1 subgroup_m2))))
(let (($x106 (>= subgroup_n0 1)))
(let (($x105 (>= subgroup_m2 1)))
(let (($x104 (>= subgroup_m1 1)))
(let (($x103 (>= subgroup_m0 1)))
(let (($x173 (= (mod n0 (* intrinsic_mn subgroup_n0)) 0)))
(let (($x170 (= (mod m2 (* intrinsic_mn subgroup_m2)) 0)))
(let (($x96 (= (mod m1 subgroup_m1) 0)))
(let (($x94 (= (mod m0 subgroup_m0) 0)))
(let (($x92 (<= sg_n_cnt 32)))
(let (($x91 (>= sg_n_cnt 1)))
(let (($x90 (<= sg_m_cnt 32)))
(let (($x89 (>= sg_m_cnt 1)))
(let ((?x161 (* intrinsic_mn (div (+ 15 intrinsic_mn) intrinsic_mn))))
(let (($x167 (<= n0 ?x161)))
(let ((?x154 (* intrinsic_mn (div (+ 63 intrinsic_mn) intrinsic_mn))))
(let (($x166 (<= m2 ?x154)))
(let (($x86 (<= m1 64)))
(let (($x85 (<= m0 32)))
(let ((?x137 (* intrinsic_k k0)))
(let ((?x144 (* intrinsic_k (div (+ 143 intrinsic_k) intrinsic_k))))
(let (($x165 (= (mod ?x144 ?x137) 0)))
(let (($x82 (>= k0 1)))
(let (($x81 (>= n0 1)))
(let (($x80 (>= m2 1)))
(let (($x79 (>= m1 1)))
(let (($x78 (>= m0 1)))
(let (($x163 (= (mod ?x161 n0) 0)))
(let (($x156 (= (mod ?x154 m2) 0)))
(let (($x73 (= (mod 64 m1) 0)))
(let (($x71 (= (mod 32 m0) 0)))
(let ((?x68 (div 512 intrinsic_k)))
(let (($x149 (<= k0 ?x68)))
(let (($x148 (<= n0 512)))
(let (($x146 (<= ?x147 512)))
(let (($x145 (<= ?x137 ?x144)))
(let (($x57 (= (mod n0 intrinsic_mn) 0)))
(let (($x55 (>= n0 intrinsic_mn)))
(let (($x54 (= (mod m2 intrinsic_mn) 0)))
(let (($x51 (>= m2 intrinsic_mn)))
(let (($x50 (<= wg_x 1024)))
(let (($x48 (= subgroup_size 64)))
(let (($x47 (= wg_z 1)))
(let (($x46 (= wg_y 1)))
(and $x46 $x47 $x48 $x50 $x51 $x54 $x55 $x57 $x145 $x146 $x148 $x149 $x71 $x73 $x156 $x163 $x78 $x79 $x80 $x81 $x82 $x165 $x85 $x86 $x166 $x167 $x89 $x90 $x91 $x92 $x94 $x96 $x170 $x173 $x103 $x104 $x105 $x106 $x174 $x176 $x118 $x120 $x179 $x186 $x23 $x24))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)

</issue_description>

Comments on the Issue (you are @copilot in this section)

@levnach As a bisection shows: the regression happenned at 7395152. Not sure how to fix it.

• Fixes Z3 Regression: solver.check() returns 'unknown' instead of 'sat' #8740

---

✨ Let Copilot coding agent set things up for you — coding agent works faster and does higher quality work when set up for your repo.