[API Coherence] Report for 2026-07-07 – Re-verification Run (Full API Surface)

[github-actions[bot]]

Summary

Re-verification run against commit d9d3be9. All API families were analyzed in prior runs. This run re-verified all 14 cached issues — none have been resolved.

Metric	Value
APIs analyzed (cumulative)	~45 API families / 200+ functions
Languages covered	C, C++, Python, Java, .NET, TypeScript/JS, OCaml, Go, Rust
Issues re-verified	14
Issues resolved	0
New API-breaking commits since last run	0

---

High Priority

1. Rust: Missing Simplifier API (high-level z3 crate)

z3-sys exposes FFI bindings but no Simplifier type or Solver::add_simplifier() exists.
Missing in: Rust | Available in: all others
Fix: Add Simplifier<'ctx> struct + Solver::add_simplifier() in prove-rs/z3.rs

2. Rust: Missing FiniteSet API (both z3-sys and z3 crate)

No Z3_mk_finite_set_* FFI bindings at all.
Missing in: Rust | Available in: all others
Fix: Add FFI bindings to z3-sys and a FiniteSet<'ctx> type in z3 crate

3. Rust: Missing polymorphic datatype support

z3-sys has Z3_mk_polymorphic_datatype/Z3_mk_type_variable but DatatypeBuilder has no polymorphic mechanism.
Missing in: Rust | Available in: all others
Fix: Extend DatatypeBuilder to accept type parameters

---

Medium Priority

4. OCaml and Go: Missing Polynomial Subresultants

Z3_polynomial_subresultants not wrapped.
Missing in: OCaml (src/api/ml/), Go (src/api/go/)

5. Go: Missing MkFreshConst / MkFreshFuncDecl

No wrappers for Z3_mk_fresh_const / Z3_mk_fresh_func_decl.
Missing in: Go | Fix: Add to src/api/go/

6. Go: Missing EnableTrace / DisableTrace

log.go has OpenLog/CloseLog but not trace functions.
Missing in: Go | Fix: Add to src/api/go/log.go

7. Rust: Missing logging wrappers (enable_trace, open_log, etc.)

z3-sys has FFI but high-level z3 crate has no wrappers.
Missing in: Rust

8. C++, Python, Go, Rust: Missing simplifier enumeration

GetNumSimplifiers/GetSimplifierName only in .NET, Java, OCaml.
Missing in: C++ (z3++.h), Python (z3.py), Go (partial), Rust

9. C++ and Rust: Missing mk_type_variable wrapper

Z3_mk_type_variable not wrapped in C++ or Rust high-level crate.
Missing in: C++, Rust

10. C++, Python, .NET, OCaml: Missing re_power (Z3_mk_re_power)

Exact-repetition regex available in Java, TypeScript/JS, Go, Rust but not others.
Missing in: C++, Python, .NET, OCaml

11. OCaml and Rust: Missing seq functional ops

seq_map/seq_mapi/seq_foldl/seq_foldli not wrapped.
Missing in: OCaml (z3.ml), Rust (z3/src/ast/seq.rs)

12. TypeScript/JS, C++, OCaml, Rust: Missing optimize_get_lower/upper_as_vector

Triple (inf, value, eps) vector form only in Python, Java, .NET, Go.
Missing in: TypeScript/JS, C++, OCaml, Rust

---

Low Priority

13. .NET: Missing MkLinearOrder, MkPiecewiseLinearOrder, MkTreeOrder

Only MkPartialOrder and MkTransitiveClosure present.
Missing in: .NET (Context.cs) | Fix: Add near line 5168

14. C++ and .NET: Missing allchar (Z3_mk_re_allchar)

Match-any-char regex not wrapped.
Missing in: C++ (z3++.h), .NET (Context.cs)

15. Go: Missing AST.Id() method

Hash() exists but no Id() wrapping Z3_get_ast_id.
Missing in: Go (z3.go) | Fix: 1-line addition

---

Progress

• API surface: ~100% analyzed across all language bindings
• Next runs: Monitor z3_api.h for new C API additions; track prove-rs/z3.rs for Rust fixes

Generated by API Coherence Checker · 124.8 AIC · ⌖ 13.6 AIC · ⊞ 28.7K · ◷

• expires on Jul 14, 2026, 5:01 AM UTC

[github-actions[bot]]

This discussion has been marked as outdated by API Coherence Checker.

A newer discussion is available at Discussion #10069.