From 3fac441f3d0bdcf0659f84fb59060173a0a55212 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 16 May 2025 21:17:06 -0700 Subject: [PATCH] fix #7647 --- src/cmd_context/simplifier_cmds.cpp | 2 ++ 1 file changed, 2 insertions(+) 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)); }