fix #7105

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/api/python/z3/z3.py

@@ -9069,7 +9069,7 @@ def AtMost(*args):
 
 
 def AtLeast(*args):
-    """Create an at-most Pseudo-Boolean k constraint.
+    """Create an at-least Pseudo-Boolean k constraint.
 
     >>> a, b, c = Bools('a b c')
     >>> f = AtLeast(a, b, c, 2)

src/api/python/z3/z3printer.py

@@ -99,6 +99,7 @@ def _z3_assert(cond, msg):
     Z3_OP_ARRAY_EXT: "Ext",
 
     Z3_OP_PB_AT_MOST: "AtMost",
+    Z3_OP_PB_AT_LEAST: "AtLeast",
     Z3_OP_PB_LE: "PbLe",
     Z3_OP_PB_GE: "PbGe",
     Z3_OP_PB_EQ: "PbEq",
@@ -1111,6 +1112,10 @@ def pp_atmost(self, a, d, f, xs):
         k = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 0)
         return seq1(self.pp_name(a), [seq3([self.pp_expr(ch, d + 1, xs) for ch in a.children()]), to_format(k)])
 
+    def pp_atleast(self, a, d, f, xs):
+        k = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 0)
+        return seq1(self.pp_name(a), [seq3([self.pp_expr(ch, d + 1, xs) for ch in a.children()]), to_format(k)])
+
     def pp_pbcmp(self, a, d, f, xs):
         chs = a.children()
         rchs = range(len(chs))
@@ -1163,6 +1168,8 @@ def pp_app(self, a, d, xs):
                 return self.pp_K(a, d, xs)
             elif k == Z3_OP_PB_AT_MOST:
                 return self.pp_atmost(a, d, f, xs)
+            elif k == Z3_OP_PB_AT_LEAST:
+                return self.pp_atleast(a, d, f, xs)
             elif k == Z3_OP_PB_LE:
                 return self.pp_pbcmp(a, d, f, xs)
             elif k == Z3_OP_PB_GE: