Function z3_sys::Z3_tactic_fail_if_not_decided

source · 
pub unsafe extern "C" fn Z3_tactic_fail_if_not_decided(
    c: Z3_context
) -> Z3_tactic
Expand description

Return a tactic that fails if the goal is not trivially satisfiable (i.e., empty) or trivially unsatisfiable (i.e., contains false).