From 9ed226dcfcb7a2fba337a263a01f68e78a6ec287 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= <joaopereira.19@gmail.com>
Date: Thu, 21 Sep 2023 16:18:00 +0200
Subject: [PATCH] fix tests

---
 .../info/implementation/property/Addressability.scala         | 1 +
 src/test/resources/regressions/features/let/let_simple.gobra  | 4 ++++
 2 files changed, 5 insertions(+)

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) {