Let expressions inside magic wands cause verifiers to crash

[viper-admin]

Created by @vakaras on 2018-03-18 19:38
Last updated on 2018-03-19 12:54

Example:

#!silver
method test()
    ensures (
        true
        --*
        let tmp2 == (
            true
            ) in (
            tmp2
            --*
            true
        )
    )
{
}

Since this example crashes both back-ends with NoSuchElementException: key not found: tmp2, I suspect that this is a Silver issue. This is a blocking issue for Prusti.

[viper-admin]

@vakaras commented on 2018-03-19 12:54

Potentially fixed in c20cac4. @mschwerhoff: could you please take a look if that commit makes sense to you?

[viper-admin]

@vakaras on 2018-03-19 12:54:

• changed the assignee from @marcoeilers to @mschwerhoff