pub unsafe extern "C" fn Z3_fixedpoint_get_reachable(
    c: Z3_context,
    d: Z3_fixedpoint,
    pred: Z3_func_decl
) -> Z3_ast
Expand description

Retrieve reachable states of a predicate.

Note: this functionality is Spacer specific.