Merge pull request #296 from ftsrg/add-svcomp-flag

added new flag --only-svcomp-witness
ftsrg · Aug 29, 2024 · cb77d7e · cb77d7e
2 parents 289781e + 87e30af
commit cb77d7e
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 4 deletions.
diff --git 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
@@ -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
@@ -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",