Merge pull request #4055 from peterschrammel/fix-io-counter

I/O names must be unique across multiple conversions

Author: peterschrammel

src/goto-symex/symex_target_equation.cpp

@@ -603,8 +603,6 @@ void symex_target_equationt::convert_assertions(
 void symex_target_equationt::convert_function_calls(
   decision_proceduret &dec_proc)
 {
-  std::size_t argument_count=0;
-
   for(auto &step : SSA_steps)
     if(!step.ignore)
     {
@@ -633,8 +631,6 @@ void symex_target_equationt::convert_function_calls(
 void symex_target_equationt::convert_io(
   decision_proceduret &dec_proc)
 {
-  std::size_t io_count=0;
-
   for(auto &step : SSA_steps)
     if(!step.ignore)
     {

src/goto-symex/symex_target_equation.h

@@ -405,6 +405,12 @@ class symex_target_equationt:public symex_targett
   // for enforcing sharing in the expressions stored
   merge_irept merge_irep;
   void merge_ireps(SSA_stept &SSA_step);
+
+  // for unique I/O identifiers
+  std::size_t io_count = 0;
+
+  // for unique function call argument identifiers
+  std::size_t argument_count = 0;
 };
 
 inline bool operator<(