diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index a7f1259a0..6af38cb82 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -637,10 +637,6 @@ namespace z3 {
             Z3_func_decl tc = Z3_mk_transitive_closure(ctx(), *this); check_error(); return func_decl(ctx(), tc); 
         }
 
-        func_decl transitive_reflexive_closure(func_decl const& f) {
-            Z3_func_decl tc = Z3_mk_transitive_reflexive_closure(ctx(), *this); check_error(); return func_decl(ctx(), tc); 
-        }
-
         bool is_const() const { return arity() == 0; }
 
         expr operator()() const;
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 485107e44..6d6220fb5 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -10403,9 +10403,3 @@ def TransitiveClosure(f):
     """
     return FuncDeclRef(Z3_mk_transitive_closure(f.ctx_ref(), f.ast), f.ctx)
 
-def TransitiveReflexiveClosure(f):
-    """Given a binary relation R, such that the two arguments have the same sort
-    create the transitive reflexive closure relation R*.
-    The transitive reflexive closure R* is a new relation.
-    """
-    return FuncDeclRef(Z3_mk_transitive_reflexive_closure(f.ctx_ref(), f.ast), f.ctx)