diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs
index 80ca7a0cd..c9e76e68e 100644
--- a/src/api/dotnet/Solver.cs
+++ b/src/api/dotnet/Solver.cs
@@ -290,6 +290,17 @@ namespace Microsoft.Z3
             }
         }
 
+        /// <summary>
+        /// Create a clone of the current solver with respect to <c>ctx</c>.
+        /// </summary>
+        public Solver Translate(Context ctx) 
+        {
+	     Contract.Requires(ctx != null);
+             Contract.Ensures(Contract.Result<Solver>() != null);
+             return new Solver(ctx, Native.Z3_solver_translate(Context.nCtx, NativeObject, ctx.nCtx));
+        }
+
+
         /// <summary>
         /// Solver statistics.
         /// </summary>
diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java
index 4d2d9b641..f312da051 100644
--- a/src/api/java/Solver.java
+++ b/src/api/java/Solver.java
@@ -293,6 +293,14 @@ public class Solver extends Z3Object
                 getNativeObject());
     }
 
+    /**
+     * Create a clone of the current solver with respect to <c>ctx</c>.
+     */
+    public Solver translate(Context ctx) 
+    {
+	return new Solver(ctx, Native.solverTranslate(getContext().nCtx(), getNativeObject(), ctx.nCtx()));
+    }
+
     /**
      * Solver statistics.
      *