From 706f9d5bd918ea49c7976594c67eb21f334ac3d1 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Mon, 14 Mar 2022 10:23:29 +0000
Subject: [PATCH] Remove duplicate implementation of stash_variables

The implementation in acceleration_utilst has exactly the same code.
---
 .../accelerate/polynomial_accelerator.cpp     | 21 +------------------
 .../accelerate/polynomial_accelerator.h       |  4 ----
 2 files changed, 1 insertion(+), 24 deletions(-)

diff --git a/src/goto-instrument/accelerate/polynomial_accelerator.cpp b/src/goto-instrument/accelerate/polynomial_accelerator.cpp
index 0435174de28..c7e7114486d 100644
--- a/src/goto-instrument/accelerate/polynomial_accelerator.cpp
+++ b/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.
diff --git a/src/goto-instrument/accelerate/polynomial_accelerator.h b/src/goto-instrument/accelerate/polynomial_accelerator.h
index 2414935cceb..763b397aa6c 100644
--- a/src/goto-instrument/accelerate/polynomial_accelerator.h
+++ b/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,