Function z3_sys::Z3_mk_probe

pub unsafe extern "C" fn Z3_mk_probe(c: Z3_context, name: Z3_string) -> Z3_probe

Return a probe associated with the given name. The complete list of probes may be obtained using the procedures Z3_get_num_probes and Z3_get_probe_name. It may also be obtained using the command (help-tactic) in the SMT 2.0 front-end.

Probes are used to inspect a goal (aka problem) and collect information that may be used to decide which solver and/or preprocessing step will be used.