diff --git a/src/cmd_context/simplifier_cmds.cpp b/src/cmd_context/simplifier_cmds.cpp
index ac8d3e839..9a915ed50 100644
--- a/src/cmd_context/simplifier_cmds.cpp
+++ b/src/cmd_context/simplifier_cmds.cpp
@@ -156,6 +156,8 @@ public:
         auto simplifier_factory = sexpr2simplifier(ctx, m_simplifier);
         ctx.init_manager();
         auto* s = ctx.get_solver();
+        if (s->get_num_assertions() > 0) 
+            throw cmd_exception("set-simplifier cannot be invoked if there are already assertions");
         if (s)
             ctx.set_solver(mk_simplifier_solver(s, &simplifier_factory));        
     }