Merge pull request #6725 from tautschnig/cleanup/stash_variables

Remove duplicate implementation of stash_variables

Author: tautschnig

src/goto-instrument/accelerate/polynomial_accelerator.cpp

@@ -730,7 +730,7 @@ void polynomial_acceleratort::stash_polynomials(
 {
   expr_sett modified;
   utils.find_modified(body, modified);
-  stash_variables(program, modified, substitution);
+  utils.stash_variables(program, modified, substitution);
 
   for(std::map<exprt, polynomialt>::iterator it=polynomials.begin();
       it!=polynomials.end();
@@ -740,25 +740,6 @@ void polynomial_acceleratort::stash_polynomials(
   }
 }
 
-void polynomial_acceleratort::stash_variables(
-  scratch_programt &program,
-  expr_sett modified,
-  substitutiont &substitution)
-{
-  find_symbols_sett vars =
-    find_symbols_or_nexts(modified.begin(), modified.end());
-  irep_idt loop_counter_name=to_symbol_expr(loop_counter).get_identifier();
-  vars.erase(loop_counter_name);
-
-  for(const irep_idt &id : vars)
-  {
-    const symbolt &orig = symbol_table.lookup_ref(id);
-    symbolt stashed_sym=utils.fresh_symbol("polynomial::stash", orig.type);
-    substitution[orig.symbol_expr()]=stashed_sym.symbol_expr();
-    program.assign(stashed_sym.symbol_expr(), orig.symbol_expr());
-  }
-}
-
 /*
  * Finds a precondition which guarantees that all the assumptions and assertions
  * along this path hold.

src/goto-instrument/accelerate/polynomial_accelerator.h

@@ -103,10 +103,6 @@ class polynomial_acceleratort
   bool check_inductive(
     std::map<exprt, polynomialt> polynomials,
     goto_programt::instructionst &body);
-  void stash_variables(
-    scratch_programt &program,
-    expr_sett modified,
-    substitutiont &substitution);
   void stash_polynomials(
     scratch_programt &program,
     std::map<exprt, polynomialt> &polynomials,