Function Z3_mk_model 

pub unsafe extern "C" fn Z3_mk_model(
    c: Z3_context,
) -> Option<Z3_model>

Create a fresh model object. It has reference count 0.