diff --git a/src/api/dotnet/Optimize.cs b/src/api/dotnet/Optimize.cs
index 9d0636425..29e5e869a 100644
--- a/src/api/dotnet/Optimize.cs
+++ b/src/api/dotnet/Optimize.cs
@@ -124,7 +124,7 @@ namespace Microsoft.Z3
             /// <summary>
             /// Retrieve a lower bound for the objective handle.
             /// </summary>                   
-            public ArithExpr Lower
+            public Expr Lower
             {
                 get { return opt.GetLower(handle); }
             }
@@ -132,7 +132,7 @@ namespace Microsoft.Z3
             /// <summary>
             /// Retrieve an upper bound for the objective handle.
             /// </summary>                   
-            public ArithExpr Upper
+            public Expr Upper
             {
                 get { return opt.GetUpper(handle); }
             }
@@ -140,7 +140,7 @@ namespace Microsoft.Z3
             /// <summary>
             /// Retrieve the value of an objective.
             /// </summary>                   
-            public ArithExpr Value
+            public Expr Value
             {
                 get { return Lower; }
             }
@@ -148,7 +148,7 @@ namespace Microsoft.Z3
             /// <summary>
             /// Retrieve a lower bound for the objective handle.
             /// </summary>                   
-            public ArithExpr[] LowerAsVector
+            public Expr[] LowerAsVector
             {
                 get { return opt.GetLowerAsVector(handle); }
             }
@@ -156,7 +156,7 @@ namespace Microsoft.Z3
             /// <summary>
             /// Retrieve an upper bound for the objective handle.
             /// </summary>                   
-            public ArithExpr[] UpperAsVector
+            public Expr[] UpperAsVector
             {
                 get { return opt.GetUpperAsVector(handle); }
             }
@@ -240,8 +240,9 @@ namespace Microsoft.Z3
         /// Declare an arithmetical maximization objective.
         /// Return a handle to the objective. The handle is used as
         /// to retrieve the values of objectives after calling Check.
+        /// The expression can be either an arithmetical expression or bit-vector.
         /// </summary>            
-        public Handle MkMaximize(ArithExpr e)
+        public Handle MkMaximize(Expr e)
         {
             return new Handle(this, Native.Z3_optimize_maximize(Context.nCtx, NativeObject, e.NativeObject));
         }
@@ -250,45 +251,46 @@ namespace Microsoft.Z3
         /// Declare an arithmetical minimization objective. 
         /// Similar to MkMaximize.
         /// </summary>            
-        public Handle MkMinimize(ArithExpr e)
+        public Handle MkMinimize(Expr e)
         {
             return new Handle(this, Native.Z3_optimize_minimize(Context.nCtx, NativeObject, e.NativeObject));
         }
 
+
         /// <summary>
         /// Retrieve a lower bound for the objective handle.
         /// </summary>            
-        private ArithExpr GetLower(uint index)
+        private Expr GetLower(uint index)
         {
-            return (ArithExpr)Expr.Create(Context, Native.Z3_optimize_get_lower(Context.nCtx, NativeObject, index));
+            return Expr.Create(Context, Native.Z3_optimize_get_lower(Context.nCtx, NativeObject, index));
         }
 
 
         /// <summary>
         /// Retrieve an upper bound for the objective handle.
         /// </summary>            
-        private ArithExpr GetUpper(uint index)
+        private Expr GetUpper(uint index)
         {
-            return (ArithExpr)Expr.Create(Context, Native.Z3_optimize_get_upper(Context.nCtx, NativeObject, index));
+            return Expr.Create(Context, Native.Z3_optimize_get_upper(Context.nCtx, NativeObject, index));
         }
 
         /// <summary>
         /// Retrieve a lower bound for the objective handle.
         /// </summary>            
-        private ArithExpr[] GetLowerAsVector(uint index)
+        private Expr[] GetLowerAsVector(uint index)
         {
             ASTVector v = new ASTVector(Context, Native.Z3_optimize_get_lower_as_vector(Context.nCtx, NativeObject, index));
-            return v.ToArithExprArray();
+            return v.ToExprArray();
         }
 
 
         /// <summary>
         /// Retrieve an upper bound for the objective handle.
         /// </summary>            
-        private ArithExpr[] GetUpperAsVector(uint index)
+        private Expr[] GetUpperAsVector(uint index)
         {
             ASTVector v = new ASTVector(Context, Native.Z3_optimize_get_upper_as_vector(Context.nCtx, NativeObject, index));
-            return v.ToArithExprArray();
+            return v.ToExprArray();
         }
 
     /// <summary>
diff --git a/src/api/java/Optimize.java b/src/api/java/Optimize.java
index 3edbff73e..a434b6e9f 100644
--- a/src/api/java/Optimize.java
+++ b/src/api/java/Optimize.java
@@ -89,7 +89,7 @@ public class Optimize extends Z3Object {
         /**
          * Retrieve a lower bound for the objective handle.
          **/
-        public ArithExpr getLower()
+        public Expr getLower()
         {
             return opt.GetLower(handle);
         }
@@ -97,7 +97,7 @@ public class Optimize extends Z3Object {
         /**
          * Retrieve an upper bound for the objective handle.
          **/
-        public ArithExpr getUpper()
+        public Expr getUpper()
         {
             return opt.GetUpper(handle);
         }
@@ -110,7 +110,7 @@ public class Optimize extends Z3Object {
          * and otherwise is represented by the expression {@code value + eps * EPSILON},
          * where {@code EPSILON} is an arbitrarily small real number.
          */
-        public ArithExpr[] getUpperAsVector()
+        public Expr[] getUpperAsVector()
         {
             return opt.GetUpperAsVector(handle);
         }
@@ -120,7 +120,7 @@ public class Optimize extends Z3Object {
          *
          * <p>See {@link #getUpperAsVector()} for triple semantics.
          */
-        public ArithExpr[] getLowerAsVector()
+        public Expr[] getLowerAsVector()
         {
             return opt.GetLowerAsVector(handle);
         }
@@ -128,7 +128,7 @@ public class Optimize extends Z3Object {
         /**
          * Retrieve the value of an objective.
          **/
-        public ArithExpr getValue()
+        public Expr getValue()
         {
             return getLower();
         }
@@ -214,7 +214,7 @@ public class Optimize extends Z3Object {
      *  Return a handle to the objective. The handle is used as
      *  to retrieve the values of objectives after calling Check.
      **/            
-    public Handle MkMaximize(ArithExpr e)
+    public Handle MkMaximize(Expr e)
     {
         return new Handle(this, Native.optimizeMaximize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
     }
@@ -223,7 +223,7 @@ public class Optimize extends Z3Object {
      *  Declare an arithmetical minimization objective. 
      *  Similar to MkMaximize.
      **/
-    public Handle MkMinimize(ArithExpr e)
+    public Handle MkMinimize(Expr e)
     {
         return new Handle(this, Native.optimizeMinimize(getContext().nCtx(), getNativeObject(), e.getNativeObject()));
     }
@@ -231,17 +231,17 @@ public class Optimize extends Z3Object {
     /**
      *  Retrieve a lower bound for the objective handle.
      **/
-    private ArithExpr GetLower(int index)
+    private Expr GetLower(int index)
     {
-        return (ArithExpr)Expr.create(getContext(), Native.optimizeGetLower(getContext().nCtx(), getNativeObject(), index));
+        return Expr.create(getContext(), Native.optimizeGetLower(getContext().nCtx(), getNativeObject(), index));
     }
 
     /**
      *  Retrieve an upper bound for the objective handle.
      **/
-    private ArithExpr GetUpper(int index)
+    private Expr GetUpper(int index)
     {
-        return (ArithExpr)Expr.create(getContext(), Native.optimizeGetUpper(getContext().nCtx(), getNativeObject(), index));
+        return Expr.create(getContext(), Native.optimizeGetUpper(getContext().nCtx(), getNativeObject(), index));
     }
 
     /**
@@ -249,7 +249,7 @@ public class Optimize extends Z3Object {
      *
      * <p>See {@link Handle#getUpperAsVector}.
      */
-    private ArithExpr[] GetUpperAsVector(int index) {
+    private Expr[] GetUpperAsVector(int index) {
         return unpackObjectiveValueVector(
                 Native.optimizeGetUpperAsVector(
                         getContext().nCtx(), getNativeObject(), index
@@ -262,7 +262,7 @@ public class Optimize extends Z3Object {
      *
      * <p>See {@link Handle#getLowerAsVector}.
      */
-    private ArithExpr[] GetLowerAsVector(int index) {
+    private Expr[] GetLowerAsVector(int index) {
         return unpackObjectiveValueVector(
                 Native.optimizeGetLowerAsVector(
                         getContext().nCtx(), getNativeObject(), index
@@ -270,12 +270,12 @@ public class Optimize extends Z3Object {
         );
     }
 
-    private ArithExpr[] unpackObjectiveValueVector(long nativeVec) {
+    private Expr[] unpackObjectiveValueVector(long nativeVec) {
         ASTVector vec = new ASTVector(
                 getContext(), nativeVec
         );
-        return new ArithExpr[] {
-                (ArithExpr) vec.get(0), (ArithExpr) vec.get(1), (ArithExpr) vec.get(2)
+        return new Expr[] {
+                (Expr) vec.get(0), (Expr) vec.get(1), (Expr) vec.get(2)
         };
 
     }