Viper gets stuck trying to verify a syntactically incorrect program (field.ref instead of ref.field)

[dnezam]

Note the following incorrect program:

field f: Int

method swap(a: Ref, b: Ref) {
    var tmp: Int
    tmp := f.a
    f.a := f.b
    f.b := tmp
}

Instead of using a.f and b.f, I accidentally wrote f.a and f.b.

When trying to verify the above program, the following behavior can be observed:

• using silicon: Verification is stuck at 0% for some time; after that, popups are spammed in the bottom right corner of VS Code notifying of a timeout. At this point, Viper is stuck aborting and must be reloaded. In fact, aborting gets stuck even if it is not caused by a timeout. using_silicon.log
• using carbon: Verification slowly goes up to 99%, where it gets stuck. Similar to using silicon, it tries to abort and spams timeout notifications in the bottom right. using_carbon.log (you can ignore the beginning of the log file which verifies an empty file ok.vpr - this was needed s.t. I can switch to carbon before opening crash.vpr and getting stuck)

This behavior has been observed on two machines: Manjaro Linux (arch-based) and Arch Linux (Java package: jre-openjdk, VS Code package: code)

[marcoeilers]

This was fixed in silver a couple of months ago.