Closed
Description
When using the VSCode extension for Viper, I first get an error at the last line of this method, which is the expected behavior. However, when I verify the file a second time, I get a spurious error reported: The first assert x == 5
, which should hold. I think this is due to how the server caches errors.
method wrong_assertion_false_when_cached() {
var x: Int := 5
assert x == 5 // Wrong cached error reported here
x := 3
assert x == 5 // Error here
}