From e3a849e96f989634bc3761de573006cc9570faaa Mon Sep 17 00:00:00 2001
From: Levente Bajczi <bajczilevi@gmail.com>
Date: Tue, 9 Dec 2025 16:05:57 +0100
Subject: [PATCH] Fix simplification getting rid of variable type

---
 build.gradle.kts                              |  2 +-
 .../java/hu/bme/mit/theta/xcfa/utils/Utils.kt | 26 ++++++++++++++-----
 2 files changed, 20 insertions(+), 8 deletions(-)

diff --git a/build.gradle.kts b/build.gradle.kts
index 9c3a978635..fd9e6bf8f2 100644
--- a/build.gradle.kts
+++ b/build.gradle.kts
@@ -36,7 +36,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.theta"
-    version = "6.27.14"
+    version = "6.27.15"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }
diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/utils/Utils.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/utils/Utils.kt
index 9f1a61cf10..19429bc66c 100644
--- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/utils/Utils.kt
+++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/utils/Utils.kt
@@ -29,6 +29,7 @@ import hu.bme.mit.theta.core.stmt.Stmts.Assign
 import hu.bme.mit.theta.core.stmt.Stmts.Assume
 import hu.bme.mit.theta.core.type.Expr
 import hu.bme.mit.theta.core.type.Type
+import hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Pos
 import hu.bme.mit.theta.core.type.abstracttype.NeqExpr
 import hu.bme.mit.theta.core.type.anytype.Dereference
 import hu.bme.mit.theta.core.type.anytype.RefExpr
@@ -147,13 +148,8 @@ fun XcfaLabel.simplify(valuation: MutableValuation, parseContext: ParseContext):
 
       is AssignStmt<*> -> {
         simplified as AssignStmt<*>
-        if (parseContext.metadata.getMetadataValue(stmt.expr, "cType").isPresent)
-          parseContext.metadata.create(
-            simplified.expr,
-            "cType",
-            CComplexType.getType(stmt.expr, parseContext),
-          )
-        StmtLabel(simplified, metadata = metadata)
+        val expr = simplified.expr.withMetadata(parseContext, stmt.expr)
+        AssignStmtLabel(simplified.varDecl, expr, metadata = metadata)
       }
 
       is AssumeStmt -> {
@@ -173,6 +169,22 @@ fun XcfaLabel.simplify(valuation: MutableValuation, parseContext: ParseContext):
     }
   } else this
 
+private fun <T : Type> Expr<T>.withMetadata(
+  parseContext: ParseContext,
+  metadataSource: Expr<*>,
+): Expr<T> {
+  val oldType = parseContext.metadata.getMetadataValue(this, "cType")
+  if (oldType.isPresent) {
+    val type = CComplexType.getType(metadataSource, parseContext)
+    if (type != oldType.get()) {
+      val newExpr = Pos(this)
+      parseContext.metadata.create(newExpr, "cType", type)
+      return newExpr as Expr<T>
+    }
+  }
+  return this
+}
+
 /**
  * Returns the set of edges that are before any thread start in the init procedure or after all
  * thread joins in the init procedure (when it is guaranteed that no other thread is running).