I'm working on analyzing solver behavior in cases where the result is sat or unknown, and I'd like to retrieve some form of proof or trace to understand what went wrong or what path the solver took. However, Solver::get_proof() is only available when the result is unsat, which limits post-analysis in other cases.

To address this, I was exploring the clause inference callback mechanism, as described in the Z3 documentation (via Z3_solver_register_on_clause in the C API). This seems like a viable way to observe proof steps.

However, I couldn't find any support for this functionality in z3.rs.
Is there a recommended way to hook into clause inferences from Rust using this crate, or would I need to manually bind and call the Z3_solver_register_on_clause C function myself?

I'd appreciate any guidance and would be happy to help contribute an implementation if this sounds like a worthwhile addition.

Thanks!