[fstar-build-fix] Fix nl-arith regression on F* obligation failedQueries-Pulse.Lib.PriorityQueue-3 (#10344)

## Summary

An F* proof build failed to discharge a proof obligation because z3
returned `unknown` instead of the expected `unsat`. This PR fixes an
attributed nonlinear-arithmetic performance/completeness **regression**
in z3 that caused the failure.

- Originating F* build run:
https://github.com/Z3Prover/z3/actions/runs/30685489878
- Failing query:
`inputs/fstar-build-failures/run-30685489878/pulse/failedQueries-Pulse.Lib.PriorityQueue-3.smt2`
(`Z3Prover/bench`)
- Query label: `failedQueries-Pulse.Lib.PriorityQueue-3`
- z3 ref under test: `1ba30df028`
- **Expected result:** `unsat` — **Observed on ref under test:**
`unknown` (`:reason-unknown "canceled"`, i.e. the embedded `(set-option
:rlimit 5000000)` budget was exhausted).

The query embeds its own options (`smt.arith.solver=6`,
`smt.mbqi=false`, `auto_config=false`, `rlimit=5000000`, ...); all runs
below honor those embedded options.

## Root cause and attribution

Bisecting `./z3` between a known-good baseline
(`a05be8a291`, which returns `unsat`) and
the ref under test identified the first bad commit as:

> **`90fe0aa0f32d4cf66f3503c249d1878a39c0cf3c` — "Imp fix (#10304)"**

That commit adds `monomial_bounds::propagate_fixed_rows()` and calls it
from `nla::core::propagate()`, gated by the new parameter
`smt.arith.nl.propagate_fixed_rows` (default **true**). The routine
scans **all** LP rows on **every** nonlinear-propagation call, and calls
`lra.find_feasible_solution()` whenever anything is propagated. On this
obligation that extra work consumes the `rlimit` budget before a proof
is found, so a query that was previously `unsat` becomes `unknown`
(`canceled`). This is a pure performance/completeness regression from a
newly-added, parameter-gated heuristic — not a soundness issue in the
query.

## Fix

Default `smt.arith.nl.propagate_fixed_rows` to **false**, restoring the
pre-#10304 behaviour. The heuristic and its code are left intact and
remain available as opt-in via `smt.arith.nl.propagate_fixed_rows=true`,
pending a more efficient implementation (e.g. not re-scanning every row
on every propagation call).

This is a one-line change in `src/params/smt_params_helper.pyg`; no
solver check is weakened and the failing behaviour is not masked — the
regressing heuristic is simply returned to being opt-in.

## Reproduction and validation

All builds via `python3 scripts/mk_make.py && make -C build -j8`
(CMake/Ninja unavailable in this environment; the Makefile build
produces an equivalent binary).

| z3 | `smt.arith.nl.propagate_fixed_rows` | Result |
|---|---|---|
| baseline `a05be8a` | (n/a, pre-feature) | `unsat` |
| ref under test `1ba30df` | true (default) | `unknown` (canceled) |
| ref under test `1ba30df` | false (override) | `unsat` |
| **patched `1ba30df` (this PR)** | false (new default) | **`unsat`** |

Before the fix the query reproduced the `unknown`/`canceled` failure;
after the fix the patched binary returns the expected `unsat` with the
query's embedded options unchanged.

## Notes / uncertainty

This change restores correctness-preserving behaviour by disabling an
optional heuristic by default rather than reworking its cost model. A
follow-up could re-enable the heuristic once its per-propagation cost is
bounded (e.g. only scanning rows touched since the last call). Created
as a **draft** for maintainer review.




> [!WARNING]
> <details>
> <summary>Firewall blocked 1 domain</summary>
>
> The following domain was blocked by the firewall during workflow
execution:
>
> - `pypi.org`
>> To allow these domains, add them to the `network.allowed` list in
your workflow frontmatter:
>
> ```yaml
> network:
>   allowed:
>     - defaults
>     - "pypi.org"
> ```
>
> See [Network
Configuration](https://github.github.com/gh-aw/reference/network/) for
more information.
>
> </details>


> Generated by [Fix a Z3 failure on an F* proof
obligation](https://github.com/Z3Prover/bench/actions/runs/30692520945)
· 398.4 AIC · ⌖ 21.5 AIC · ⊞ 9.4K ·
[◷](https://github.com/search?q=repo%3AZ3Prover%2Fz3+%22gh-aw-workflow-id%3A+fstar-build-fixer%22&type=pullrequests)

<!-- gh-aw-agentic-workflow: Fix a Z3 failure on an F* proof obligation,
engine: copilot, version: 1.0.65, model: claude-opus-4.8, id:
30692520945, workflow_id: fstar-build-fixer, run:
https://github.com/Z3Prover/bench/actions/runs/30692520945 -->

<!-- gh-aw-workflow-id: fstar-build-fixer -->
<!-- gh-aw-workflow-call-id: Z3Prover/bench/fstar-build-fixer -->

Co-authored-by: z3prover-ci-bot[bot] <305651407+z3prover-ci-bot[bot]@users.noreply.github.com>
Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>

src/params/smt_params_helper.pyg

@@ -101,7 +101,7 @@ def_module_params(module_name='smt',
                           ('arith.nl.delay', UINT, 10, 'number of calls to final check before invoking bounded nlsat check'),
                           ('arith.nl.propagate_linear_monomials', BOOL, True, 'propagate linear monomials'),
                           ('arith.nl.optimize_bounds', BOOL, True, 'enable bounds optimization'),
-                          ('arith.nl.propagate_fixed_rows', BOOL, True, 'scan LP rows for fixed variables'), 
+                          ('arith.nl.propagate_fixed_rows', BOOL, False, 'scan LP rows for fixed variables'), 
                           ('arith.nl.optimize_bounds_lp_max_vars', UINT, 120, 'skip LP-based nonlinear bounds optimization when the number of candidate monomial variables exceeds this threshold (0 = unlimited)'),
                           ('arith.nl.cross_nested', BOOL, True, 'enable cross-nested consistency checking'),
                           ('arith.nl.log', BOOL, False, 'Log lemmas sent to nra solver'),