Revert "Don't generate unnecessary fresh symbols for the GOTO trace"

This reverts commit c0f4c34.

Author: tautschnig

regression/cbmc-incr-smt2/pointers-conversions/pointer_to_int.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 pointer_to_int.c
 --trace
 \[main\.assertion\.1\] line \d+ expected result == -1: success: SUCCESS

src/goto-symex/build_goto_trace.cpp

@@ -351,12 +351,10 @@ 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(const auto &arg : SSA_step.converted_function_arguments)
-      {
-        goto_trace_step.function_arguments.push_back(
-          simplify_expr(decision_procedure.get(arg), ns));
-      }
+      for(auto &arg : goto_trace_step.function_arguments)
+        arg = decision_procedure.get(arg);
 
       // update internal field for specific variables in the counterexample
       update_internal_field(SSA_step, goto_trace_step, ns);
@@ -393,8 +391,15 @@ void build_goto_trace(
 
       for(const auto &j : SSA_step.converted_io_args)
       {
-        goto_trace_step.io_args.push_back(
-          simplify_expr(decision_procedure.get(j), ns));
+        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);
+        }
       }
 
       if(SSA_step.is_assert() || SSA_step.is_assume() || SSA_step.is_goto())

src/goto-symex/symex_target_equation.cpp

@@ -620,18 +620,33 @@ void symex_target_equationt::convert_function_calls(
   {
     if(!step.ignore)
     {
+      and_exprt::operandst conjuncts;
       step.converted_function_arguments.reserve(step.ssa_function_arguments.size());
 
       for(const auto &arg : step.ssa_function_arguments)
       {
-        if(!arg.is_constant() && arg.id() != ID_string_constant)
+        if(arg.is_constant() ||
+           arg.id()==ID_string_constant)
+          step.converted_function_arguments.push_back(arg);
+        else
         {
-          equal_exprt eq{arg, arg};
+          const irep_idt identifier="symex::args::"+std::to_string(argument_count++);
+          symbol_exprt symbol(identifier, arg.type());
+
+          equal_exprt eq(arg, symbol);
           merge_irep(eq);
-          decision_procedure.set_to_true(eq);
+
+          decision_procedure.set_to(eq, true);
+          conjuncts.push_back(eq);
+          step.converted_function_arguments.push_back(symbol);
         }
-        step.converted_function_arguments.push_back(arg);
       }
+      with_solver_hardness(
+        decision_procedure,
+        [step_index, &conjuncts, &step](solver_hardnesst &hardness) {
+          hardness.register_ssa(
+            step_index, conjunction(conjuncts), step.source.pc);
+        });
     }
     ++step_index;
   }
@@ -644,16 +659,32 @@ void symex_target_equationt::convert_io(decision_proceduret &decision_procedure)
   {
     if(!step.ignore)
     {
+      and_exprt::operandst conjuncts;
       for(const auto &arg : step.io_args)
       {
-        if(!arg.is_constant() && arg.id() != ID_string_constant)
+        if(arg.is_constant() ||
+           arg.id()==ID_string_constant)
+          step.converted_io_args.push_back(arg);
+        else
         {
-          equal_exprt eq{arg, arg};
+          const irep_idt identifier =
+            "symex::io::" + std::to_string(io_count++);
+          symbol_exprt symbol(identifier, arg.type());
+
+          equal_exprt eq(arg, symbol);
           merge_irep(eq);
-          decision_procedure.set_to_true(eq);
+
+          decision_procedure.set_to(eq, true);
+          conjuncts.push_back(eq);
+          step.converted_io_args.push_back(symbol);
         }
-        step.converted_io_args.push_back(arg);
       }
+      with_solver_hardness(
+        decision_procedure,
+        [step_index, &conjuncts, &step](solver_hardnesst &hardness) {
+          hardness.register_ssa(
+            step_index, conjunction(conjuncts), step.source.pc);
+        });
     }
     ++step_index;
   }

src/solvers/smt2/smt2_conv.cpp

@@ -297,6 +297,14 @@ exprt smt2_convt::get(const exprt &expr) const
     if(it!=identifier_map.end())
       return it->second.value;
   }
+  else if(expr.id()==ID_member)
+  {
+    const member_exprt &member_expr=to_member_expr(expr);
+    exprt tmp=get(member_expr.struct_op());
+    if(tmp.is_nil())
+      return nil_exprt();
+    return member_exprt(tmp, member_expr.get_component_name(), expr.type());
+  }
   else if(expr.id() == ID_literal)
   {
     auto l = to_literal_expr(expr).get_literal();
@@ -315,17 +323,14 @@ exprt smt2_convt::get(const exprt &expr) const
   }
   else if(expr.is_constant())
     return expr;
-  else if(expr.has_operands())
+  else if(const auto &array = expr_try_dynamic_cast<array_exprt>(expr))
   {
-    exprt copy = expr;
-    for(auto &op : copy.operands())
+    exprt array_copy = *array;
+    for(auto &element : array_copy.operands())
     {
-      exprt eval_op = get(op);
-      if(eval_op.is_nil())
-        return nil_exprt{};
-      op = std::move(eval_op);
+      element = get(element);
     }
-    return copy;
+    return array_copy;
   }
 
   return nil_exprt();
@@ -4628,9 +4633,7 @@ void smt2_convt::set_to(const exprt &expr, bool value)
       const irep_idt &identifier=
         to_symbol_expr(equal_expr.lhs()).get_identifier();
 
-      if(
-        identifier_map.find(identifier) == identifier_map.end() &&
-        equal_expr.lhs() != equal_expr.rhs())
+      if(identifier_map.find(identifier)==identifier_map.end())
       {
         identifiert &id=identifier_map[identifier];
         CHECK_RETURN(id.type.is_nil());