diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index c918533ca..23d4e3e6c 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -7337,7 +7337,7 @@ def PbLe(args, k):
     _args, sz = _to_ast_array(args)
     _coeffs = (ctypes.c_int * len(coeffs))()
     for i in range(len(coeffs)):
-	_coeffs[i] = coeffs[i]
+        _coeffs[i] = coeffs[i]
     return BoolRef(Z3_mk_pble(ctx.ref(), sz, _args, _coeffs, k), ctx)
 
 
diff --git a/src/api/python/z3printer.py b/src/api/python/z3printer.py
index b4b83dc2b..e8a6b992f 100644
--- a/src/api/python/z3printer.py
+++ b/src/api/python/z3printer.py
@@ -843,16 +843,16 @@ class Formatter:
         return seq1(self.pp_name(a), [ self.pp_sort(a.domain()), self.pp_expr(a.arg(0), d+1, xs) ])
 
     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)])
+        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))
-	k   = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 0)
-	ks = [Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, i+1) for i in rchs]
-	ls = [ seq3([self.pp_expr(chs[i], d+1,xs), to_format(ks[i])]) for i in rchs]
-	return seq1(self.pp_name(a), [seq3(ls), to_format(k)])
+        chs = a.children()
+        rchs = range(len(chs))
+        k   = Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, 0)
+        ks = [Z3_get_decl_int_parameter(a.ctx_ref(), a.decl().ast, i+1) for i in rchs]
+        ls = [ seq3([self.pp_expr(chs[i], d+1,xs), to_format(ks[i])]) for i in rchs]
+        return seq1(self.pp_name(a), [seq3(ls), to_format(k)])
 
 
     def pp_app(self, a, d, xs):
@@ -889,12 +889,12 @@ class Formatter:
                 return self.pp_map(a, d, xs)
             elif k == Z3_OP_CONST_ARRAY:
                 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_LE:
-		return self.pp_pbcmp(a, d, f, xs)
-	    elif k == Z3_OP_PB_GE:
-		return self.pp_pbcmp(a, d, f, xs)
+            elif k == Z3_OP_PB_AT_MOST:
+                return self.pp_atmost(a, d, f, xs)
+            elif k == Z3_OP_PB_LE:
+                return self.pp_pbcmp(a, d, f, xs)
+            elif k == Z3_OP_PB_GE:
+                return self.pp_pbcmp(a, d, f, xs)
             elif z3.is_pattern(a):
                 return self.pp_pattern(a, d, xs)
             elif self.is_infix(k):