rz3 v0.1.2 — first public release

First public release of rz3: a deterministic, exact-rational SMT solver in pure Rust.

Highlights

• DPLL(T)/CDCL with a complete linear-arithmetic core — never returns unknown on a linear-arithmetic query. Strict inequalities use a symbolic δ-infinitesimal (Dutertre–de Moura); the feasibility Simplex avoids cycling via lexicographic ε-perturbation.
• Exact arithmetic: arbitrary-precision rationals, no floating-point in the decision core.
• Deterministic: run-to-run bit-identical, verified by an n=30 SHA-256 harness.
• Zero native dependencies → WebAssembly-deployable.
• Difference-Logic fragment decided by native Bellman-Ford negative-cycle detection.

Scope and limitations (vs. Z3)

Smaller theory coverage, no optimization (MaxSMT/OMT), partial proof/unsat-core, a subset of SMT-LIB, less performance tuning. See README.

License

Dual-licensed MIT OR Apache-2.0.

Verified: suite 87/0, clippy clean, cargo publish --dry-run valid.