The encoding of WaitLevel in a Quantifier as a loop invariant re-uses a quantified variable in a separate generated loop invariant, causing Silicon to crash.
See wl_forall_bug.py for a small example that triggers this.
Here an excerpt from the translated Viper file, where lambda32_30$j is used incorrectly:
The encoding of WaitLevel in a Quantifier as a loop invariant re-uses a quantified variable in a separate generated loop invariant, causing Silicon to crash.
See wl_forall_bug.py for a small example that triggers this.
Here an excerpt from the translated Viper file, where
lambda32_30$jis used incorrectly: