strenthen typing in disjunctive_polynomial_accelerationt

Author: Daniel Kroening

src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.cpp

@@ -546,8 +546,8 @@ bool disjunctive_polynomial_accelerationt::fit_polynomial(
 
   // Start building the program.  Begin by decl'ing each of the
   // master distinguishers.
-  for(std::list<exprt>::iterator it=distinguishers.begin();
-      it!=distinguishers.end();
+  for(std::list<symbol_exprt>::iterator it = distinguishers.begin();
+      it != distinguishers.end();
       ++it)
   {
     program.add_instruction(DECL)->code=code_declt(*it);
@@ -888,8 +888,8 @@ void disjunctive_polynomial_accelerationt::build_fixed()
 
   // Create shadow distinguisher variables.  These guys identify the path that
   // is taken through the fixed-path body.
-  for(std::list<exprt>::iterator it=distinguishers.begin();
-      it!=distinguishers.end();
+  for(std::list<symbol_exprt>::iterator it = distinguishers.begin();
+      it != distinguishers.end();
       ++it)
   {
     exprt &distinguisher=*it;
@@ -1006,8 +1006,8 @@ void disjunctive_polynomial_accelerationt::record_path(
 {
   distinguish_valuest path_val;
 
-  for(std::list<exprt>::iterator it=distinguishers.begin();
-      it!=distinguishers.end();
+  for(std::list<symbol_exprt>::iterator it = distinguishers.begin();
+      it != distinguishers.end();
       ++it)
   {
     path_val[*it]=program.eval(*it).is_true();

src/goto-instrument/accelerate/disjunctive_polynomial_acceleration.h

@@ -98,7 +98,7 @@ class disjunctive_polynomial_accelerationt
   acceleration_utilst utils;
   exprt loop_counter;
   distinguish_mapt distinguishing_points;
-  std::list<exprt> distinguishers;
+  std::list<symbol_exprt> distinguishers;
   expr_sett modified;
   goto_programt fixed;
   std::list<distinguish_valuest> accelerated_paths;