From 87e30af82cabc9f320ba46b276290e6eb2f61678 Mon Sep 17 00:00:00 2001
From: Levente Bajczi <bajczilevi@gmail.com>
Date: Thu, 29 Aug 2024 16:27:41 +0200
Subject: [PATCH] added new flag --only-svcomp-witness

---
 build.gradle.kts                                          | 2 +-
 .../main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt  | 2 +-
 .../java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt   | 8 ++++++--
 3 files changed, 8 insertions(+), 4 deletions(-)

diff --git a/build.gradle.kts b/build.gradle.kts
index 741094252d..e029ef4eda 100644
--- a/build.gradle.kts
+++ b/build.gradle.kts
@@ -28,7 +28,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.theta"
-    version = "6.5.1"
+    version = "6.5.2"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }
diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt
index d54865638a..9469c2eca3 100644
--- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt
+++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/ExecuteConfig.kt
@@ -316,7 +316,7 @@ private fun postVerificationLogging(
             }
 
             if (!config.outputConfig.witnessConfig.disable) {
-                if (safetyResult.isUnsafe && safetyResult.asUnsafe().cex != null) {
+                if (safetyResult.isUnsafe && safetyResult.asUnsafe().cex != null && !config.outputConfig.witnessConfig.svcomp) {
                     val concrTrace: Trace<XcfaState<ExplState>, XcfaAction> = XcfaTraceConcretizer.concretize(
                         safetyResult.asUnsafe().cex as Trace<XcfaState<PtrState<*>>, XcfaAction>?,
                         getSolver(
diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt
index ef50a1e108..a52a05c957 100644
--- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt
+++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/XcfaConfig.kt
@@ -347,11 +347,12 @@ data class OutputConfig(
 ) : Config {
 
     override fun getObjects(): Set<Config> {
-        return super.getObjects() union cOutputConfig.getObjects() union xcfaOutputConfig.getObjects() union witnessConfig.getObjects() union argConfig.getObjects()
+        return super.getObjects() union cOutputConfig.getObjects() union xcfaOutputConfig.getObjects() union chcOutputConfig.getObjects() union witnessConfig.getObjects() union argConfig.getObjects()
     }
 
     override fun update(): Boolean =
-        listOf(cOutputConfig, xcfaOutputConfig, witnessConfig, argConfig).map { it.update() }.any { it }
+        listOf(cOutputConfig, xcfaOutputConfig, chcOutputConfig, witnessConfig, argConfig).map { it.update() }
+            .any { it }
 }
 
 data class XcfaOutputConfig(
@@ -382,6 +383,9 @@ data class WitnessConfig(
     @Parameter(names = ["--disable-witness-generation"])
     var disable: Boolean = false,
 
+    @Parameter(names = ["--only-svcomp-witness"])
+    var svcomp: Boolean = false,
+
     @Parameter(names = ["--cex-solver"], description = "Concretizer solver name")
     var concretizerSolver: String = "Z3",