From badcc4358fff85e48629edb194ca2d6992b8cc35 Mon Sep 17 00:00:00 2001
From: Levente Bajczi <bajczilevi@gmail.com>
Date: Thu, 16 Nov 2023 21:32:57 +0100
Subject: [PATCH] Fixed tests

---
 .../java/hu/bme/mit/theta/xcfa/cli/utils/BMCValToTrace.kt   | 6 +++---
 .../java/hu/bme/mit/theta/xcfa/cli/XcfaCliVerifyTest.kt     | 3 ---
 2 files changed, 3 insertions(+), 6 deletions(-)

diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/BMCValToTrace.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/BMCValToTrace.kt
index 735cc3103e..767854453e 100644
--- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/BMCValToTrace.kt
+++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/BMCValToTrace.kt
@@ -33,12 +33,12 @@ fun valToAction(xcfa: XCFA, val1: Valuation, val2: Valuation): XcfaAction {
     val val2Map = val2.toMap()
     var i = 0
     val map: MutableMap<XcfaLocation, Int> = HashMap()
-    for (x in xcfa.procedures.first().locs) {
+    for (x in xcfa.procedures.first { it.name == "main" }.locs) {
         map[x] = i++
     }
     return XcfaAction(
         pid = 0,
-        edge = xcfa.procedures.first().edges.first { edge ->
+        edge = xcfa.procedures.first { it.name == "main" }.edges.first { edge ->
             map[edge.source] == (val1Map[val1Map.keys.first { it.name == "__loc_" }] as IntLitExpr).value.toInt() &&
                 map[edge.target] == (val2Map[val2Map.keys.first { it.name == "__loc_" }] as IntLitExpr).value.toInt()
         })
@@ -48,7 +48,7 @@ fun valToState(xcfa: XCFA, val1: Valuation): XcfaState<ExplState> {
     val valMap = val1.toMap()
     var i = 0
     val map: MutableMap<Int, XcfaLocation> = HashMap()
-    for (x in xcfa.procedures.first().locs) {
+    for (x in xcfa.procedures.first { it.name == "main" }.locs) {
         map[i++] = x
     }
     return XcfaState(
diff --git a/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliVerifyTest.kt b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliVerifyTest.kt
index 3918d17e5b..98a68c6600 100644
--- a/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliVerifyTest.kt
+++ b/subprojects/xcfa/xcfa-cli/src/test/java/hu/bme/mit/theta/xcfa/cli/XcfaCliVerifyTest.kt
@@ -65,12 +65,9 @@ class XcfaCliVerifyTest {
                 Arguments.of("/c/litmustest/singlethread/03bitwise.c", null),
                 Arguments.of("/c/litmustest/singlethread/04real.c", null),
                 Arguments.of("/c/litmustest/singlethread/06arrays.c", null),
-                Arguments.of("/c/litmustest/singlethread/07arrayinit.c", null),
-                Arguments.of("/c/litmustest/singlethread/08vararray.c", null),
                 Arguments.of("/c/litmustest/singlethread/13typedef.c", "--domain PRED_CART"),
                 Arguments.of("/c/litmustest/singlethread/14ushort.c", null),
                 Arguments.of("/c/litmustest/singlethread/15addition.c", null),
-                Arguments.of("/c/litmustest/singlethread/16loop.c", null),
                 Arguments.of("/c/litmustest/singlethread/20testinline.c", null),
                 Arguments.of("/c/litmustest/singlethread/21namecollision.c", null),
                 Arguments.of("/c/litmustest/singlethread/22nondet.c", null),