diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp
index 9f4f9431c..ce15bf37d 100644
--- a/examples/c++/example.cpp
+++ b/examples/c++/example.cpp
@@ -205,6 +205,9 @@ void bitvector_example1() {
 
     // using unsigned <=
     prove(ule(x - 10, 0) == ule(x, 10));
+
+    expr y = c.bv_const("y", 32);
+    prove(implies(concat(x, y) == concat(y, x), x == y));
 }
 
 /**
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index f43ba83e5..ca93d28d9 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -655,6 +655,7 @@ namespace z3 {
         friend expr ite(expr const & c, expr const & t, expr const & e);
 
         friend expr distinct(expr_vector const& args);
+        friend expr concat(expr const& a, expr const& b);
 
         friend expr operator==(expr const & a, expr const & b) {
             check_context(a, b);
@@ -1108,6 +1109,12 @@ namespace z3 {
         ctx.check_error();
         return expr(ctx, r);
     }
+
+    inline expr concat(expr const& a, expr const& b) {
+        Z3_ast r = Z3_mk_concat(ctx, (Z3_app) a, (Z3_app) b);
+        ctx.check_error();
+        return expr(ctx, r);
+    }
     
     class func_entry : public object {
         Z3_func_entry m_entry;