z3_sys
pub unsafe extern "C" fn Z3_mk_pble( c: Z3_context, num_args: c_uint, args: *const Z3_ast, coeffs: *const c_int, k: c_int) -> Z3_ast
Pseudo-Boolean relations.
Encode k1p1 + k2p2 + ... + kn*pn <= k