[API Coherence] Report for 2026-06-09 — Full Verification Run (11 Issues Confirmed)

[github-actions[bot]]

Summary

Full verification run — all 44 Z3 API families analyzed in prior runs. This run re-verified all 11 cached issues against the current codebase (2026-06-09).

Metric	Value
API families analyzed (cumulative)	44
Issues verified	11
Newly resolved	0
Still unresolved	11
Priority breakdown	3 High · 5 Medium · 3 Low

Languages: C · C++ · Python · Java · .NET · TypeScript/JS · OCaml · Go · Rust

Go updates noted (new files confirmed in repo): finiteset.go, relations.go, simplifier.go (basic Simplifier type with GetSimplifierDescr but still missing enumeration functions). Despite these, the gaps below remain.

---

High Priority

1. Rust: No Simplifier API in high-level crate

Missing in: z3/src/ (prove-rs/z3.rs). Have in: all other languages including Go.
z3-sys has full FFI (Z3_mk_simplifier, Z3_simplifier_and_then, Z3_simplifier_using_params, Z3_solver_add_simplifier).
Fix: Add Simplifier<'ctx> struct with new/and_then/using_params/get_help/get_param_descrs and Solver::add_simplifier().

2. Rust: No FiniteSet API (missing in both z3-sys and high-level crate)

Missing in: z3-sys/src/generated/functions.rs (zero Z3_mk_finite_set_* entries) and z3/src/. Have in: all other languages (Go: finiteset.go).
Fix: Re-run bindgen to pick up finite set functions in z3_api.h, then add FiniteSet<'ctx> in z3/src/.

3. Rust: No polymorphic datatype support

DatatypeBuilder is monomorphic only. Have in: all other languages.
z3-sys has Z3_mk_type_variable + Z3_mk_polymorphic_datatype.
Fix: Extend DatatypeBuilder or add PolymorphicDatatypeBuilder; add Context::type_variable().

---

Medium Priority

4. OCaml + Go: No polynomial subresultants

Z3_polynomial_subresultants exposed in C++/Python/Java/.NET/TS/Rust(z3-sys) but absent from src/api/ml/ and src/api/go/.
Fix (OCaml): Add polynomial_subresultants ctx p q x in z3.ml under Arithmetic.
Fix (Go): Add (c *Context) PolynomialSubresultants(p, q, x *Expr) []*Expr in arith.go.

5. Go: No MkFreshConst / MkFreshFuncDecl

Z3_mk_fresh_const and Z3_mk_fresh_func_decl have no Go wrappers. Have in: all other languages.
Fix: Add to z3.go or new const.go.

6. Go: No EnableTrace / DisableTrace

log.go has OpenLog/CloseLog/AppendLog/IsLogOpen but not EnableTrace(tag)/DisableTrace(tag).
Fix: Add two package-level functions in log.go calling C.Z3_enable_trace / C.Z3_disable_trace.

7. Rust: No logging wrappers (EnableTrace, DisableTrace, OpenLog, CloseLog)

None exposed in z3/src/. z3-sys has all four bindings.
Fix: Add free functions enable_trace(tag: &str), open_log(path: &str) -> bool, etc.

8. Simplifier enumeration missing in C++, Python, TS/JS, Go, Rust

Z3_get_num_simplifiers + Z3_get_simplifier_name are exposed in Java/NET/OCaml but not in C++ (z3++.h), Python (z3.py), TypeScript, Go (simplifier.go has GetSimplifierDescr only), or Rust high-level crate. z3-sys has both bindings.
Fix per language: context::num_simplifiers() + simplifier_name(i) wrappers in each binding.

9. C++ + Rust: No type_variable wrapper

No context::type_variable() in z3++.h; users must call Z3_mk_type_variable() directly (see examples/c++/example.cpp:1016). Rust z3-sys has it but z3/src/ does not.
Fix (C++): Add sort type_variable(symbol const& name) to context class in z3++.h.
Fix (Rust): Add Context::type_variable(name: &Symbol) -> Sort in sort.rs.

---

Low Priority

10. .NET: Missing MkLinearOrder, MkPiecewiseLinearOrder, MkTreeOrder

Context.cs has MkPartialOrder + MkTransitiveClosure but not the other three special relation constructors. Have in: all other languages (Go: relations.go).
Fix: Add three methods to Context.cs calling Native.Z3_mk_linear_order, Z3_mk_piecewise_linear_order, Z3_mk_tree_order.

11. Go: No AST.Id() method

AST has Hash() (Z3_get_ast_hash) but no Id() (Z3_get_ast_id). Have in: all other languages.
Fix: Add func (a *AST) Id() uint { return uint(C.Z3_get_ast_id(a.ctx.ptr, a.ptr)) } in z3.go.

---

Next Steps

1. Monitor z3_api.h for new C API functions
2. Monitor prove-rs/z3.rs for upstream Rust fixes (issues 1–3, 7–9)
3. Re-verify after PRs to Go, .NET, C++, or Rust bindings

Generated by API Coherence Checker · sonnet46 3M · ◷

• expires on Jun 16, 2026, 5:12 AM UTC

[github-actions[bot]]

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

A newer discussion is available at Discussion #9805.