Are there any ways to "catch" the error of Z3_mk_model?

[LEAFERx]

Currently when calling Solver::get_model() without Solver::check() (or Solver::check_assumption) first or with Solver::check() returning UnSat, the process will just print out an error message and then exit, leaving users no room to do any error handling. Are there any workarounds to fix this?

For one workaround I can think of without handling the exception at the boundary of FFI, maybe we can maintain a status in Solver, like

enum SolverStatus {
  UnCheckedOrUnSat,
  Checked
}

And Solver::get_model() would return a Result<Model, [Some Error]> instead of just letting the process exits.