diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java
index 8efa977c4..181055b03 100644
--- a/src/api/java/Solver.java
+++ b/src/api/java/Solver.java
@@ -472,7 +472,7 @@ public class Solver extends Z3Object {
      * @return The root expression of the congruence class
      * @throws Z3Exception
      **/
-    public Expr<?> getCongruenceRoot(Expr<?> t)
+    public Expr<?> congruenceRoot(Expr<?> t)
     {
         getContext().checkContextMatch(t);
         return Expr.create(getContext(),
@@ -487,7 +487,7 @@ public class Solver extends Z3Object {
      * @return The next expression in the congruence class
      * @throws Z3Exception
      **/
-    public Expr<?> getCongruenceNext(Expr<?> t)
+    public Expr<?> congruenceNext(Expr<?> t)
     {
         getContext().checkContextMatch(t);
         return Expr.create(getContext(),
@@ -502,7 +502,7 @@ public class Solver extends Z3Object {
      * @return An expression explaining the congruence between a and b
      * @throws Z3Exception
      **/
-    public Expr<?> getCongruenceExplain(Expr<?> a, Expr<?> b)
+    public Expr<?> congruenceExplain(Expr<?> a, Expr<?> b)
     {
         getContext().checkContextMatch(a);
         getContext().checkContextMatch(b);
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 9438af21f..6582c2a26 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -7777,7 +7777,7 @@ class Solver(Z3PPObject):
         cube are likely more useful to cube on."""
         return self.cube_vs
 
-    def root(self, t):
+    def congruence_root(self, t):
         """Retrieve congruence closure root of the term t relative to the current search state
         The function primarily works for SimpleSolver. Terms and variables that are
         eliminated during pre-processing are not visible to the congruence closure.
@@ -7785,7 +7785,7 @@ class Solver(Z3PPObject):
         t = _py2expr(t, self.ctx)
         return _to_expr_ref(Z3_solver_congruence_root(self.ctx.ref(), self.solver, t.ast), self.ctx)
 
-    def next(self, t):
+    def congruence_next(self, t):
         """Retrieve congruence closure sibling of the term t relative to the current search state
         The function primarily works for SimpleSolver. Terms and variables that are
         eliminated during pre-processing are not visible to the congruence closure.
@@ -7793,7 +7793,7 @@ class Solver(Z3PPObject):
         t = _py2expr(t, self.ctx)
         return _to_expr_ref(Z3_solver_congruence_next(self.ctx.ref(), self.solver, t.ast), self.ctx)
 
-    def explain_congruent(self, a, b):
+    def congruence_explain(self, a, b):
         """Explain congruence of a and b relative to the current search state"""
         a = _py2expr(a, self.ctx)
         b = _py2expr(b, self.ctx)