◉ COOLJAPAN
← All posts
August 26, 2026 • 12 min read

OxiZ 0.3.3 Released — Fifteen Benchmarks Said sat, All Fifteen Were Unsat, All Fifteen Are Fixed

OxiZ 0.3.3 is a soundness release: fifteen SMT-LIB benchmarks marked unsat in their own header were answering sat, most in under a second. Eight independent defects fixed, plus first-class RoundingMode, end-to-end recursive functions, algebraic-number model witnesses, and a working wasm32 clock. 170/170 Z3 parity, 10,323 tests. Pure Rust, Apache-2.0.

release oxiz smt-solver z3 formal-verification pure-rust soundness wasm

Fifteen SMT-LIB benchmarks carry (set-info :status unsat) in their own file header. OxiZ answered sat on every one of them, most in under a second. That is not a rare edge case — soundness is the one property an SMT solver exists to guarantee, and this release found eight independent ways OxiZ was breaking it.

Today we released OxiZ 0.3.3 — a soundness release built around seventeen .smt2 files from the public, non-incremental SMT-LIB distribution, all named in issues #44–#50. Fifteen were obtained and run against the 0.3.2 tree; all fifteen came back wrong. None of them does any more. The two QF_BV files in #47 were never obtained — the archive is 1.73 GB — so #47 stays open and unreproduced rather than claimed fixed by inference.

No C. No C++. No Fortran. OxiZ reimplements Z3 entirely in Rust — the SAT core, theory solvers, quantifier instantiation, optimization, and proof system are all memory-safe Rust you can read end to end. It compiles to a single static binary or WebAssembly and runs everywhere — and as of 0.3.3, “everywhere” stops being aspirational for the browser: the crate that made every build read the system clock unconditionally, which is fine on every target except wasm32-unknown-unknown, is gone.

Why OxiZ 0.3.3 is a game changer

Before this release, eight independent defects could each turn a genuinely unsatisfiable formula into a confidently wrong sat, with no crash to flag it:

0.3.3 ends all of that:

This is not a claim that the 170-benchmark parity suite improved because of these fixes — it can’t. A curated regression suite already at 100% cannot show a soundness gain; that’s exactly the limitation issue #25 raised, and it stays open on purpose. The evidence for this release lives in the fifteen benchmarks and the 43 tests built from them, not in the parity number.

Technical Deep Dive

Eight bugs, one shape each. Every defect above is a case of a real check that existed somewhere in the tree but had a gap in what could reach it: the let-blindness was a parser artifact (smtlib/parser/terms.rs), the trichotomy gap was a syntactic pre-pass that enumerated connectives instead of covering the encoder’s one true chokepoint (solver/encode.rs, now 86 lines shorter after four overlapping walks were deleted in favor of one), the array bug was a setter that only the Select arm could reach (track_theory_vars.rs), and the load-dependent verdict was a skip that forgot to tell the honesty gate it had skipped (check_core.rs). None of these needed a new theory — they needed the existing one wired to fire every time, not most of the time.

Three honest rejections became features. Recursive functions (define-fun-rec/define-funs-rec) are now discharged by fuel-bounded unfolding with two termination-safe certificates — saturation when the unfolding boundary closes, model re-computation otherwise — never by inlining, which is why mutual recursion (is-even/is-odd) just works. RoundingMode is a real fifth built-in sort with closure and distinctness axioms and binder relativization for quantifiers, not a free uninterpreted domain masquerading as one. And (assert (= (* x x) 2.0)) now returns sat with an actual root-obj term reproducing z3 4.15.4’s exact spelling rule, instead of unknown — backed by a new algebraic witness carrier (oxiz-theories/src/nl_witness.rs) that also fixed five root-isolation bugs in oxiz-nlsat along the way, one of which would have made x·x = 2 answer sat on the integers.

Nonlinear integer arithmetic gets an LP relaxation, and Gomory cuts finally run. A new engine (oxiz-theories/src/arithmetic/nla/) linearizes every nonlinear product into a monic-constrained fresh variable and loops LP feasibility, exact BigInt consistency checks, McCormick and square-tangent cuts, and integer case splits — turning goals like x² + y² + 1 = 0 and x,y,z ≥ 2 ∧ x·y·z ≤ 7 from unknown into unsat, each with a real infeasibility certificate. Separately, oxiz-theories’s Gomory and GMI cut generators had been fully implemented and completely unreachable — zero callers anywhere in the repo. A new root cutting-plane loop now runs them before any branch-and-bound push, so a simplex error there is an honest integer-infeasibility proof.

WASM gets a working clock and a smaller footprint. std::time::Instant::now() is a hard unreachable!() on wasm32-unknown-unknown, and OxiZ read it unconditionally on the main solve path — so any real (check-sat) trapped, and because it’s an abort rather than an unwind, the whole session was left permanently poisoned afterward. New crate oxiz-time re-exports std::time bit-identically everywhere that has a clock and freezes to a const zero everywhere that doesn’t; 101 call sites across 47 files were rewritten onto it. Separately, oxiz-nlsat is now behind an opt-out nlsat feature — dropping it from a size-tuned browser build measured 1,557,287 → 1,363,027 raw bytes (−12.5%) and 573,181 → 504,913 after gzip (−11.9%), at the honestly-documented cost of every QF_NRA nonlinear verdict becoming unknown (QF_NIA is unaffected either way, since it’s re-verified in exact rational arithmetic regardless).

Getting Started

cargo add oxiz

The let-blindness fix, demonstrated — this query answered sat on 0.3.2:

use oxiz_solver::Context;

let mut ctx = Context::new();
let output = ctx.execute_script(r#"
    (set-logic QF_LIA)
    (declare-const x Int)
    (declare-const y Int)
    (assert (= x 2))
    (assert (= y (+ x 1)))
    (assert (let ((unused 0)) (not (= y 3))))
    (check-sat)
"#).expect("script should parse and run");

assert_eq!(output[0], "unsat");
// x = 2, y = x + 1 = 3, so `y != 3` is false and the whole conjunction is
// unsat. Before 0.3.3, the vacuous `(let ((unused 0)) ...)` wrapper around
// the disequality silently disabled the assert-time trichotomy pre-pass —
// the *only* difference from an equivalent let-free query was a binding
// nothing used, and that was enough to flip the verdict to `sat`.

Feature flags: nlsat for nonlinear arithmetic, scripting for the embedded Rhai tactic engine, optimization for MaxSMT/OMT, spacer for CHC model checking, proof for DRAT/Alethe/LFSC export, full for everything. Both nlsat and scripting are on by default — see Tips below if you want them off.

What’s New in 0.3.3

Breaking (0.x API — see the CHANGELOG for full detail on each)

Fixed

Added

Full itemized detail, crate by crate, is in the CHANGELOG.

Tips

This is the foundation

OxiZ is the formal-reasoning backbone of the COOLJAPAN ecosystem. OxiLean uses it as its SMT proof backend; Legalis-RS uses it for legal formal verification; OxiCAD, OxiCar, OxiEDA, OxiAutoRS, OxiMed, and OxiQuant all depend on oxiz-core/oxiz-solver/oxiz-proof for constraint solving; OxiAero leans on it for flight-critical verification; OxiML builds proof-backed model checks on top of it; SciRS2 uses it to prune candidates in scirs2-symbolic’s SMT-pruned regression; and SplitRS — the file-splitting refactoring tool this very project uses to keep its own source under its line-count policy — calls it to verify a split preserves behavior. AstRS is the first downstream to depend on the exact default-features = false, features = ["std"] selection this release adds, specifically to keep rhai’s MPL-2.0 dependency out of its own license graph. Underneath, OxiZ relies on pure-Rust OxiARC for compression. The whole stack is C/C++/Fortran-free — sovereign from the SAT core all the way up to the application.

Repository: https://github.com/cool-japan/oxiz

Star the repo if you want an SMT solver that responds to “fifteen benchmarks marked unsat in their own header say sat” by fixing eight independent root causes and shipping 43 regression tests built from minimal repros, instead of patching the fifteen symptoms.

The era of trusting a solver’s soundness without a public audit trail is over. Pure Rust formal reasoning is here — audited, honest, and sovereign.

— KitaSan at COOLJAPAN OÜ August 26, 2026

↑ Back to all posts