Make symex_output take renamedt args

This reflect the assumptions we should have on the arguments.

Author: romainbrenguier

src/goto-symex/symex_builtin_functions.cpp

@@ -358,13 +358,14 @@ void goto_symext::symex_output(
   PRECONDITION(code.operands().size() >= 2);
   exprt id_arg = state.rename(code.op0(), ns).get();
 
-  std::list<exprt> args;
+  std::list<renamedt<exprt, L2>> args;
 
   for(std::size_t i=1; i<code.operands().size(); i++)
   {
-    exprt l2_arg = state.rename(code.operands()[i], ns).get();
-    do_simplify(l2_arg);
-    args.emplace_back(std::move(l2_arg));
+    renamedt<exprt, L2> l2_arg = state.rename(code.operands()[i], ns);
+    if(symex_config.simplify_opt)
+      l2_arg.simplify(ns);
+    args.emplace_back(l2_arg);
   }
 
   const irep_idt output_id=get_string_argument(id_arg, ns);
@@ -470,12 +471,12 @@ void goto_symext::symex_trace(
 
   if(symex_config.debug_level >= debug_lvl)
   {
-    std::list<exprt> vars;
+    std::list<renamedt<exprt, L2>> vars;
 
     irep_idt event = to_string_constant(code.arguments()[1].op0()).get_value();
 
     for(std::size_t j=2; j<code.arguments().size(); j++)
-      vars.push_back(state.rename(code.arguments()[j], ns).get());
+      vars.push_back(state.rename(code.arguments()[j], ns));
 
     target.output(state.guard.as_expr(), state.source, event, vars);
   }

src/goto-symex/symex_target.h

@@ -191,7 +191,7 @@ class symex_targett
     const exprt &guard,
     const sourcet &source,
     const irep_idt &output_id,
-    const std::list<exprt> &args)=0;
+    const std::list<renamedt<exprt, L2>> &args) = 0;
 
   /// Record formatted output.
   /// \param guard: Precondition for writing to the output

src/goto-symex/symex_target_equation.cpp

@@ -224,13 +224,14 @@ void symex_target_equationt::output(
   const exprt &guard,
   const sourcet &source,
   const irep_idt &output_id,
-  const std::list<exprt> &args)
+  const std::list<renamedt<exprt, L2>> &args)
 {
   SSA_steps.emplace_back(source, goto_trace_stept::typet::OUTPUT);
   SSA_stept &SSA_step=SSA_steps.back();
 
   SSA_step.guard=guard;
-  SSA_step.io_args=args;
+  for(const auto &arg : args)
+    SSA_step.io_args.emplace_back(arg.get());
   SSA_step.io_id=output_id;
 
   merge_ireps(SSA_step);

src/goto-symex/symex_target_equation.h

@@ -109,7 +109,7 @@ class symex_target_equationt:public symex_targett
     const exprt &guard,
     const sourcet &source,
     const irep_idt &output_id,
-    const std::list<exprt> &args);
+    const std::list<renamedt<exprt, L2>> &args);
 
   /// \copydoc symex_targett::output_fmt()
   virtual void output_fmt(