diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index 93e979016..29df0cb84 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -61,6 +61,11 @@ extern "C" {
         m_out << "(push)\n";
     }
 
+    void solver2smt2_pp::reset() {
+        m_out << "(reset)\n";
+        m_pp_util.reset();
+    }
+
     void solver2smt2_pp::pop(unsigned n) {
         m_out << "(pop " << n << ")\n";
     }
@@ -75,6 +80,22 @@ extern "C" {
         m_out.flush();
     }
 
+    void solver2smt2_pp::get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& variables) {
+        m_out << "(get-consequences (";
+        for (expr* f : assumptions) {
+            m_out << "\n";
+            m_pp_util.display_expr(m_out, f);
+        }
+        m_out << ") (";
+        for (expr* f : variables) {
+            m_out << "\n";
+            m_pp_util.display_expr(m_out, f);
+        }
+        m_out << ")\n";
+        m_out.flush();
+    }
+
+
     solver2smt2_pp::solver2smt2_pp(ast_manager& m, char const* file): m_pp_util(m), m_out(file) {
         if (!m_out) {
             std::string msg;
@@ -383,6 +404,7 @@ extern "C" {
         LOG_Z3_solver_reset(c, s);
         RESET_ERROR_CODE();
         to_solver(s)->m_solver = nullptr;
+        if (to_solver(s)->m_pp) to_solver(s)->m_pp->reset();
         Z3_CATCH;
     }
     
@@ -711,6 +733,7 @@ extern "C" {
             scoped_timer timer(timeout, &eh);
             scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
             try {
+                if (to_solver(s)->m_pp) to_solver(s)->m_pp->get_consequences(_assumptions, _variables); 
                 result = to_solver_ref(s)->get_consequences(_assumptions, _variables, _consequences);
             }
             catch (z3_exception & ex) {
diff --git a/src/api/api_solver.h b/src/api/api_solver.h
index ed3733a9a..dd7672fd2 100644
--- a/src/api/api_solver.h
+++ b/src/api/api_solver.h
@@ -29,7 +29,9 @@ struct solver2smt2_pp {
     void assert_expr(expr* e, expr* t);
     void push();
     void pop(unsigned n);
+    void reset();
     void check(unsigned n, expr* const* asms);
+    void get_consequences(expr_ref_vector const& assumptions, expr_ref_vector const& variables);
 };
 
 struct Z3_solver_ref : public api::object {
diff --git a/src/ast/ast_pp_util.h b/src/ast/ast_pp_util.h
index d4f65b975..1b978c1b3 100644
--- a/src/ast/ast_pp_util.h
+++ b/src/ast/ast_pp_util.h
@@ -35,6 +35,8 @@ class ast_pp_util {
 
     ast_pp_util(ast_manager& m): m(m), m_env(m), m_num_sorts(0), m_num_decls(0), coll(m) {}
 
+    void reset() { coll.reset(); m_removed.reset(); m_num_sorts = 0; m_num_decls = 0; }
+
     void collect(expr* e);
 
     void collect(unsigned n, expr* const* es);
diff --git a/src/ast/decl_collector.h b/src/ast/decl_collector.h
index 29e47cab4..3dfb5c94d 100644
--- a/src/ast/decl_collector.h
+++ b/src/ast/decl_collector.h
@@ -48,6 +48,7 @@ public:
     decl_collector(ast_manager & m);
     ast_manager & m() { return m_manager; }
 
+    void reset() { m_sorts.reset(); m_decls.reset(); m_visited.reset(); m_trail.reset(); }
     void visit_func(func_decl* n);
     void visit(ast * n);
     void visit(unsigned n, expr* const* es);