Merge pull request #7323 from tautschnig/cleanup/goto-trace-simp

Goto trace: simplify io args, function arguments

Author: tautschnig

src/goto-symex/build_goto_trace.cpp

@@ -354,10 +354,12 @@ void build_goto_trace(
       goto_trace_step.io_id = SSA_step.io_id;
       goto_trace_step.formatted = SSA_step.formatted;
       goto_trace_step.called_function = SSA_step.called_function;
-      goto_trace_step.function_arguments = SSA_step.converted_function_arguments;
 
-      for(auto &arg : goto_trace_step.function_arguments)
-        arg = decision_procedure.get(arg);
+      for(const auto &arg : SSA_step.converted_function_arguments)
+      {
+        goto_trace_step.function_arguments.push_back(
+          simplify_expr(decision_procedure.get(arg), ns));
+      }
 
       // update internal field for specific variables in the counterexample
       update_internal_field(SSA_step, goto_trace_step, ns);
@@ -395,15 +397,8 @@ void build_goto_trace(
 
       for(const auto &j : SSA_step.converted_io_args)
       {
-        if(j.is_constant() || j.id() == ID_string_constant)
-        {
-          goto_trace_step.io_args.push_back(j);
-        }
-        else
-        {
-          exprt tmp = decision_procedure.get(j);
-          goto_trace_step.io_args.push_back(tmp);
-        }
+        goto_trace_step.io_args.push_back(
+          simplify_expr(decision_procedure.get(j), ns));
       }
 
       if(SSA_step.is_assert() || SSA_step.is_assume() || SSA_step.is_goto())