◉ COOLJAPAN
← All posts
August 5, 2026 • 9 min read

OxiZ 0.3.2 Released — Eight Unmerged Pull Requests, One In-House Soundness Sweep, and 168/168 Correct Again

OxiZ 0.3.2 is a soundness release driven by an external differential-testing report: 8 pull requests, 0 merged, every fix independently reimplemented from scratch and backed by a regression test. EUF congruence, Bool/EUF encoding, Arithmetic⇄EUF combination, and NLSAT conflict analysis are all corrected — 168/168 Correct on the Z3 parity suite, 9,953 tests passing. Pure Rust, Apache-2.0.

release oxiz smt-solver z3 formal-verification pure-rust soundness differential-testing

Someone ran 50 random QF_UF queries against real Z3 and OxiZ disagreed on 17 of them. That is not a rounding error — that is a solver you cannot trust.

Today we released OxiZ 0.3.2 — a soundness release that started with an outside bug report and ended as a from-scratch audit of every code path it touched. GitHub issue #25 showed that the project’s own 168-case “Z3 parity” suite was a regression suite, not a differential-testing result: a random 50-instance QF_UF sample run against a real z3 binary found a 34% (17/50) disagreement rate. The reporter opened eight pull requests (#26–#33) against the bugs they found. Per project policy — there is no CLA or uniform contribution-provenance guarantee here yet — none of them were merged directly. Every one was read in full for its diagnostic value, and every fix in this release is an independent, from-scratch reimplementation, verified against a regression test derived from a minimal repro that fails on the pre-fix code. ~270 such tests were added in the process.

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 WASM) and runs everywhere. 0.3.2 is what that transparency is for: a bug report with reproducible counterexamples, applied line by line against a codebase with no black box to hide behind.

Why OxiZ 0.3.2 is a game changer

Before this release, four independent bug families could make OxiZ confidently wrong without a single crash:

0.3.2 ends all of that:

This is not a blanket “100% Z3 compatibility” claim — the parity suite still doesn’t include plain QF_UF, the exact fragment the reporter’s own sample targeted. Issue #25 stays open on purpose: this release closes the bugs it led to, not the broader claim.

Technical Deep Dive: nine bugs, one shape each

EUF congruence + Bool/EUF encoding (oxiz-theories/src/euf/solver/congruence.rs, oxiz-solver/src/solver/encode/bool_euf_encoding.rs). Congruence closure republished a re-canonicalized node’s signature without evicting its old entry, so a stale signature-table hit could merge in a node that had since diverged. Separately, non-Bool ite, Bool-sorted =, and Bool terms in UF argument position each had a gap in how they reached EUF completion. All four are fixed with evict-and-reinsert signature maintenance plus explicit hoisting/completion for each encoding gap.

Arithmetic⇄EUF combination (oxiz-solver/src/solver/encode/numeric_purification.rs, oxiz-theories/src/arithmetic/solver.rs, oxiz-solver/src/solver/theory_manager/nelson_oppen.rs). Numeric UF arguments are now purified into fresh proxy variables with a get-value alias back to the original term; a bounded per-round “care graph” probes for entailed (dis)equalities via new Farkas-certificate probes; and for the genuinely non-convex case, a small explicit case-split disjunction is asserted before conceding sat.

NLSAT conflict analysis (oxiz-nlsat/src/solver/conflict.rs, solver/resample.rs). The 1-UIP resolution step now reconstructs every resolved-in literal from the trail itself instead of negating the wrong thing; theory-forced literals with no clause backing are tracked explicitly so an empty clause through one yields Unknown, never a fabricated Unsat; and a new witness ledger retries a different point from the same region instead of conceding infeasibility at decision level 0.

Parser and encoder edge cases. A distinct-over-constants query that constant-folds to TermKind::False now returns the correctly-signed literal (oxiz-solver/src/solver/encode.rs); define-fun call-site arguments are substituted by their exact TermId rather than re-derived by name (oxiz-core/src/smtlib/parser/); a lone 0 clause terminator in a DIMACS file — the empty, unconditionally-false clause — is no longer silently dropped (oxiz-sat/src/dimacs.rs); and pure-literal elimination now checks an explicit trail-status exclusion set instead of contradicting a fact the trail already forced.

Getting Started

Add OxiZ to your project:

cargo add oxiz

The distinct-over-constants fix, demonstrated — this query answered unsat before 0.3.2:

use oxiz_solver::Context;

let mut ctx = Context::new();
let output = ctx.execute_script(r#"
    (set-logic QF_LIA)
    (assert (distinct 5 2))
    (check-sat)
"#).expect("script should parse and run");

assert_eq!(output[0], "sat");
// Before 0.3.2, `distinct` over two constants constant-folded to a Tseitin
// `False` node whose encoder returned the wrong-polarity literal for it —
// so a query that is trivially true (5 != 2) reported `unsat` instead.

Feature flags are unchanged: nlsat for nonlinear arithmetic, optimization for MaxSMT/OMT, spacer for CHC model checking, proof for DRAT/Alethe/LFSC export, full for everything.

What’s New in 0.3.2

Breaking (0.x API)

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. 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 a “you’re 34% wrong on this sample” bug report by re-deriving every fix from scratch and shipping the regression tests to prove it.

The era of trusting a solver’s parity claims without tracked evidence is over. Pure Rust formal reasoning is here — audited, honest, and sovereign.

— KitaSan at COOLJAPAN OÜ August 5, 2026

↑ Back to all posts