Fixed metadata for witness

ftsrg · Nov 21, 2023 · 76323a5 · 76323a5
1 parent 3d2492a
commit 76323a5
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 3 deletions.
diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/SimplifyExprsPass.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/SimplifyExprsPass.kt
@@ -36,7 +36,6 @@ import hu.bme.mit.theta.frontend.transformation.model.types.complex.CComplexType
 import hu.bme.mit.theta.xcfa.collectVarsWithAccessType
 import hu.bme.mit.theta.xcfa.isRead
 import hu.bme.mit.theta.xcfa.model.*
-import java.lang.UnsupportedOperationException
 
 /**
  * This pass simplifies the expressions inside statements and substitutes the values of constant variables
@@ -71,7 +70,7 @@ class SimplifyExprsPass(val parseContext: ParseContext) : ProcedurePass {
                                 CComplexType.getType(it.stmt.cond, parseContext))
                         }
                         parseContext.metadata.create(simplified, "cTruth", it.stmt.cond is NeqExpr<*>)
-                        StmtLabel(Assume(simplified), metadata = it.metadata)
+                        StmtLabel(Assume(simplified), metadata = it.metadata, choiceType = it.choiceType)
                     }
 
                     else -> it

diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/Utils.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/passes/Utils.kt
@@ -91,7 +91,8 @@ fun XcfaLabel.changeVars(varLut: Map<out Decl<*>, VarDecl<*>>, parseContext: Par
             is StartLabel -> StartLabel(name, params.map { it.changeVars(varLut, parseContext) },
                 pidVar.changeVars(varLut), metadata = metadata)
 
-            is StmtLabel -> StmtLabel(stmt.changeVars(varLut, parseContext), metadata = metadata)
+            is StmtLabel -> StmtLabel(stmt.changeVars(varLut, parseContext), metadata = metadata,
+                choiceType = this.choiceType)
             is WriteLabel -> WriteLabel(local.changeVars(varLut), global.changeVars(varLut), labels,
                 metadata = metadata)