Retrieve non-unsat proof attempts via on_clause callback

[LeskovarLukas]

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!

[Pat-Lafon]

(Not addressing your comments) In the case of sat, you get a model that can be interpreted no? In the case of unknown, what I've found most helpful is using something like https://github.com/viperproject/smt-scope. Create a log file with proof mode on, then use their website to interpret the logs and look at where the solver is spending most of its time.

Interested about this on_clause mechanism... haven't used it before