Make goto_instruction take a renamedt argument

This reflects the assumptions on the argument better.

Author: romainbrenguier

src/goto-symex/symex_goto.cpp

@@ -59,8 +59,10 @@ void goto_symext::symex_goto(statet &state)
   exprt new_guard = instruction.get_condition();
   clean_expr(new_guard, state, false);
 
-  new_guard = state.rename(std::move(new_guard), ns).get();
-  do_simplify(new_guard);
+  renamedt<exprt, L2> renamed_guard = state.rename(std::move(new_guard), ns);
+  if(symex_config.simplify_opt)
+    renamed_guard.simplify(ns);
+  new_guard = renamed_guard.get();
 
   if(new_guard.is_false())
   {
@@ -71,7 +73,7 @@ void goto_symext::symex_goto(statet &state)
     return; // nothing to do
   }
 
-  target.goto_instruction(state.guard.as_expr(), new_guard, state.source);
+  target.goto_instruction(state.guard.as_expr(), renamed_guard, state.source);
 
   DATA_INVARIANT(
     !instruction.targets.empty(), "goto should have at least one target");

src/goto-symex/symex_target.h

@@ -248,8 +248,8 @@ class symex_targett
   ///  goto instruction
   virtual void goto_instruction(
     const exprt &guard,
-    const exprt &cond,
-    const sourcet &source)=0;
+    const renamedt<exprt, L2> &cond,
+    const sourcet &source) = 0;
 
   /// Record a _global_ constraint: there is no guard limiting its scope.
   /// \param cond: Condition represented by this constraint

src/goto-symex/symex_target_equation.cpp

@@ -304,14 +304,14 @@ void symex_target_equationt::assertion(
 
 void symex_target_equationt::goto_instruction(
   const exprt &guard,
-  const exprt &cond,
+  const renamedt<exprt, L2> &cond,
   const sourcet &source)
 {
   SSA_steps.emplace_back(source, goto_trace_stept::typet::GOTO);
   SSA_stept &SSA_step=SSA_steps.back();
 
   SSA_step.guard=guard;
-  SSA_step.cond_expr=cond;
+  SSA_step.cond_expr = cond.get();
 
   merge_ireps(SSA_step);
 }

src/goto-symex/symex_target_equation.h

@@ -142,7 +142,7 @@ class symex_target_equationt:public symex_targett
   /// \copydoc symex_targett::goto_instruction()
   virtual void goto_instruction(
     const exprt &guard,
-    const exprt &cond,
+    const renamedt<exprt, L2> &cond,
     const sourcet &source);
 
   /// \copydoc symex_targett::constraint()