From b0c8a5cf2117d29d7db5f87cd10ec061adfd91ff Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 16 May 2025 21:22:08 -0700 Subject: [PATCH] fix #7647 - with respect to scope level --- src/cmd_context/simplifier_cmds.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/cmd_context/simplifier_cmds.cpp b/src/cmd_context/simplifier_cmds.cpp index 9a915ed50..b2d96844a 100644 --- a/src/cmd_context/simplifier_cmds.cpp +++ b/src/cmd_context/simplifier_cmds.cpp @@ -156,10 +156,13 @@ public: auto simplifier_factory = sexpr2simplifier(ctx, m_simplifier); ctx.init_manager(); auto* s = ctx.get_solver(); + if (!s) + return; 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)); + if (s->get_scope_level() > 0) + throw cmd_exception("set-simplifier cannot be invoked above base scope level"); + ctx.set_solver(mk_simplifier_solver(s, &simplifier_factory)); } };