Feature Request: Z3 NIA Support for Solving Hard Arithmetic Constraints

[gustavo-grieco]

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)

; 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)

; 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/:

# 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/

[gustavo-grieco]

Ok, fixed the example to use 2**256 divisors, so bitwuzla cannot solve it.

[msooseth]

It's something to consider. However, again, this work ought to be done by the SMT solver IMO. However, we could of course launch more than one SMT solvers, or do more than one (or more than 2/3/etc) phases, as you mention. It feels like we are doing a poor job of what the solver ought to be doing, so I'm a bit hesitant.

At the same time, we can't wait around forever for the SMT solvers to pick up the slack. Also to consider is whether we have more information than what the SMT solver would have. I think in this instance we don't have more information (which may be in contrast to the PR #995 )