diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp
index cc1c4398a..878c0a007 100644
--- a/examples/c++/example.cpp
+++ b/examples/c++/example.cpp
@@ -1044,6 +1044,27 @@ void opt_example() {
     }
 }
 
+/**
+ * translate from one optimization context to another.
+ */
+void opt_translate_example() {
+    context c1, c2;
+    optimize o1(c1);
+    expr x = c1.int_const("x");
+    expr y = c1.int_const("y");
+    o1.add(10 >= x && x >= 0);
+    o1.add(10 >= y && y >= 0);
+    o1.add(x + y <= 11);
+    optimize::handle h1 = o1.maximize(x);
+    optimize::handle h2 = o1.maximize(y);
+    optimize o2(c2, o1);
+    expr z = c2.int_const("z");
+    expr x2 = c2.int_const("x");
+    o2.add(x2 + z == 2);
+    o2.minimize(z);
+    std::cout << o2 << "\n";
+}
+
 void extract_example() {
     std::cout << "extract example\n";
     context c;
@@ -1305,6 +1326,7 @@ int main() {
         exists_expr_vector_example(); std::cout << "\n";
         substitute_example(); std::cout << "\n";
         opt_example(); std::cout << "\n";
+        opt_translate_example(); std::cout << "\n";
         extract_example(); std::cout << "\n";
         param_descrs_example(); std::cout << "\n";
         sudoku_example(); std::cout << "\n";
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index 6052727e3..4fc69981d 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -1872,6 +1872,8 @@ namespace z3 {
         ast_vector_tpl(context & c):object(c) { init(Z3_mk_ast_vector(c)); }
         ast_vector_tpl(context & c, Z3_ast_vector v):object(c) { init(v); }
         ast_vector_tpl(ast_vector_tpl const & s):object(s), m_vector(s.m_vector) { Z3_ast_vector_inc_ref(ctx(), m_vector); }
+        ast_vector_tpl(context& c, ast_vector_tpl const& src): object(c) { init(Z3_ast_vector_translate(src.ctx(), src, c)); }
+
         ~ast_vector_tpl() { Z3_ast_vector_dec_ref(ctx(), m_vector); }
         operator Z3_ast_vector() const { return m_vector; }
         unsigned size() const { return Z3_ast_vector_size(ctx(), m_vector); }
@@ -2778,6 +2780,11 @@ namespace z3 {
             Z3_optimize_inc_ref(o.ctx(), o.m_opt);
             m_opt = o.m_opt;
         }
+        optimize(context& c, optimize& src):object(c) {
+            m_opt = Z3_mk_optimize(c); Z3_optimize_inc_ref(c, m_opt);
+            add(expr_vector(c, src.assertions()));
+            for (expr& o : expr_vector(c, src.objectives())) minimize(o);            
+        }
         optimize& operator=(optimize const& o) {
             Z3_optimize_inc_ref(o.ctx(), o.m_opt);
             Z3_optimize_dec_ref(ctx(), m_opt);
@@ -2791,6 +2798,9 @@ namespace z3 {
             assert(e.is_bool());
             Z3_optimize_assert(ctx(), m_opt, e);
         }
+        void add(expr_vector const& es) {
+            for (expr& e : es) add(e);
+        }
         handle add(expr const& e, unsigned weight) {
             assert(e.is_bool());
             std::stringstream strm;
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index ef875479f..23caf8d93 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -217,7 +217,7 @@ namespace opt {
             break;
         case O_MAXIMIZE:
             result = o.m_term;
-            if (m_arith.is_arith_expr(result)) {
+            if (m_arith.is_int_real(result)) {
                 result = m_arith.mk_uminus(result);
             }
             else if (m_bv.is_bv(result)) {