Function at_most 

pub fn at_most(vars: &[ProofExpr], k: usize, aux: &str) -> ProofExpr

“At most k of vars are true.” Auxiliary atoms are named {aux}_{i}_{j}, so distinct constraints in one formula must use distinct aux prefixes.