diff --git a/src/api/dotnet/ASTVector.cs b/src/api/dotnet/ASTVector.cs
index f858c7862..8b599ca48 100644
--- a/src/api/dotnet/ASTVector.cs
+++ b/src/api/dotnet/ASTVector.cs
@@ -112,7 +112,7 @@ namespace Microsoft.Z3
         }
 
         /// <summary>
-        /// Translates an AST vector into an Expr[]
+        /// Translates an ASTVector into an Expr[]
         /// </summary>    
         public Expr[] ToExprArray()
         {
@@ -123,6 +123,114 @@ namespace Microsoft.Z3
             return res;
         }
 
+        /// <summary>
+        /// Translates an ASTVector into a BoolExpr[]
+        /// </summary>    
+        public BoolExpr[] ToBoolExprArray()
+        {
+            uint n = Size;
+            BoolExpr[] res = new BoolExpr[n];
+            for (uint i = 0; i < n; i++)
+                res[i] = (BoolExpr) Expr.Create(this.Context, this[i].NativeObject);
+            return res;
+        }
+
+        /// <summary>
+        /// Translates an ASTVector into a BitVecExpr[]
+        /// </summary>    
+        public BitVecExpr[] ToBitVecExprArray()
+        {
+            uint n = Size;
+            BitVecExpr[] res = new BitVecExpr[n];
+            for (uint i = 0; i < n; i++)
+                res[i] = (BitVecExpr)Expr.Create(this.Context, this[i].NativeObject);
+            return res;
+        }
+
+        /// <summary>
+        /// Translates an ASTVector into a ArithExpr[]
+        /// </summary>    
+        public ArithExpr[] ToArithExprArray()
+        {
+            uint n = Size;
+            ArithExpr[] res = new ArithExpr[n];
+            for (uint i = 0; i < n; i++)
+                res[i] = (ArithExpr)Expr.Create(this.Context, this[i].NativeObject);
+            return res;
+        }
+
+        /// <summary>
+        /// Translates an ASTVector into a ArrayExpr[]
+        /// </summary>    
+        public ArrayExpr[] ToArrayExprArray()
+        {
+            uint n = Size;
+            ArrayExpr[] res = new ArrayExpr[n];
+            for (uint i = 0; i < n; i++)
+                res[i] = (ArrayExpr)Expr.Create(this.Context, this[i].NativeObject);
+            return res;
+        }
+
+        /// <summary>
+        /// Translates an ASTVector into a DatatypeExpr[]
+        /// </summary>    
+        public DatatypeExpr[] ToDatatypeExprArray()
+        {
+            uint n = Size;
+            DatatypeExpr[] res = new DatatypeExpr[n];
+            for (uint i = 0; i < n; i++)
+                res[i] = (DatatypeExpr)Expr.Create(this.Context, this[i].NativeObject);
+            return res;
+        }
+
+        /// <summary>
+        /// Translates an ASTVector into a FPExpr[]
+        /// </summary>    
+        public FPExpr[] ToFPExprArray()
+        {
+            uint n = Size;
+            FPExpr[] res = new FPExpr[n];
+            for (uint i = 0; i < n; i++)
+                res[i] = (FPExpr)Expr.Create(this.Context, this[i].NativeObject);
+            return res;
+        }
+
+        /// <summary>
+        /// Translates an ASTVector into a FPRMExpr[]
+        /// </summary>    
+        public FPRMExpr[] ToFPRMExprArray()
+        {
+            uint n = Size;
+            FPRMExpr[] res = new FPRMExpr[n];
+            for (uint i = 0; i < n; i++)
+                res[i] = (FPRMExpr)Expr.Create(this.Context, this[i].NativeObject);
+            return res;
+        }
+
+        /// <summary>
+        /// Translates an ASTVector into a IntExpr[]
+        /// </summary>    
+        public IntExpr[] ToIntExprArray()
+        {
+            uint n = Size;
+            IntExpr[] res = new IntExpr[n];
+            for (uint i = 0; i < n; i++)
+                res[i] = (IntExpr)Expr.Create(this.Context, this[i].NativeObject);
+            return res;
+        }
+
+        /// <summary>
+        /// Translates an ASTVector into a RealExpr[]
+        /// </summary>    
+        public RealExpr[] ToRealExprArray()
+        {
+            uint n = Size;
+            RealExpr[] res = new RealExpr[n];
+            for (uint i = 0; i < n; i++)
+                res[i] = (RealExpr)Expr.Create(this.Context, this[i].NativeObject);
+            return res;
+        }
+
         #region Internal
         internal ASTVector(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
         internal ASTVector(Context ctx) : base(ctx, Native.Z3_mk_ast_vector(ctx.nCtx)) { Contract.Requires(ctx != null); }
diff --git a/src/api/dotnet/Fixedpoint.cs b/src/api/dotnet/Fixedpoint.cs
index 54dbcd3c1..66449ddbb 100644
--- a/src/api/dotnet/Fixedpoint.cs
+++ b/src/api/dotnet/Fixedpoint.cs
@@ -279,7 +279,7 @@ namespace Microsoft.Z3
                 Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
 
                 ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_get_rules(Context.nCtx, NativeObject));
-                return (BoolExpr[])av.ToExprArray();
+                return av.ToBoolExprArray();
             }
         }
 
@@ -293,7 +293,7 @@ namespace Microsoft.Z3
                 Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
 
                 ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_get_assertions(Context.nCtx, NativeObject));
-                return (BoolExpr[])av.ToExprArray();
+                return av.ToBoolExprArray();
             }
         }
 
@@ -318,7 +318,7 @@ namespace Microsoft.Z3
         public BoolExpr[] ParseFile(string file)
         {
             ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_from_file(Context.nCtx, NativeObject, file));
-            return (BoolExpr[])av.ToExprArray();
+            return av.ToBoolExprArray();
         }
 
         /// <summary>
@@ -327,7 +327,7 @@ namespace Microsoft.Z3
         public BoolExpr[] ParseString(string s)
         {
             ASTVector av = new ASTVector(Context, Native.Z3_fixedpoint_from_string(Context.nCtx, NativeObject, s));
-            return (BoolExpr[])av.ToExprArray();
+            return av.ToBoolExprArray();
         }
 
 
diff --git a/src/api/dotnet/InterpolationContext.cs b/src/api/dotnet/InterpolationContext.cs
index 9fbdf456e..e6e258b9a 100644
--- a/src/api/dotnet/InterpolationContext.cs
+++ b/src/api/dotnet/InterpolationContext.cs
@@ -47,7 +47,7 @@ namespace Microsoft.Z3
         /// <remarks>For more information on interpolation please refer
         /// too the function Z3_get_interpolant in the C/C++ API, which is 
         /// well documented.</remarks>
-        public Expr[] GetInterpolant(Expr pf, Expr pat, Params p)
+        public BoolExpr[] GetInterpolant(Expr pf, Expr pat, Params p)
         {
             Contract.Requires(pf != null);
             Contract.Requires(pat != null);
@@ -59,7 +59,7 @@ namespace Microsoft.Z3
             CheckContextMatch(p);
 
             ASTVector seq = new ASTVector(this, Native.Z3_get_interpolant(nCtx, pf.NativeObject, pat.NativeObject, p.NativeObject));
-            return seq.ToExprArray();
+            return seq.ToBoolExprArray();
         }
 
         /// <summary> 
@@ -68,7 +68,7 @@ namespace Microsoft.Z3
         /// <remarks>For more information on interpolation please refer
         /// too the function Z3_compute_interpolant in the C/C++ API, which is 
         /// well documented.</remarks>
-        public Z3_lbool ComputeInterpolant(Expr pat, Params p, out Expr[] interp, out Model model)
+        public Z3_lbool ComputeInterpolant(Expr pat, Params p, out BoolExpr[] interp, out Model model)
         {
             Contract.Requires(pat != null);
             Contract.Requires(p != null);
@@ -80,7 +80,7 @@ namespace Microsoft.Z3
 
             IntPtr i = IntPtr.Zero, m = IntPtr.Zero;
             int r = Native.Z3_compute_interpolant(nCtx, pat.NativeObject, p.NativeObject, ref i, ref m);
-            interp = new ASTVector(this, i).ToExprArray();
+            interp = new ASTVector(this, i).ToBoolExprArray();
             model = new Model(this, m);
             return (Z3_lbool)r;
         }
@@ -102,7 +102,7 @@ namespace Microsoft.Z3
         /// <remarks>For more information on interpolation please refer
         /// too the function Z3_check_interpolant in the C/C++ API, which is 
         /// well documented.</remarks>
-        public int CheckInterpolant(Expr[] cnsts, uint[] parents, Expr[] interps, out string error, Expr[] theory)
+        public int CheckInterpolant(Expr[] cnsts, uint[] parents, BoolExpr[] interps, out string error, Expr[] theory)
         {
             Contract.Requires(cnsts.Length == parents.Length);
             Contract.Requires(cnsts.Length == interps.Length + 1);
diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs
index c5227d18f..80ca7a0cd 100644
--- a/src/api/dotnet/Solver.cs
+++ b/src/api/dotnet/Solver.cs
@@ -193,7 +193,7 @@ namespace Microsoft.Z3
                 Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
 
                 ASTVector assertions = new ASTVector(Context, Native.Z3_solver_get_assertions(Context.nCtx, NativeObject));
-                return (BoolExpr[])assertions.ToExprArray();
+                return assertions.ToBoolExprArray();
             }
         }
 
@@ -273,7 +273,7 @@ namespace Microsoft.Z3
                 Contract.Ensures(Contract.Result<Expr[]>() != null);
 
                 ASTVector core = new ASTVector(Context, Native.Z3_solver_get_unsat_core(Context.nCtx, NativeObject));                
-                return (BoolExpr[])core.ToExprArray();
+                return core.ToBoolExprArray();
             }
         }
 
diff --git a/src/api/java/ASTVector.java b/src/api/java/ASTVector.java
index 7011eeb50..5b57db9d9 100644
--- a/src/api/java/ASTVector.java
+++ b/src/api/java/ASTVector.java
@@ -142,4 +142,112 @@ public class ASTVector extends Z3Object
             res[i] = Expr.create(getContext(), get(i).getNativeObject());
         return res;	
     }
-}
+
+    /**
+     * Translates the AST vector into an BoolExpr[]
+     * */  
+    public BoolExpr[] ToBoolExprArray()
+    {
+        int n = size();
+        BoolExpr[] res = new BoolExpr[n];
+        for (int i = 0; i < n; i++)
+            res[i] = (BoolExpr) Expr.create(getContext(), get(i).getNativeObject());
+        return res;
+    }
+
+    /**
+     * Translates the AST vector into an BitVecExpr[]
+     * */    
+    public BitVecExpr[] ToBitVecExprArray()
+    {
+        int n = size();
+        BitVecExpr[] res = new BitVecExpr[n];
+        for (int i = 0; i < n; i++)
+            res[i] = (BitVecExpr)Expr.create(getContext(), get(i).getNativeObject());
+        return res;
+    }
+
+    /**
+     * Translates the AST vector into an ArithExpr[]
+     * */   
+    public ArithExpr[] ToArithExprExprArray()
+    {
+        int n = size();
+        ArithExpr[] res = new ArithExpr[n];
+        for (int i = 0; i < n; i++)
+            res[i] = (ArithExpr)Expr.create(getContext(), get(i).getNativeObject());
+        return res;
+    }
+
+    /**
+     * Translates the AST vector into an ArrayExpr[]
+     * */  
+    public ArrayExpr[] ToArrayExprArray()
+    {
+        int n = size();
+        ArrayExpr[] res = new ArrayExpr[n];
+        for (int i = 0; i < n; i++)
+            res[i] = (ArrayExpr)Expr.create(getContext(), get(i).getNativeObject());
+        return res;
+    }
+
+    /**
+     * Translates the AST vector into an DatatypeExpr[]
+     * */ 
+    public DatatypeExpr[] ToDatatypeExprArray()
+    {
+        int n = size();
+        DatatypeExpr[] res = new DatatypeExpr[n];
+        for (int i = 0; i < n; i++)
+            res[i] = (DatatypeExpr)Expr.create(getContext(), get(i).getNativeObject());
+        return res;
+    }
+
+    /**
+     * Translates the AST vector into an FPExpr[]
+     * */   
+    public FPExpr[] ToFPExprArray()
+    {
+        int n = size();
+        FPExpr[] res = new FPExpr[n];
+        for (int i = 0; i < n; i++)
+            res[i] = (FPExpr)Expr.create(getContext(), get(i).getNativeObject());
+        return res;
+    }
+
+    /**
+     * Translates the AST vector into an FPRMExpr[]
+     * */
+    public FPRMExpr[] ToFPRMExprArray()
+    {
+        int n = size();
+        FPRMExpr[] res = new FPRMExpr[n];
+        for (int i = 0; i < n; i++)
+            res[i] = (FPRMExpr)Expr.create(getContext(), get(i).getNativeObject());
+        return res;
+    }
+
+    /**
+     * Translates the AST vector into an IntExpr[]
+     * */ 
+    public IntExpr[] ToIntExprArray()
+    {
+        int n = size();
+        IntExpr[] res = new IntExpr[n];
+        for (int i = 0; i < n; i++)
+            res[i] = (IntExpr)Expr.create(getContext(), get(i).getNativeObject());
+        return res;
+    }
+
+    /**
+     * Translates the AST vector into an RealExpr[]
+     * */   
+    public RealExpr[] ToRealExprArray()
+    {
+        int n = size();
+        RealExpr[] res = new RealExpr[n];
+        for (int i = 0; i < n; i++)
+            res[i] = (RealExpr)Expr.create(getContext(), get(i).getNativeObject());
+        return res;
+    }
+}
\ No newline at end of file
diff --git a/src/api/java/Fixedpoint.java b/src/api/java/Fixedpoint.java
index b59a9700a..e1fccdf4f 100644
--- a/src/api/java/Fixedpoint.java
+++ b/src/api/java/Fixedpoint.java
@@ -296,7 +296,7 @@ public class Fixedpoint extends Z3Object
     public BoolExpr[] getRules()
     {
         ASTVector v = new ASTVector(getContext(), Native.fixedpointGetRules(getContext().nCtx(), getNativeObject()));
-        return (BoolExpr[]) v.ToExprArray();
+        return v.ToBoolExprArray();
     }
 
     /**
@@ -307,7 +307,7 @@ public class Fixedpoint extends Z3Object
     public BoolExpr[] getAssertions()
     {
         ASTVector v = new ASTVector(getContext(), Native.fixedpointGetAssertions(getContext().nCtx(), getNativeObject()));
-        return (BoolExpr[]) v.ToExprArray();
+        return v.ToBoolExprArray();
     }
 
     /**
@@ -329,7 +329,7 @@ public class Fixedpoint extends Z3Object
     public BoolExpr[] ParseFile(String file)
     {
         ASTVector av = new ASTVector(getContext(), Native.fixedpointFromFile(getContext().nCtx(), getNativeObject(), file));
-        return (BoolExpr[])av.ToExprArray();
+        return av.ToBoolExprArray();
     }
 
     /** 
@@ -340,7 +340,7 @@ public class Fixedpoint extends Z3Object
     public BoolExpr[] ParseString(String s)
     {
         ASTVector av = new ASTVector(getContext(), Native.fixedpointFromString(getContext().nCtx(), getNativeObject(), s));
-        return (BoolExpr[])av.ToExprArray();
+        return av.ToBoolExprArray();
     }
     
 
diff --git a/src/api/java/InterpolationContext.java b/src/api/java/InterpolationContext.java
index 5af2a6af8..ddce9ee33 100644
--- a/src/api/java/InterpolationContext.java
+++ b/src/api/java/InterpolationContext.java
@@ -73,14 +73,14 @@ public class InterpolationContext extends Context
      * well documented.
      * @throws Z3Exception 
      **/
-    public Expr[] GetInterpolant(Expr pf, Expr pat, Params p)
+    public BoolExpr[] GetInterpolant(Expr pf, Expr pat, Params p)
     {
         checkContextMatch(pf);
         checkContextMatch(pat);
         checkContextMatch(p);
 
         ASTVector seq = new ASTVector(this, Native.getInterpolant(nCtx(), pf.getNativeObject(), pat.getNativeObject(), p.getNativeObject()));
-        return seq.ToExprArray();
+        return seq.ToBoolExprArray();
     }
 
     public class ComputeInterpolantResult 
@@ -107,7 +107,7 @@ public class InterpolationContext extends Context
         Native.LongPtr n_m = new Native.LongPtr();
         res.status = Z3_lbool.fromInt(Native.computeInterpolant(nCtx(), pat.getNativeObject(), p.getNativeObject(), n_i, n_m));        
         if (res.status == Z3_lbool.Z3_L_FALSE)
-            res.interp = (BoolExpr[]) (new ASTVector(this, n_i.value)).ToExprArray();
+            res.interp = (new ASTVector(this, n_i.value)).ToBoolExprArray();
         if (res.status == Z3_lbool.Z3_L_TRUE) res.model = new Model(this, n_m.value);
         return res;
     }
@@ -135,7 +135,7 @@ public class InterpolationContext extends Context
     /// Remarks: For more information on interpolation please refer
     /// too the function Z3_check_interpolant in the C/C++ API, which is 
     /// well documented.
-    public CheckInterpolantResult CheckInterpolant(Expr[] cnsts, int[] parents, Expr[] interps, String error, Expr[] theory)
+    public CheckInterpolantResult CheckInterpolant(Expr[] cnsts, int[] parents, BoolExpr[] interps, String error, Expr[] theory)
     {
         CheckInterpolantResult res = new CheckInterpolantResult();
         Native.StringPtr n_err_str = new Native.StringPtr();
diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java
index eb8e81aa5..4d2d9b641 100644
--- a/src/api/java/Solver.java
+++ b/src/api/java/Solver.java
@@ -188,7 +188,7 @@ public class Solver extends Z3Object
     public BoolExpr[] getAssertions()
     {
         ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(getContext().nCtx(), getNativeObject()));
-        return (BoolExpr[]) assrts.ToExprArray();
+        return assrts.ToBoolExprArray();
     }
 
     /**
@@ -280,7 +280,7 @@ public class Solver extends Z3Object
     {
 
         ASTVector core = new ASTVector(getContext(), Native.solverGetUnsatCore(getContext().nCtx(), getNativeObject()));        
-        return (BoolExpr[])core.ToExprArray();
+        return core.ToBoolExprArray();
     }
 
     /**