diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index ca13451b6..7c489ccc3 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1493,7 +1493,8 @@ void cmd_context::insert_aux_pdecl(pdecl * p) {
     m_aux_pdecls.push_back(p);
 }
 
-void cmd_context::reset(bool finalize) {    
+void cmd_context::reset(bool finalize) {
+    m_simplifier_factory = nullptr;
     m_logic = symbol::null;
     m_check_sat_result = nullptr;
     m_numeral_as_real = false;
@@ -2260,6 +2261,8 @@ void cmd_context::mk_solver() {
     m_params.get_solver_params(p, proofs_enabled, models_enabled, unsat_core_enabled);
     m_solver = (*m_solver_factory)(m(), p, proofs_enabled, models_enabled, unsat_core_enabled, m_logic);
     m_solver = mk_slice_solver(m_solver.get());
+    if (m_simplifier_factory) 
+        m_solver = mk_simplifier_solver(m_solver.get(), &m_simplifier_factory);
 }
 
 
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index c90d56237..5e5f30028 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -38,6 +38,7 @@ Notes:
 #include "solver/solver.h"
 #include "solver/check_logic.h"
 #include "solver/progress_callback.h"
+#include "solver/simplifier_solver.h"
 #include "cmd_context/pdecl.h"
 #include "cmd_context/tactic_manager.h"
 #include "params/context_params.h"
@@ -282,6 +283,7 @@ protected:
     std::vector<std::string>     m_assertion_strings;
     ptr_vector<expr>             m_assertion_names; // named assertions are represented using boolean variables.
     scoped_ptr<var_subst>        m_std_subst, m_rev_subst;
+    simplifier_factory           m_simplifier_factory;
 
     struct scope {
         unsigned m_func_decls_stack_lim;
@@ -429,6 +431,7 @@ public:
     void set_initial_value(expr* var, expr* value);
 
     void set_solver_factory(solver_factory * s);
+    void set_simplifier_factory(simplifier_factory& sf) { m_simplifier_factory = sf; }
     void set_check_sat_result(check_sat_result * r) { m_check_sat_result = r; }
     check_sat_result * get_check_sat_result() const { return m_check_sat_result.get(); }
     check_sat_state cs_state() const;
diff --git a/src/cmd_context/simplifier_cmds.cpp b/src/cmd_context/simplifier_cmds.cpp
index b2d96844a..291142b53 100644
--- a/src/cmd_context/simplifier_cmds.cpp
+++ b/src/cmd_context/simplifier_cmds.cpp
@@ -156,7 +156,8 @@ public:
         auto simplifier_factory = sexpr2simplifier(ctx, m_simplifier);
         ctx.init_manager();
         auto* s = ctx.get_solver();
-        if (!s)
+        ctx.set_simplifier_factory(simplifier_factory);
+        if (!s) 
             return;
         if (s->get_num_assertions() > 0) 
             throw cmd_exception("set-simplifier cannot be invoked if there are already assertions");