Change odd behaviour of remove_java_nondet()

Author: Owen Jones

src/goto-programs/replace_java_nondet.cpp

@@ -121,26 +121,6 @@ static bool is_typecast_with_id(const exprt& expr, const irep_idt& identifier)
   return op_symbol.get_identifier()==identifier;
 }
 
-/// Return whether the instruction is an assignment, and the rhs is a symbol or
-/// typecast expression with the specified identifier.
-/// \param instr: A goto program instruction.
-/// \param identifier: Some identifier.
-/// \return True if the expression is a typecast with one operand, and the
-///   typecast's identifier matches the specified identifier.
-static bool is_assignment_from(
-  const goto_programt::instructiont &instr,
-  const irep_idt &identifier)
-{
-  // If not an assignment, return false
-  if(!instr.is_assign())
-  {
-    return false;
-  }
-  const auto &rhs=to_code_assign(instr.code).rhs();
-  return is_symbol_with_id(rhs, identifier) ||
-         is_typecast_with_id(rhs, identifier);
-}
-
 /// Given an iterator into a list of instructions, modify the list to replace
 /// 'nondet' library functions with CBMC-native nondet expressions, and return
 /// an iterator to the next instruction to check.
@@ -170,30 +150,17 @@ static goto_programt::targett check_and_replace_target(
   {
     return next_instr;
   }
-  const auto return_identifier=
-    to_symbol_expr(next_instr_assign_lhs).get_identifier();
 
   auto &instructions=goto_program.instructions;
   const auto end=instructions.end();
 
-  // Look for an instruction where this name is on the RHS of an assignment
-  const auto matching_assignment=std::find_if(
-    next_instr,
-    end,
-    [&return_identifier](const goto_programt::instructiont &instr)
-    {
-      return is_assignment_from(instr, return_identifier);
-    });
-
-  assert(matching_assignment!=end);
-
   // Assume that the LHS of *this* assignment is the actual nondet variable
-  const auto &code_assign=to_code_assign(matching_assignment->code);
+  const auto &code_assign=to_code_assign(next_instr->code);
   const auto nondet_var=code_assign.lhs();
   const auto source_loc=target->source_location;
 
   // Erase from the nondet function call to the assignment
-  const auto after_matching_assignment=std::next(matching_assignment);
+  const auto after_matching_assignment=std::next(next_instr);
   assert(after_matching_assignment!=end);
 
   std::for_each(