Skip to content

Commit af514dc

Browse files
Function call argument identifiers must be unique across conversions
Necessary for incremental unwinding, which performs incremental conversions of symex_target_equationt.
1 parent c7d8047 commit af514dc

File tree

2 files changed

+3
-2
lines changed

2 files changed

+3
-2
lines changed

src/goto-symex/symex_target_equation.cpp

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -603,8 +603,6 @@ void symex_target_equationt::convert_assertions(
603603
void symex_target_equationt::convert_function_calls(
604604
decision_proceduret &dec_proc)
605605
{
606-
std::size_t argument_count=0;
607-
608606
for(auto &step : SSA_steps)
609607
if(!step.ignore)
610608
{

src/goto-symex/symex_target_equation.h

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -408,6 +408,9 @@ class symex_target_equationt:public symex_targett
408408

409409
// for unique I/O identifiers
410410
std::size_t io_count = 0;
411+
412+
// for unique function call argument identifiers
413+
std::size_t argument_count = 0;
411414
};
412415

413416
inline bool operator<(

0 commit comments

Comments
 (0)