Function z3_sys::Z3_model_get_const_interp

pub unsafe extern "C" fn Z3_model_get_const_interp(
    c: Z3_context, 
    m: Z3_model, 
    a: Z3_func_decl
) -> Z3_ast

Return the interpretation (i.e., assignment) of constant a in the model m.

Return NULL, if the model does not assign an interpretation for a. That should be interpreted as: the value of a does not matter.

Precondition: Z3_get_arity(c, a) == 0