Symbolic variables are declared multiple times when also used as bound variables in quantified expressions

[mi-ki]

Expected behavior

Variables which are bound by quantified expressions only matter within those expressions, not outside of them.

Actual behavior

Defined symbolic variables can be used as bound variables in quantified expressions. The resulting C code thus declares this variable two times, once in the beginning and once in the loop itself, more precisely as the loop index which is declared and initialized.

Proposed solution

Forbid symbolic variables as bound variables in quantified expressions, i.e., only allow new/fresh variables to be bound by quantifiers.
Alternatively, a new variable could be produced, but I would rather have a clear distinction already in the property editor.

Steps to reproduce the behavior

In the property editor, I specify as symbolic variables a candidate Alice and a voter Bob, with the following precondition:

VOTER_AT_POS(0) == Bob;
!EXISTS_ONE_VOTER(Bob) :VOTES1(Bob) == Alice;

and the following postcondition:

ELECT1 != Alice;
VOTER_AT_POS(0) == Bob;

Among other code, the following c code is produced:

unsigned int Bob = nondet_uint();
assume (0 <= Bob && Bob < V);
// ...
for (unsigned int Bob = 0; Bob < V && !thereExists_0; Bob++) { /* ... */ }
// ...
unsigned int comparison_2 = 1;
comparison_2 = voterAtPos_1 == Bob;
assert (comparison_2);

Note that Bob is declared two times. Apparently, gcc is not picky about this program itself, but it is at least confusing to the reader and I am not too sure whether this is the intended behaviour.