I came across the following small glitch. Running this code with 4.12.5:

from z3 import *
expr = AtMost(a, b, c, 1)
print(expr)
print(expr.sexpr())
print(simplify(expr))
print(simplify(expr).sexpr())

produces

AtMost((a, b, c), 1)
((_ at-most 1) a b c)
at-least(Not(a), Not(b), Not(c))
((_ at-least 2) (not a) (not b) (not c))

The two sexpr confirm that Z3 understands and simplifies the constraint correctly. The first output line (AtLeast((a,b,c),1)) uses syntax that is not supported by the API, which wants AtLeast(a,b,c,1) instead. The third line, uses a name (at-least) that is not in the API and does not print the threshold.

These are clearly not show stoppers, but I thought you'd want to know. Also, in the header comment of AtLeast in z3py.py, it says "Create an at-most Pseudo-Boolean constraint."