diff --git a/src/api/java/AST.java b/src/api/java/AST.java
index 436a9fdcb..6b5493bf9 100644
--- a/src/api/java/AST.java
+++ b/src/api/java/AST.java
@@ -22,10 +22,8 @@ import com.microsoft.z3.enumerations.Z3_ast_kind;
 /**
  * The abstract syntax tree (AST) class.
  **/
-public class AST extends Z3Object
+public class AST extends Z3Object implements Comparable
 {
-    /* Overloaded operators are not translated. */
-
     /**
      * Object comparison.
      * 
@@ -35,7 +33,7 @@ public class AST extends Z3Object
     {
         AST casted = null;
 
-        try
+	try
         {
             casted = AST.class.cast(o);
         } catch (ClassCastException e)
@@ -43,8 +41,13 @@ public class AST extends Z3Object
             return false;
         }
 
-        return this.getNativeObject() == casted.getNativeObject();
-    }
+	return  
+	    (this == casted) || 
+	    (this != null) &&
+	    (casted != null) &&
+	    (getContext().nCtx() == casted.getContext().nCtx()) &&
+	    (Native.isEqAst(getContext().nCtx(), getNativeObject(), casted.getNativeObject()));
+}
 
     /**
      * Object Comparison. 
diff --git a/src/api/java/FuncDecl.java b/src/api/java/FuncDecl.java
index 28cdf2a2d..bc2baab91 100644
--- a/src/api/java/FuncDecl.java
+++ b/src/api/java/FuncDecl.java
@@ -26,22 +26,6 @@ import com.microsoft.z3.enumerations.Z3_parameter_kind;
  **/
 public class FuncDecl extends AST
 {
-    /**
-     * Comparison operator.
-     * 
-     * @return True if {@code a"/> and <paramref name="b} share the
-     *         same context and are equal, false otherwise.
-     **/
-    /* Overloaded operators are not translated. */
-
-    /**
-     * Comparison operator.
-     * 
-     * @return True if {@code a"/> and <paramref name="b} do not
-     *         share the same context or are not equal, false otherwise.
-     **/
-    /* Overloaded operators are not translated. */
-
     /**
      * Object comparison.
      **/
@@ -55,7 +39,12 @@ public class FuncDecl extends AST
             return false;
         }
 
-        return this.getNativeObject() == casted.getNativeObject();
+	return  
+	    (this == casted) || 
+	    (this != null) &&
+	    (casted != null) &&
+	    (getContext().nCtx() == casted.getContext().nCtx()) &&
+	    (Native.isEqFuncDecl(getContext().nCtx(), getNativeObject(), casted.getNativeObject()));
     }
 
     /**
diff --git a/src/api/java/Sort.java b/src/api/java/Sort.java
index b118a5dc2..db6bee80e 100644
--- a/src/api/java/Sort.java
+++ b/src/api/java/Sort.java
@@ -25,8 +25,6 @@ import com.microsoft.z3.enumerations.Z3_sort_kind;
  **/
 public class Sort extends AST
 {
-    /* Overloaded operators are not translated. */
-
     /**
      * Equality operator for objects of type Sort. 
      * @param o
@@ -42,7 +40,12 @@ public class Sort extends AST
             return false;
         }
 
-        return this.getNativeObject() == casted.getNativeObject();
+	return  
+	    (this == casted) || 
+	    (this != null) &&
+	    (casted != null) &&
+	    (getContext().nCtx() == casted.getContext().nCtx()) &&
+	    (Native.isEqSort(getContext().nCtx(), getNativeObject(), casted.getNativeObject()));
     }
 
     /**