diff --git a/src/main/scala/viper/gobra/frontend/info/implementation/property/Addressability.scala b/src/main/scala/viper/gobra/frontend/info/implementation/property/Addressability.scala index 30ade529b..59ccd55d4 100644 --- a/src/main/scala/viper/gobra/frontend/info/implementation/property/Addressability.scala +++ b/src/main/scala/viper/gobra/frontend/info/implementation/property/Addressability.scala @@ -86,6 +86,7 @@ trait Addressability extends BaseProperty { this: TypeInfoImpl => case p => Violation.violation(s"Unexpected invoke resolve, got $p") } case _: PLength | _: PCapacity => AddrMod.callResult + case _: PLet => AddrMod.rValue case _: PSliceExp => AddrMod.sliceExpr case _: PTypeAssertion => AddrMod.typeAssertionResult case _: PReceive => AddrMod.receive diff --git a/src/test/resources/regressions/features/let/let_simple.gobra b/src/test/resources/regressions/features/let/let_simple.gobra index 6d0cd8ae0..f50a4e1b6 100644 --- a/src/test/resources/regressions/features/let/let_simple.gobra +++ b/src/test/resources/regressions/features/let/let_simple.gobra @@ -32,6 +32,10 @@ func (a *A) g(x int) { fold a.Mem() } +pred Q(x int) { + true +} + requires acc(x) requires Q(y) func impureLets(x *int, y int) {