diff --git a/examples/c++/example.cpp b/examples/c++/example.cpp
index b348e7d36..0d8a3ceb3 100644
--- a/examples/c++/example.cpp
+++ b/examples/c++/example.cpp
@@ -21,6 +21,7 @@ void demorgan() {
     // adding the negation of the conjecture as a constraint.
     s.add(!conjecture);
     std::cout << s << "\n";
+    std::cout << s.to_smt2() << "\n";
     switch (s.check()) {
     case unsat:   std::cout << "de-Morgan is valid\n"; break;
     case sat:     std::cout << "de-Morgan is not valid\n"; break;
diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h
index c35208d86..7380e52f1 100644
--- a/src/api/c++/z3++.h
+++ b/src/api/c++/z3++.h
@@ -1314,6 +1314,26 @@ namespace z3 {
         expr_vector assertions() const { Z3_ast_vector r = Z3_solver_get_assertions(ctx(), m_solver); check_error(); return expr_vector(ctx(), r); }
         expr proof() const { Z3_ast r = Z3_solver_get_proof(ctx(), m_solver); check_error(); return expr(ctx(), r); }
         friend std::ostream & operator<<(std::ostream & out, solver const & s) { out << Z3_solver_to_string(s.ctx(), s); return out; }
+
+        std::string to_smt2(char const* status = "unknown") {
+            array<Z3_ast> es(assertions());
+            Z3_ast const* fmls = es.ptr();
+            Z3_ast fml = 0;
+            unsigned sz = es.size();
+            if (sz > 0) {
+                --sz;
+                fml = fmls[sz];
+            }
+            else {
+                fml = ctx().bool_val(true);
+            }
+            return std::string(Z3_benchmark_to_smtlib_string(
+                                   ctx(),
+                                   "", "", status, "", 
+                                   sz, 
+                                   fmls, 
+                                   fml));
+        }
     };
 
     class goal : public object {