@@ -730,7 +730,7 @@ void polynomial_acceleratort::stash_polynomials(
730730{
731731 expr_sett modified;
732732 utils.find_modified (body, modified);
733- stash_variables (program, modified, substitution);
733+ utils. stash_variables (program, modified, substitution);
734734
735735 for (std::map<exprt, polynomialt>::iterator it=polynomials.begin ();
736736 it!=polynomials.end ();
@@ -740,25 +740,6 @@ void polynomial_acceleratort::stash_polynomials(
740740 }
741741}
742742
743- void polynomial_acceleratort::stash_variables (
744- scratch_programt &program,
745- expr_sett modified,
746- substitutiont &substitution)
747- {
748- find_symbols_sett vars =
749- find_symbols_or_nexts (modified.begin (), modified.end ());
750- irep_idt loop_counter_name=to_symbol_expr (loop_counter).get_identifier ();
751- vars.erase (loop_counter_name);
752-
753- for (const irep_idt &id : vars)
754- {
755- const symbolt &orig = symbol_table.lookup_ref (id);
756- symbolt stashed_sym=utils.fresh_symbol (" polynomial::stash" , orig.type );
757- substitution[orig.symbol_expr ()]=stashed_sym.symbol_expr ();
758- program.assign (stashed_sym.symbol_expr (), orig.symbol_expr ());
759- }
760- }
761-
762743/*
763744 * Finds a precondition which guarantees that all the assumptions and assertions
764745 * along this path hold.
0 commit comments