From 72cb4219966080b6d9aa1db4a7053e3093d88f00 Mon Sep 17 00:00:00 2001
From: Alexander Stekelenburg <a.v.stekelenburg@utwente.nl>
Date: Fri, 13 Sep 2024 13:41:42 +0200
Subject: [PATCH] Fix unsoundness in pointer cast encoding

---
 src/rewrite/vct/rewrite/ClassToRef.scala | 22 +++++++++++++++-------
 1 file changed, 15 insertions(+), 7 deletions(-)

diff --git a/src/rewrite/vct/rewrite/ClassToRef.scala b/src/rewrite/vct/rewrite/ClassToRef.scala
index 77c3e6b64..15c2ce2b4 100644
--- a/src/rewrite/vct/rewrite/ClassToRef.scala
+++ b/src/rewrite/vct/rewrite/ClassToRef.scala
@@ -377,7 +377,6 @@ case class ClassToRef[Pre <: Generation]() extends Rewriter[Pre] {
           case cls: ByValueClass[Pre] =>
             implicit val o: Origin = cls.o
             val axiomType = TAxiomatic[Post](byValClassSucc.ref(cls), Nil)
-            val classType = cls.classType(Nil)
             var valueAsAxioms: Seq[ADTAxiom[Post]] = Seq()
             val (fieldFunctions, fieldInverses, fieldTypes) =
               cls.decls.collect { case field: Field[Pre] =>
@@ -409,12 +408,21 @@ case class ClassToRef[Pre <: Generation]() extends Rewriter[Pre] {
                     ))
 
                   valueAsAxioms =
-                    valueAsAxioms ++ unwrapValueAs(
-                      axiomType,
-                      field.t,
-                      newT,
-                      byValFieldSucc.ref(field),
-                    )
+                    valueAsAxioms ++
+                      (field.t match {
+                        case t: TByValueClass[Pre] =>
+                          // TODO: If there are no fields we should ignore the first field and add the axioms for the second field
+                          t.cls.decl.decls
+                            .collectFirst({ case innerF: InstanceField[Pre] =>
+                              unwrapValueAs(
+                                axiomType,
+                                innerF.t,
+                                dispatch(innerF.t),
+                                byValFieldSucc.ref(field),
+                              )
+                            }).getOrElse(Nil)
+                        case _ => Nil
+                      })
                 }
                 (
                   byValFieldSucc(field),