Variables in specifications aren't correctly renamed when building the AST.

[icmccorm]

The following loop invariants are used in composite.c0:

  while(i < stressCaptured)
  //@loop_invariant 0 <= i && i <= stressCaptured && tree(node);
  {
    ...
    struct Node* current = node;

    while(tree_has_left(current) && tree_has_right(current))
    //@loop_invariant tree(current);
    {
       ...
    }
    ...
  }

The variable current is renamed during translation in multiple locations except in the predicate instance tree(current) in the invariant, leading to verification errors when a partial, imprecise specification is created that has everything precise except for the outer invariant, where the expressions 0 <= i && i <= stressCaptured are replaced by a ?.

[icmccorm]

This was fixed by ensuring that variables in loop invariants are also targeted for renaming. See line #65-68 in Replacer.scala

    case loop: IR.While => {
      loop.condition = replace(loop.condition, m)
      loop.invariant = replace(loop.invariant, m)
    }