OxiZ 0.3.1 Released — Wide Bit-Vectors Stop Lying, MBQI Reaches Completeness, and 168/168 Correct on the Z3 Parity Suite

A model that says x = 0 when the formula demands x = 2^64 isn’t an edge case — it’s the solver lying about the one thing it exists to get right.

Today we released OxiZ 0.3.1 — a soundness-and-honesty release that started as a sweep of five reported GitHub issues and became a workspace-wide hunt for one recurring bug shape: an input the code didn’t handle, silently dropped or defaulted instead of raising an error. Confirmed at release time: 9,668 tests passing, 8 skipped, plus 110 doc-tests, all --all-features, clippy/rustdoc -D warnings clean.

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. 0.3.1 turns that same read-it-end-to-end property into an audit tool: every silent-wrong-answer bug in this release was found by grepping the codebase for a shape — a catch-all match, a fallible conversion with a silent default, a guard that skipped a write — not by chasing one specific symptom.

Why OxiZ 0.3.1 is a game changer

Before this release, OxiZ could be confidently, silently wrong in ways that never showed up as a crash:

• A 128-bit bit-vector constant lost every bit past the 64th on its way into the solver — x = 2^64 silently became x = 0, and x <u 1 came back sat on a query that was actually unsatisfiable
• mk_distinct / mk_not(mk_eq) over integer arithmetic could return a model that violated the very constraint it claimed to satisfy
• An E-matching instantiation’s rebuild step ended in a catch-all that could leave the quantified variable free in the “instantiated” formula handed to the solver
• Theory-solver state could leak across MBQI rounds, producing a false Unsat on a satisfiable re-check
• A (push)(pop) loop’s own Tseitin memo leaked one full extra copy of the goal’s definitional clauses per cycle — one measured goal went from 25 to 361 original clauses over 30 cycles, with no plateau

0.3.1 ends all of that:

• ModelValue::BitVec widened from u64 to BigUint — every wide bit-vector answer is now exact, not truncated to 64 bits. This is a breaking change, and it’s the API half of three separate wide-bit-vector fixes described below.
• 5 reported issues closed (#12, #14, #17, #18, #23) plus 40+ more bugs of the same shape, found by pattern rather than symptom.
• MBQI completeness: AUFLIA 7/10→10/10, UFLIA 14/20→20/20, UFLRA 5/10→10/10 — each closed by a genuinely different mechanism (finite-range quantifier expansion, Skolem witness synthesis with CEGAR refinement, and symbolic model certification over the Reals).
• Extended suite (168 benchmarks / 19 logics): 168/168 Correct, 0 Wrong, 0 Inconclusive, 0 Timeout, 0 Error — up from 154 Correct / 12 Inconclusive / 2 Timeout at 0.3.0, with all 19 logic families individually at 100%.
• A new verdict cache turns repeated (check-sat) on an unchanged goal into an O(1) hit instead of a full re-search.

This is not a blanket “100% Z3 compatibility” claim — it’s 100% of this differential parity suite, measured under a comparator that refuses to score Unknown as agreement. TODO.md itemizes every remaining gap.

Technical Deep Dive: how the wrong answers were found and fixed

Wide bit-vector correctness (oxiz-theories/src/bv/solver.rs, oxiz-solver/src/solver/theory_bv_encode.rs, theory_manager.rs, model_builder.rs). Three independent code paths for values above 64 bits — constant assertion, EUF congruence keying, and model read-out — each keyed or truncated on the low 64 bits alone. All three now carry or read every limb of the value, via assert_const_limbs/assert_const_big and BvSolver::get_value_big.

Recursion, depth and resource hardening (~400 sites). Every remaining unguarded recursive term walk — parsers, printers, the model evaluator, substitution, and the derived Drop/Clone/PartialEq implementations on deep public enums that never appear in a backtrace — is now an explicit heap stack. The SMT-LIB term parser is fully iterative, with its old recursion-depth constant repurposed as an honest resource bound.

MBQI completeness mechanisms (oxiz-solver/src/solver/encode/finite_expand.rs, encode/exists_skolem.rs, mbqi/model_certify/). A bounded integer quantifier is expanded into the finite conjunction/disjunction it actually is; a positive-polarity existential is Skolemized so the ground solver searches for the witness instead of MBQI guessing it; and certify answers sat only after building a concrete, total interpretation of every symbol the goal mentions and checking every assertion true under it.

Repeated-(check-sat) fixes. Hyper-binary-resolution clauses now register in the learned and assertion ledgers instead of going invisible to pop; Solver::pop retracts Tseitin-memo entries per-entry through the undo journal rather than clearing the whole memo (the fix for the 25→361-clause leak above); MBQI search state is checkpointed and restored around each check; and the new verdict cache short-circuits the common unchanged-goal case entirely.

Getting Started

Add OxiZ to your project:

cargo add oxiz

The wide bit-vector fix, demonstrated — this query was silently sat before 0.3.1:

use oxiz_solver::Context;

let mut ctx = Context::new();
let output = ctx.execute_script(r#"
    (set-logic QF_BV)
    (declare-const x (_ BitVec 128))
    (assert (= x (_ bv18446744073709551616 128))) ; 2^64
    (assert (bvult x (_ bv1 128)))
    (check-sat)
"#).expect("script should parse and run");

assert_eq!(output[0], "unsat");
// Before 0.3.1, truncating to the low 64 bits encoded x as 0,
// and 0 <u 1 is true — a spurious `sat` on an unsatisfiable query.

Feature flags are unchanged from previous releases: 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.1

Breaking

• ModelValue::BitVec is now { value: BigUint, width: u32 }. New APIs: ModelValue::from_bitvec_int, from_bitvec_bits, as_bitvec, Model::assign_bitvec_big. The existing u64-based Model::assign_bitvec still compiles and now delegates to assign_bitvec_big.

Fixed

• 5 reported GitHub issues (#12, #14, #17, #18, #23) plus 40+ further bugs of the same silently-wrong-answer shape across the workspace.
• Three separate wide-bit-vector wrong-answer paths: constant assertion, congruence keying, and model read-out.
• E-matching instantiation no longer leaves the quantified variable free in the rebuilt instance.
• Theory-solver state no longer leaks across MBQI rounds.
• An unjustified conflict clause now yields Unknown, never a fabricated Unsat.
• Three independent mechanisms behind repeated-(check-sat) clause/state growth, including the genuinely unbounded Tseitin-memo leak on pop.
• Cooper quantifier elimination’s Xor/Ite expansion is now memoized, turning an exponential blow-up into O(n).
• The SMT-LIB parser now rejects mixed-width bit-vector binary operands at parse time, matching Z3.
• oxiz-math: a real multivariate polynomial GCD (primitive polynomial remainder sequence), replacing a stub.

Added

• MBQI completeness: finite-range quantifier expansion, Skolem witness synthesis with CEGAR refinement, and symbolic model certification over the Reals.
• A verdict cache for O(1) repeated (check-sat) on an unchanged goal.
• A cross-environment parity-record agreement test guarding the tracked per-OS/arch benchmark snapshots.

Changed

• Cargo.lock is no longer committed to the repository (policy change — see the CHANGELOG for the rationale and the one downstream build-tooling note).
• to_cnf_tseitin is now a dedicated, equisatisfiable CNF entry point, kept separate from the equivalence-preserving to_cnf.

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

Tips

• Re-check any bit-vector logic wider than 64 bits. Cryptographic widths, wide counters, hashing — if you rely on (_ BitVec N) for N > 64, this release fixes three independent silent-truncation bugs. Re-verify any model you cached from a pre-0.3.1 solve.
• AUFLIA/UFLIA/UFLRA are no longer the honest-gap logics. All three quantified logics that shipped below 100% at 0.3.0 are now fully certified in the parity suite — if your application routed around Unknown/Timeout on these, it’s worth re-testing without the workaround.
• Polling (check-sat) in a loop just got much cheaper. The new verdict cache makes an unchanged goal an O(1) hit — if you had application-level memoization around repeated checks, you may be able to simplify it.
• Cargo.lock is gone from the repo. If your build tooling expects a committed lockfile (the oxiz-smtcomp/Dockerfile did), run cargo fetch or any cargo build once in a fresh clone before building.
• :produce-unsat-cores now works even if enabled mid-session. Assertion names are recorded unconditionally at assert time, so (get-unsat-core) no longer requires the option to have been set before the first named assert.

This is the foundation

OxiZ is the formal-reasoning backbone of the COOLJAPAN ecosystem. OxiLean uses it as its SMT proof backend; OxiRS leans on it for validation; Legalis-RS uses it for legal formal verification, and OxigenAI builds on Legalis-RS and OxiZ together. OxiCAD, OxiCar, OxiEDA, OxiAutoRS, OxiMed, and OxiQuant all depend on oxiz-core/oxiz-solver/oxiz-proof for constraint solving. 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 whose bit-vectors don’t quietly lose bits past 64 — and that tells you Unknown rather than guessing.

Pure Rust formal reasoning is here — audited, honest, and sovereign.

— KitaSan at COOLJAPAN OÜ July 31, 2026