AUTOMATED REASONING · CONTINUOUSLY VERIFIED

Xolver⊨

∀φ ∈ SMT-LIB. Xolver(φ) ∈ {sat, unsat}

A high-performance SMT solver with a focus on quantifier-free nonlinear arithmetic — front-ended by SOMTParser, and proven on every commit against Z3, cvc5, MathSAT and more at the Observatory.

Get Xolver Live benchmarks ↗

instances solved: 52,813
wrong answers: 0
solvers compared: 9+
leading logic: QF_NRA

latest official SMT-LIB run · live data on the Observatory

xolver — smt-lib v2.6⌘

01 · ECOSYSTEM

One system, three components

xolver.org is the unified home for the solver, its parser front end, and the observatory that keeps both honest.

⊢

Xolver

the solver

The decision core. A C++ SMT solver engineered for quantifier-free nonlinear real and integer arithmetic, built to answer sat or unsat — fast, and never wrong.

C++SMTQF_NRA · QF_NIA

github.com/fuqi-jia/Xolver ↗

SOMTParser

the front end

A standalone C++ parser library for SMT-LIB and OMT. It turns raw problem text into typed ASTs — the shared front end for Xolver and anything else you build.

C++ librarySMT-LIB v2.6OMT

github.com/fuqi-jia/SOMTParser ↗

⊨

Observatory

the proving ground

Continuous benchmarking infrastructure. Every commit runs the full SMT-LIB suite against Z3, cvc5, MathSAT, Yices and more — gated on zero wrong answers.

CI benchmarking9 solvers0-wrong gate

observatory.xolver.org ↗github.com/fuqi-jia/Xolver-Observatory ↗

02 · PIPELINE

From formula to certified verdict

Three judgments, composed. Each stage of the toolchain is stated the way we like our systems: as an inference rule.

φ : SMT-LIB2

SOMTParser ⇓ φ

AST(φ) well-typed

01 — Parse

SOMTParser reads SMT-LIB / OMT input and produces a fully typed abstract syntax tree.

AST(φ)

𝒯 = NRA ∪ NIA ∪ …

Xolver(φ) ∈ {sat, unsat}

02 — Decide

The Xolver core applies theory-aware search and nonlinear reasoning to reach a verdict.

Xolver(φ) = v

∀ oracle O. O(φ) = v

commit ✓ observatory-certified

03 — Observe

Every commit is cross-checked against reference solvers on the full suite — zero wrong answers, or the gate stays closed.

03 · BENCHMARKS

Measured, not claimed

Solved-instance rates by SMT-LIB logic, from the latest official suite. The Observatory tracks every run, every regression, every solver.

full capability matrix ↗

LogicCasesXolver vs best competitor (% solved)Leader

QF_NRA9,280

xolver 94.1%

z3 92.2%

⊢ xolver

QF_NIRA2,560

xolver 86.4%

z3 81.8%

⊢ xolver

QF_LIA12,450

xolver 91.6%

z3 93.5%

QF_NIA6,410

xolver 83%

z3 89%

QF_UFNIA1,420

xolver 65.6%

z3 77.5%

snapshot: SMT-LIB benchmark 2026-08-01 · correctness gate 0 wrong / 0 crash · live numbers at observatory.xolver.org

⊨xolver.orgresearch in progress

Γ ⊢ BUILDING

Proof in progress_

Xolver and its Observatory are being prepared for public release. The solver is open on GitHub; benchmark results will follow once the full dataset has been verified.

⊢↗

SMT SOLVER

Xolver

Source code, releases, and development progress

⊨↗

BENCHMARKING

Observatory

Private while the benchmark dataset is being prepared

∀φ · solve · verify · repeatobservatory access: pending