diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index 851e8e243..db629cd2d 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -6166,7 +6166,7 @@ class Fixedpoint(Z3PPObject):
             Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, head.as_ast(), name)            
         else:
             body = _get_args(body)
-            f    = self.abstract(Implies(And(body),head))
+            f    = self.abstract(Implies(And(body, self.ctx),head))
             Z3_fixedpoint_add_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
         
     def rule(self, head, body = None, name = None):
@@ -6194,7 +6194,7 @@ class Fixedpoint(Z3PPObject):
             if sz == 1:
                 query = query[0]
             else:
-                query = And(query)
+                query = And(query, self.ctx)
             query = self.abstract(query, False)
             r = Z3_fixedpoint_query(self.ctx.ref(), self.fixedpoint, query.as_ast())
         return CheckSatResult(r)
@@ -6213,7 +6213,7 @@ class Fixedpoint(Z3PPObject):
             name = ""
         name = to_symbol(name, self.ctx)
         body = _get_args(body)
-        f    = self.abstract(Implies(And(body),head))
+        f    = self.abstract(Implies(And(body, self.ctx),head))
         Z3_fixedpoint_update_rule(self.ctx.ref(), self.fixedpoint, f.as_ast(), name)
 
     def get_answer(self):