diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp index 74c7b3c775d..b8e6f1a0a36 100644 --- a/src/goto-symex/symex_goto.cpp +++ b/src/goto-symex/symex_goto.cpp @@ -102,6 +102,17 @@ void goto_symext::symex_goto(statet &state) new_state_pc=goto_target; state_pc=state.source.pc; state_pc++; + + // skip dead instructions + if(new_guard.is_true()) + while(state_pc!=goto_target && !state_pc->is_target()) + ++state_pc; + + if(state_pc==goto_target) + { + state.source.pc=goto_target; + return; // nothing else to do + } } else {