Feature Request: Z3 NIA Support for Solving Hard Arithmetic Constraints

Z3's Nonlinear Integer Arithmetic (NIA) solver can prove properties involving nested multiplications that **bitvector solvers cannot solve at all**. This enables verification of fixed-point math properties that would otherwise be impossible to verify.

### Benchmark: 2^256 Double Inverse (BV solvers cannot solve)

| Solver | Logic | Result | Time |
|--------|-------|--------|------|
| Z3 | QF_NIA | **unsat** | **5 ms** |
| Bitwuzla | QF_BV | unknown | >10 s (timeout) |
| Z3 | QF_BV | timeout | >10 s |

## The Problem

Ethereum smart contracts use 256-bit integers. When verifying contracts with multiplication and division, SMT solvers using bitvector theory (QF_BV) must "bit-blast" operations into boolean circuits:

- **256-bit multiplication** bit-blasts to ~1.8 million gates
- **256-bit division** is even more expensive
- **Nested operations** compound exponentially

This makes many mathematically simple properties **impossible to verify** with bitvector solvers.

## The Solution: NIA Encoding

Instead of bit-blasting, encode arithmetic using integer constraints that Z3's algebraic solver can reason about directly.

## Benchmark: Double Inverse Property

The property `inv(inv(x)) == x` where `inv(x) = 2^N / x` is a fundamental identity in fixed-point arithmetic.

### Why We Test a Restricted Case

The **original Solidity property** uses `equal_within_precision` because integer division truncates:
```
inv(x) = floor(2^N / x) // truncation error
inv(inv(x)) = floor(2^N / inv(x)) // more truncation error
```
For arbitrary `x`, the result differs from `x` by up to `2 * log2(x) + 2` bits.

Our benchmark tests a **restricted but still hard case**: values of `x` that evenly divide `2^N` (e.g., powers of 2). For these values:
- `2^N = x * inv_x` exactly (no truncation)
- `2^N = inv_x * inv_inv_x` exactly (no truncation)
- Therefore `inv_inv_x == x` exactly

This restricted case is still valuable because:
1. **BV solvers can't solve this** — both Bitwuzla and Z3 BV timeout after 10 seconds
2. **The algebraic structure is the same** — NIA's advantage comes from reasoning about `x * y = y * z ⟹ x = z`, not from handling precision bounds
3. **The full property would be even harder for BV** — adding precision tolerance makes constraints more complex

Both NIA and BV queries assert **exactly the same constraints**:
- `x > 0` and `x ≤ 2^N`
- `inv_x > 0` and `inv_x ≤ 2^N`
- `2^N = x × inv_x` (exact, no overflow)
- `inv_inv_x > 0` and `inv_inv_x ≤ 2^N`
- `2^N = inv_x × inv_inv_x` (exact, no overflow)
- Looking for counterexample: `inv_inv_x ≠ x`

### Bitvector Query (BV solvers cannot solve)

```smt2
; Double Inverse Property - Bitvector Version (2^256)
;
; Property: For x that evenly divides 2^256, inv(inv(x)) == x exactly
; Where inv(x) = 2^256 / x
;
; Uses 512-bit arithmetic since 2^256 doesn't fit in 256 bits.

(set-logic QF_BV)
(set-info :status unsat)

; The constant 2^256 in 512-bit representation
(define-fun TWO_POW_256_WIDE () (_ BitVec 512)
#x00000000000000000000000000000000000000000000000000000000000000010000000000000000000000000000000000000000000000000000000000000000)

; Upper bound for x and inv_x (2^256)
(define-fun BOUND () (_ BitVec 512)
#x00000000000000000000000000000000000000000000000000000000000000010000000000000000000000000000000000000000000000000000000000000000)

(declare-const x (_ BitVec 512))
(assert (bvugt x (_ bv0 512)))
(assert (bvule x BOUND))

(declare-const inv_x (_ BitVec 512))
(assert (bvugt inv_x (_ bv0 512)))
(assert (bvule inv_x BOUND))

; x * inv_x must equal 2^256 exactly (no wraparound)
(assert (= TWO_POW_256_WIDE (bvmul x inv_x)))

(declare-const inv_inv_x (_ BitVec 512))
(assert (bvugt inv_inv_x (_ bv0 512)))
(assert (bvule inv_inv_x BOUND))

; inv_x * inv_inv_x must equal 2^256 exactly
(assert (= TWO_POW_256_WIDE (bvmul inv_x inv_inv_x)))

(assert (not (= inv_inv_x x)))

(check-sat)
```

**Result:** Bitwuzla returns `unknown` after 10 seconds, Z3 BV times out

### NIA Query (solves in 5ms)

```smt2
; Double Inverse Property - NIA Version (2^256)
;
; Property: For x that evenly divides 2^256, inv(inv(x)) == x exactly
; Where inv(x) = 2^256 / x
;
; NIA uses unbounded integers, so multiplication is exact (no overflow).
; The bounds constraints are analogous to the BV version.

(set-logic QF_NIA)
(set-info :status unsat)

; 2^256
(define-fun TWO_POW_256 () Int 115792089237316195423570985008687907853269984665640564039457584007913129639936)

(declare-const x Int)
(assert (> x 0))
(assert (<= x TWO_POW_256))

(declare-const inv_x Int)
(assert (> inv_x 0))
(assert (<= inv_x TWO_POW_256))
; Exact multiplication (no overflow in NIA - integers are unbounded)
(assert (= TWO_POW_256 (* x inv_x)))

(declare-const inv_inv_x Int)
(assert (> inv_inv_x 0))
(assert (<= inv_inv_x TWO_POW_256))
; Exact multiplication for second inversion
(assert (= TWO_POW_256 (* inv_x inv_inv_x)))

(assert (not (= inv_inv_x x)))

(check-sat)
```

**Result:** `unsat` in 5 milliseconds

## Why the Difference?

### Bitvector (QF_BV)

To prove UNSAT, the solver must reason that `x * inv_x = inv_x * inv_inv_x` implies `x = inv_inv_x`. This requires:

1. Bit-blasting 512-bit multiplications (for overflow detection)
2. Converting the problem to SAT
3. Exploring the exponential constraint space

The 2^256 case requires 512-bit bitvectors and is simply too hard for BV solvers:
- **Bitwuzla** returns `unknown` after 10 seconds
- **Z3 BV** times out after 10 seconds

### NIA (QF_NIA)

Z3's NIA solver uses algebraic reasoning:

1. From `TWO_POW_256 = x * inv_x` and `TWO_POW_256 = inv_x * inv_inv_x`
2. We get `x * inv_x = inv_x * inv_inv_x`
3. Since `inv_x > 0`, we can cancel: `x = inv_inv_x`
4. Therefore no counterexample exists → UNSAT

This algebraic manipulation is trivial for NIA regardless of the constant size.

## Running the Benchmark

The benchmark files are in `examples/`:

```bash
# NIA version - solves instantly
time z3 examples/double_inverse_256_nia.smt2
# Result: unsat, ~5ms

# BV version with Bitwuzla - cannot solve
time bitwuzla --time-limit=10000 examples/double_inverse_256_bv.smt2
# Result: unknown after 10 seconds

# BV version with Z3 - times out
time z3 -T:10 examples/double_inverse_256_bv.smt2
# Result: timeout after 10 seconds
```

## Soundness

NIA is an **over-approximation**:
- **UNSAT from NIA → UNSAT for BV** (sound proof)
- **SAT from NIA → Unknown** (constraints may have been dropped)

This is why NIA is Phase 5, only consulted when other phases fail.

## References

- Z3 NIA documentation: https://microsoft.github.io/z3guide/docs/theories/Arithmetic/

Start with examples/double_inverse_256_nia.smt2 and examples/double_inverse_256_bv.smt2, then run the listed Z3 and Bitwuzla commands to reproduce the benchmark. Inspect the existing solver phases to locate the proposed Phase 5 integration point; done should include NIA support that preserves the stated UNSAT soundness behavior.

Written by the indexing model from the issue text.