From 60d8a91f17afab2304f52ed4fca7dd4a03e77b58 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Mon, 26 Nov 2018 15:26:18 +0000 Subject: [PATCH] Don't clean and rename unused guard expression As it was we tried to do renaming and simplification, only to bail because of the already-false state guard. That wasted time, and also generated false alarms when profiling calls to rename. --- src/goto-symex/symex_goto.cpp | 13 +++++++++---- 1 file changed, 9 insertions(+), 4 deletions(-) diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index b846e34ce52..e8fcd6fd1c4 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -25,6 +25,13 @@ void goto_symext::symex_goto(statet &state) const goto_programt::instructiont &instruction=*state.source.pc; statet::framet &frame=state.top(); + if(state.guard.is_false()) + { + // next instruction + symex_transition(state); + return; // nothing to do + } + exprt old_guard=instruction.guard; clean_expr(old_guard, state, false); @@ -32,11 +39,9 @@ void goto_symext::symex_goto(statet &state) state.rename(new_guard, ns); do_simplify(new_guard); - if(new_guard.is_false() || - state.guard.is_false()) + if(new_guard.is_false()) { - if(!state.guard.is_false()) - target.location(state.guard.as_expr(), state.source); + target.location(state.guard.as_expr(), state.source); // next instruction symex_transition(state);