Function z3_sys::Z3_mk_quantifier_const_ex

pub unsafe extern "C" fn Z3_mk_quantifier_const_ex(
    c: Z3_context,
    is_forall: Z3_bool,
    weight: c_uint,
    quantifier_id: Z3_symbol,
    skolem_id: Z3_symbol,
    num_bound: c_uint,
    bound: *const Z3_app,
    num_patterns: c_uint,
    patterns: *const Z3_pattern,
    num_no_patterns: c_uint,
    no_patterns: *const Z3_ast,
    body: Z3_ast
) -> Z3_ast

Create a universal or existential quantifier using a list of constants that will form the set of bound variables.