diff --git a/src/solver/solver_pool.cpp b/src/solver/solver_pool.cpp
index 8012dd129..a015c5ea2 100644
--- a/src/solver/solver_pool.cpp
+++ b/src/solver/solver_pool.cpp
@@ -32,8 +32,11 @@ class pool_solver : public solver_na2as {
     expr_ref_vector    m_flat;
     bool               m_pushed;
     bool               m_in_delayed_scope;
+    bool               m_dump_benchmarks;
+    double             m_dump_threshold;
     unsigned           m_dump_counter;
 
+
     bool is_virtual() const { return !m.is_true(m_pred); }
 public:
     pool_solver(solver* b, solver_pool& pool, app_ref& pred):
@@ -47,10 +50,13 @@ public:
         m_flat(m),
         m_pushed(false),
         m_in_delayed_scope(false),
+        m_dump_benchmarks(false),
+        m_dump_threshold(5.0),
         m_dump_counter(0) {
         if (is_virtual()) {
             solver_na2as::assert_expr_core2(m.mk_true(), pred);
         }
+        updt_params(m_base->get_params());
     }
 
     ~pool_solver() override {
@@ -64,7 +70,11 @@ public:
     solver* base_solver() { return m_base.get(); }
 
     solver* translate(ast_manager& m, params_ref const& p) override { UNREACHABLE(); return nullptr; }
-    void updt_params(params_ref const& p) override { solver::updt_params(p); m_base->updt_params(p); }
+    void updt_params(params_ref const& p) override {
+        solver::updt_params(p); m_base->updt_params(p);
+        m_dump_benchmarks = solver::get_params().get_bool("dump_benchmarks", false);
+        m_dump_threshold = solver::get_params().get_double("dump_threshold", 5.0);
+    }
     void push_params() override {m_base->push_params();}
     void pop_params() override {m_base->pop_params();}
 
@@ -76,8 +86,8 @@ public:
     void get_unsat_core(ptr_vector<expr> & r) override {
         m_base->get_unsat_core(r);
         unsigned j = 0;
-        for (unsigned i = 0; i < r.size(); ++i) 
-            if (m_pred != r[i]) 
+        for (unsigned i = 0; i < r.size(); ++i)
+            if (m_pred != r[i])
                 r[j++] = r[i];
         r.shrink(j);
     }
@@ -132,8 +142,10 @@ public:
         }
         set_status(res);
 
-        if (false /*m_dump_benchmarks && sw.get_seconds() >= m_pool.fparams().m_dump_min_time*/) {
-            dump_benchmark(num_assumptions, assumptions, res, sw);
+        if (m_dump_benchmarks && sw.get_seconds() >= m_dump_threshold) {
+            expr_ref_vector cube(m, num_assumptions, assumptions);
+            expr_ref_vector clause(m);
+            dump_benchmark(cube, clause, res, sw.get_seconds());
         }
         return res;
     }
@@ -164,9 +176,9 @@ public:
         }
         set_status(res);
 
-        // if (false /*m_dump_benchmarks && sw.get_seconds() >= m_pool.fparams().m_dump_min_time*/) {
-        //     dump_benchmark(num_assumptions, assumptions, res, sw);
-        // }
+        if (m_dump_benchmarks && sw.get_seconds() >= m_dump_threshold) {
+            dump_benchmark(cube, clause, res, sw.get_seconds());
+        }
         return res;
     }
 
@@ -179,9 +191,9 @@ public:
             m_pushed = true;
             m_in_delayed_scope = false;
         }
-        
-        if (!m_pushed) { 
-            m_in_delayed_scope = true; 
+
+        if (!m_pushed) {
+            m_in_delayed_scope = true;
         }
         else {
             SASSERT(!m_in_delayed_scope);
@@ -196,24 +208,24 @@ public:
             SASSERT(!m_in_delayed_scope);
             m_base->pop(n);
             m_pushed = lvl - n > 0;
-        } 
-        else { 
-            m_in_delayed_scope = lvl - n > 0; 
+        }
+        else {
+            m_in_delayed_scope = lvl - n > 0;
         }
     }
-    
+
     void assert_expr_core(expr * e) override {
         SASSERT(!m_pushed || get_scope_level() > 0);
-        if (m.is_true(e)) return; 
+        if (m.is_true(e)) return;
         if (m_in_delayed_scope) {
             internalize_assertions();
             m_base->push();
             m_pushed = true;
             m_in_delayed_scope = false;
         }
-        
+
         if (m_pushed) {
-            m_base->assert_expr(e); 
+            m_base->assert_expr(e);
         }
         else {
             m_flat.push_back(e);
@@ -221,7 +233,7 @@ public:
             m_assertions.append(m_flat);
             m_flat.reset();
         }
-    }   
+    }
 
     void get_model_core(model_ref & _m) override { m_base->get_model_core(_m); }
 
@@ -235,7 +247,7 @@ public:
     void set_progress_callback(progress_callback * callback) override { m_base->set_progress_callback(callback); }
 
     expr_ref_vector cube(expr_ref_vector& vars, unsigned ) override { return expr_ref_vector(m); }
-    
+
     ast_manager& get_manager() const override { return m_base->get_manager(); }
 
     void refresh(solver* new_base) {
@@ -253,42 +265,49 @@ public:
 
 private:
 
-    void dump_benchmark(unsigned num_assumptions, expr * const * assumptions, lbool res, stopwatch& sw) {
-        std::string file_name = mk_file_name();            
+    void dump_benchmark(const expr_ref_vector &cube, const expr_ref_vector &clause,
+                        lbool last_status, double last_time) {
+        std::string file_name = mk_file_name();
         std::ofstream out(file_name);
-        if (!out) { 
+        if (!out) {
             IF_VERBOSE(0, verbose_stream() << "could not open file " << file_name << " for output\n");
             return;
         }
 
-        out << "(set-info :status " << lbool2status(res) << ")\n";
-        m_base->display(out, num_assumptions, assumptions);
-        out << "(check-sat";
-        for (unsigned i = 0; i < num_assumptions; ++i) {
-            out << " " << mk_pp(assumptions[i], m);
+        out << "(set-info :status " << lbool2status(last_status) << ")\n";
+        m_base->display(out, cube.size(), cube.c_ptr());
+        if (!clause.empty()) {
+            out << ";; extra clause\n";
+            out << "(assert (or ";
+            for (auto *lit : clause) out << mk_pp(lit, m) << " ";
+            out << "))\n";
         }
-        out << ")";            
+
+        out << "(check-sat";
+        for (auto * lit : cube) out << " " << mk_pp(lit, m);
+        out << ")\n";
+
         out << "(exit)\n";
         ::statistics st;
         m_base->collect_statistics(st);
-        st.update("time", sw.get_seconds());
-        st.display_smt2(out);            
-        out.close();        
+        st.update("time", last_time);
+        st.display_smt2(out);
+        out.close();
     }
 
     char const* lbool2status(lbool r) const {
         switch (r) {
         case l_true:  return "sat";
         case l_false: return "unsat";
-        case l_undef: return "unknown"; 
+        case l_undef: return "unknown";
         }
         return "?";
     }
 
     std::string mk_file_name() {
         std::stringstream file_name;
-        file_name << "virt_solver";
-        if (is_virtual()) file_name << "_" << m_pred->get_decl()->get_name(); 
+        file_name << "pool_solver";
+        if (is_virtual()) file_name << "_" << m_pred->get_decl()->get_name();
         file_name << "_" << (m_dump_counter++) << ".smt2";
         return file_name.str();
     }
@@ -317,12 +336,11 @@ ptr_vector<solver> solver_pool::get_base_solvers() const {
 
 void solver_pool::updt_params(const params_ref &p) {
     m_base_solver->updt_params(p);
-    ptr_vector<solver> solvers = get_base_solvers();
-    for (solver *s : solvers) s->updt_params(p);
+    for (solver *s : m_solvers) s->updt_params(p);
 }
 void solver_pool::collect_statistics(statistics &st) const {
     ptr_vector<solver> solvers = get_base_solvers();
-    for (solver* s : solvers) s->collect_statistics(st);        
+    for (solver* s : solvers) s->collect_statistics(st);
     st.update("time.pool_solver.smt.total", m_check_watch.get_seconds());
     st.update("time.pool_solver.smt.total.sat", m_check_sat_watch.get_seconds());
     st.update("time.pool_solver.smt.total.undef", m_check_undef_watch.get_seconds());
@@ -336,7 +354,7 @@ void solver_pool::reset_statistics() {
 #if 0
     ptr_vector<solver> solvers = get_base_solvers();
     for (solver* s : solvers) {
-        s->reset_statistics();    
+        s->reset_statistics();
     }
 #endif
     m_stats.reset();
@@ -348,7 +366,7 @@ void solver_pool::reset_statistics() {
 
 /**
    \brief Create a fresh solver instance.
-   The first num_pools solvers are independent and 
+   The first num_pools solvers are independent and
    use a fresh instance of the base solver.
    Subsequent solvers reuse the first num_polls base solvers, rotating
    among the first num_pools.
@@ -374,7 +392,7 @@ solver* solver_pool::mk_solver() {
 void solver_pool::reset_solver(solver* s) {
     pool_solver* ps = dynamic_cast<pool_solver*>(s);
     SASSERT(ps);
-    if (ps) ps->reset();    
+    if (ps) ps->reset();
 }
 
 void solver_pool::refresh(solver* base_solver) {