In the attached test script, I created two solvers in different contexts, one with set_param(proof=True) and one without. I wanted to verify that one solver would be able to produce proofs and the other wouldn't. That seems to be the case. However, when I try to print the proof for the solver that is not supposed to have it, CPython segfaults instead of raising an exception as it normally does.

This is with z3 4.15.2 and CPython 3.13.3 on Ubuntu 25.04. It's not a show stopper, but I thought you'd like to know.

contexts.zip