Merge pull request #3466 from smowton/smowton/cleanup/skip-unreachable-goto

Don't clean and rename unused guard expression

Author: tautschnig

src/goto-symex/symex_goto.cpp

@@ -25,18 +25,23 @@ 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);
 
   exprt new_guard=old_guard;
   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);