Do not add __CPROVER variables to counterexample

Signed-off-by: František Nečas <[email protected]>

Author: FrNecas

src/ssa/ssa_build_goto_trace.cpp

@@ -168,11 +168,6 @@ bool ssa_build_goto_tracet::record_step(
 
   case ASSIGN:
   {
-    if(has_prefix(
-      id2string(unwindable_local_SSA.function_identifier),
-      CPROVER_PREFIX))
-      break;
-
     const code_assignt &code_assign=
       to_code_assign(current_pc->code);
 
@@ -182,6 +177,8 @@ bool ssa_build_goto_tracet::record_step(
     exprt rhs_simplified=simplify_expr(rhs_value, unwindable_local_SSA.ns);
     exprt lhs_ssa=finalize_lhs(code_assign.lhs());
     exprt lhs_simplified=simplify_expr(lhs_ssa, unwindable_local_SSA.ns);
+    if(from_expr(lhs_simplified).find(CPROVER_PREFIX)!=std::string::npos)
+      break;
 
 #if 0
     std::cout << "ASSIGN "