From 153c9a29dff1fc8cd6c1dc7dacbd53c0a44f7496 Mon Sep 17 00:00:00 2001 From: Nathan Glenn Date: Tue, 25 Jun 2024 23:27:54 -0500 Subject: [PATCH] Don't push/pop disabled SVS subgoal states When SVS is disabled for subgoals, don't push or pop the state stack as new subgoals are created. --- Core/SVS/src/svs.cpp | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/Core/SVS/src/svs.cpp b/Core/SVS/src/svs.cpp index 96f6f585e8..7e5c84d643 100644 --- a/Core/SVS/src/svs.cpp +++ b/Core/SVS/src/svs.cpp @@ -384,6 +384,11 @@ void svs::state_creation_callback(Symbol* state) std::string type, msg; svs_state* s; + if (!(state->is_top_state() || is_enabled_in_substates())) + { + return; + } + if (state_stack.empty()) { if (scn_cache) @@ -404,6 +409,12 @@ void svs::state_creation_callback(Symbol* state) void svs::state_deletion_callback(Symbol* state) { svs_state* s; + + if (!(state->is_top_state() || is_enabled_in_substates())) + { + return; + } + s = state_stack.back(); assert(state == s->get_state()); if (state_stack.size() == 1)