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 https://github.com/viperproject/silver/commit/c20cac4f63e5eb4905729d6ed63133d05e2d98ab. @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