From 87f22d17fea0a9e2978fadd2a16fb06a49dbaf50 Mon Sep 17 00:00:00 2001
From: Pointerbender <pointerbender@gmail.com>
Date: Fri, 27 May 2022 12:23:09 +0200
Subject: [PATCH] fixes and regression tests for #581

---
 .../plugin/standard/adt/AdtPASTExtension.scala  | 10 ++++++++--
 src/test/resources/adt/issue-581.vpr            | 17 +++++++++++++++++
 2 files changed, 25 insertions(+), 2 deletions(-)
 create mode 100644 src/test/resources/adt/issue-581.vpr

diff --git a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala
index d34d04abb..6ab0a3a86 100644
--- a/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala
+++ b/src/main/scala/viper/silver/plugin/standard/adt/AdtPASTExtension.scala
@@ -463,7 +463,6 @@ case class PDestructorCall(name: String, rcv: PExp)
   override def args: Seq[PExp] = Seq(rcv)
 
   override def translateExp(t: Translator): Exp = {
-    val actualRcv = t.exp(rcv)
     val so: Option[Map[TypeVar, Type]] = adtSubstitution match {
       case Some(ps) => Some(ps.m.map(kv => TypeVar(kv._1) -> t.ttyp(kv._2)))
       case None => None
@@ -472,6 +471,10 @@ case class PDestructorCall(name: String, rcv: PExp)
       case Some(s) =>
         val adt = t.getMembers()(this.adt.idndef.name).asInstanceOf[Adt]
         assert(s.keys.toSet == adt.typVars.toSet)
+        val actualRcv = rcv match {
+          case pr@PResultLit() => Result(AdtType(adt, s))(t.liftPos(pr))
+          case _ => t.exp(rcv)
+        }
         AdtDestructorApp(adt, name, actualRcv, s)(t.liftPos(this))
       case _ => sys.error("type unification error - should report and not crash")
     }
@@ -496,7 +499,6 @@ case class PDiscriminatorCall(name: PIdnUse, rcv: PExp)
   override def args: Seq[PExp] = Seq(rcv)
 
   override def translateExp(t: Translator): Exp = {
-    val actualRcv = t.exp(rcv)
     val so: Option[Map[TypeVar, Type]] = adtSubstitution match {
       case Some(ps) => Some(ps.m.map(kv => TypeVar(kv._1) -> t.ttyp(kv._2)))
       case None => None
@@ -505,6 +507,10 @@ case class PDiscriminatorCall(name: PIdnUse, rcv: PExp)
       case Some(s) =>
         val adt = t.getMembers()(this.adt.idndef.name).asInstanceOf[Adt]
         assert(s.keys.toSet == adt.typVars.toSet)
+        val actualRcv = rcv match {
+          case pr@PResultLit() => Result(AdtType(adt, s))(t.liftPos(pr))
+          case _ => t.exp(rcv)
+        }
         AdtDiscriminatorApp(adt, name.name, actualRcv, s)(t.liftPos(this))
       case _ => sys.error("type unification error - should report and not crash")
     }
diff --git a/src/test/resources/adt/issue-581.vpr b/src/test/resources/adt/issue-581.vpr
new file mode 100644
index 000000000..73beb244b
--- /dev/null
+++ b/src/test/resources/adt/issue-581.vpr
@@ -0,0 +1,17 @@
+adt Test {
+    A()
+    B(b: Int)
+}
+
+function foo(): Test
+    ensures result.isA
+{
+    A()
+}
+
+function bar(): Test
+    ensures result.isB
+    ensures result.b == 42
+{
+    B(42)
+}