diff --git a/src/api/go/z3.go b/src/api/go/z3.go
index 321870c0c..864b68691 100644
--- a/src/api/go/z3.go
+++ b/src/api/go/z3.go
@@ -414,6 +414,100 @@ func (c *Context) MkDistinct(exprs ...*Expr) *Expr {
 	return newExpr(c, C.Z3_mk_distinct(c.ptr, C.uint(len(exprs)), &cExprs[0]))
 }
 
+// Pseudo-Boolean / cardinality constraints
+
+// MkAtMost encodes p1 + p2 + ... + pn <= k.
+func (c *Context) MkAtMost(args []*Expr, k uint) *Expr {
+	cArgs := make([]C.Z3_ast, len(args))
+	for i, a := range args {
+		cArgs[i] = a.ptr
+	}
+	var cArgsPtr *C.Z3_ast
+	if len(cArgs) > 0 {
+		cArgsPtr = &cArgs[0]
+	}
+	return newExpr(c, C.Z3_mk_atmost(c.ptr, C.uint(len(args)), cArgsPtr, C.uint(k)))
+}
+
+// MkAtLeast encodes p1 + p2 + ... + pn >= k.
+func (c *Context) MkAtLeast(args []*Expr, k uint) *Expr {
+	cArgs := make([]C.Z3_ast, len(args))
+	for i, a := range args {
+		cArgs[i] = a.ptr
+	}
+	var cArgsPtr *C.Z3_ast
+	if len(cArgs) > 0 {
+		cArgsPtr = &cArgs[0]
+	}
+	return newExpr(c, C.Z3_mk_atleast(c.ptr, C.uint(len(args)), cArgsPtr, C.uint(k)))
+}
+
+// MkPBLe encodes k1*p1 + k2*p2 + ... + kn*pn <= k.
+func (c *Context) MkPBLe(args []*Expr, coeffs []int, k int) *Expr {
+	if len(args) != len(coeffs) {
+		panic("MkPBLe: args and coeffs must have the same length")
+	}
+	cArgs := make([]C.Z3_ast, len(args))
+	for i, a := range args {
+		cArgs[i] = a.ptr
+	}
+	cCoeffs := make([]C.int, len(coeffs))
+	for i, v := range coeffs {
+		cCoeffs[i] = C.int(v)
+	}
+	var cArgsPtr *C.Z3_ast
+	var cCoeffsPtr *C.int
+	if len(cArgs) > 0 {
+		cArgsPtr = &cArgs[0]
+		cCoeffsPtr = &cCoeffs[0]
+	}
+	return newExpr(c, C.Z3_mk_pble(c.ptr, C.uint(len(args)), cArgsPtr, cCoeffsPtr, C.int(k)))
+}
+
+// MkPBGe encodes k1*p1 + k2*p2 + ... + kn*pn >= k.
+func (c *Context) MkPBGe(args []*Expr, coeffs []int, k int) *Expr {
+	if len(args) != len(coeffs) {
+		panic("MkPBGe: args and coeffs must have the same length")
+	}
+	cArgs := make([]C.Z3_ast, len(args))
+	for i, a := range args {
+		cArgs[i] = a.ptr
+	}
+	cCoeffs := make([]C.int, len(coeffs))
+	for i, v := range coeffs {
+		cCoeffs[i] = C.int(v)
+	}
+	var cArgsPtr *C.Z3_ast
+	var cCoeffsPtr *C.int
+	if len(cArgs) > 0 {
+		cArgsPtr = &cArgs[0]
+		cCoeffsPtr = &cCoeffs[0]
+	}
+	return newExpr(c, C.Z3_mk_pbge(c.ptr, C.uint(len(args)), cArgsPtr, cCoeffsPtr, C.int(k)))
+}
+
+// MkPBEq encodes k1*p1 + k2*p2 + ... + kn*pn = k.
+func (c *Context) MkPBEq(args []*Expr, coeffs []int, k int) *Expr {
+	if len(args) != len(coeffs) {
+		panic("MkPBEq: args and coeffs must have the same length")
+	}
+	cArgs := make([]C.Z3_ast, len(args))
+	for i, a := range args {
+		cArgs[i] = a.ptr
+	}
+	cCoeffs := make([]C.int, len(coeffs))
+	for i, v := range coeffs {
+		cCoeffs[i] = C.int(v)
+	}
+	var cArgsPtr *C.Z3_ast
+	var cCoeffsPtr *C.int
+	if len(cArgs) > 0 {
+		cArgsPtr = &cArgs[0]
+		cCoeffsPtr = &cCoeffs[0]
+	}
+	return newExpr(c, C.Z3_mk_pbeq(c.ptr, C.uint(len(args)), cArgsPtr, cCoeffsPtr, C.int(k)))
+}
+
 // FuncDecl represents a function declaration.
 type FuncDecl struct {
 	ctx *Context
diff --git a/src/api/ml/z3.ml b/src/api/ml/z3.ml
index 74cf974b2..c8d42f22e 100644
--- a/src/api/ml/z3.ml
+++ b/src/api/ml/z3.ml
@@ -587,6 +587,12 @@ struct
   let mk_eq = Z3native.mk_eq
   let mk_distinct ctx args = Z3native.mk_distinct ctx (List.length args) args
 
+  let mk_atmost ctx args k = Z3native.mk_atmost ctx (List.length args) args k
+  let mk_atleast ctx args k = Z3native.mk_atleast ctx (List.length args) args k
+  let mk_pble ctx args coeffs k = Z3native.mk_pble ctx (List.length args) args coeffs k
+  let mk_pbge ctx args coeffs k = Z3native.mk_pbge ctx (List.length args) args coeffs k
+  let mk_pbeq ctx args coeffs k = Z3native.mk_pbeq ctx (List.length args) args coeffs k
+
   let get_bool_value x = lbool_of_int (Z3native.get_bool_value (gc x) x)
 
   let is_bool x =
diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli
index 689fa088d..6b5fe6410 100644
--- a/src/api/ml/z3.mli
+++ b/src/api/ml/z3.mli
@@ -632,6 +632,21 @@ sig
   (** Creates a [distinct] term. *)
   val mk_distinct : context -> Expr.expr list -> Expr.expr
 
+  (** Encodes p1 + p2 + ... + pn <= k. *)
+  val mk_atmost : context -> Expr.expr list -> int -> Expr.expr
+
+  (** Encodes p1 + p2 + ... + pn >= k. *)
+  val mk_atleast : context -> Expr.expr list -> int -> Expr.expr
+
+  (** Encodes k1*p1 + k2*p2 + ... + kn*pn <= k. *)
+  val mk_pble : context -> Expr.expr list -> int list -> int -> Expr.expr
+
+  (** Encodes k1*p1 + k2*p2 + ... + kn*pn >= k. *)
+  val mk_pbge : context -> Expr.expr list -> int list -> int -> Expr.expr
+
+  (** Encodes k1*p1 + k2*p2 + ... + kn*pn = k. *)
+  val mk_pbeq : context -> Expr.expr list -> int list -> int -> Expr.expr
+
   (** Indicates whether the expression is the true or false expression
       or something else (L_UNDEF). *)
   val get_bool_value : Expr.expr -> Z3enums.lbool