I don't know if there is an issue or I am using the API incorrectly, but I'm having trouble with Z3_goal_convert_model when giving it a NULL model. I could be misunderstanding the API docs:

Convert a model of the formulas of a goal to a model of an original goal.
The model may be null, in which case the returned model is valid if the goal was
established satisfiable.

To be concrete, consider the attached program test_convert_model.c.txt (with extra .txt to appease github). This program sets up a small instance and calls Z3_goal_convert_model in a way that makes Z3 unhappy, see the comment pointing to the call that crashes.