diff --git a/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/SolverBase.java b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/SolverBase.java
index 5688959915..51fc7d80e4 100644
--- a/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/SolverBase.java
+++ b/subprojects/solver/solver/src/main/java/hu/bme/mit/theta/solver/SolverBase.java
@@ -84,5 +84,7 @@ default void pop() {
      *
      * @return Statistics
      */
-    default ImmutableMap<String, String> getStatistics() { return ImmutableMap.of(); }
+    default ImmutableMap<String, String> getStatistics() {
+        return ImmutableMap.of();
+    }
 }
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 e41e2f3cc6..d38072b0eb 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
@@ -68,8 +68,7 @@ import java.util.concurrent.TimeUnit
 import kotlin.random.Random
 
 fun runConfig(
-    config: XcfaConfig<*, *>, logger: Logger, uniqueLogger: Logger,
-    throwDontExit: Boolean
+    config: XcfaConfig<*, *>, logger: Logger, uniqueLogger: Logger, throwDontExit: Boolean
 ): SafetyResult<*, *> {
     propagateInputOptions(config, logger, uniqueLogger)
 
@@ -113,17 +112,13 @@ private fun propagateInputOptions(config: XcfaConfig<*, *>, logger: Logger, uniq
 
 private fun validateInputOptions(config: XcfaConfig<*, *>, logger: Logger, uniqueLogger: Logger) {
     rule("NoCoiWhenDataRace") {
-        config.backendConfig.backend == Backend.CEGAR &&
-            (config.backendConfig.specConfig as? CegarConfig)?.coi != ConeOfInfluenceMode.NO_COI &&
-            config.inputConfig.property == ErrorDetection.DATA_RACE
+        config.backendConfig.backend == Backend.CEGAR && (config.backendConfig.specConfig as? CegarConfig)?.coi != ConeOfInfluenceMode.NO_COI && config.inputConfig.property == ErrorDetection.DATA_RACE
     }
     rule("NoAaporWhenDataRace") {
-        (config.backendConfig.specConfig as? CegarConfig)?.porLevel?.isAbstractionAware == true &&
-            config.inputConfig.property == ErrorDetection.DATA_RACE
+        (config.backendConfig.specConfig as? CegarConfig)?.porLevel?.isAbstractionAware == true && config.inputConfig.property == ErrorDetection.DATA_RACE
     }
     rule("DPORWithoutDFS") {
-        (config.backendConfig.specConfig as? CegarConfig)?.porLevel?.isDynamic == true &&
-            (config.backendConfig.specConfig as? CegarConfig)?.abstractorConfig?.search != Search.DFS
+        (config.backendConfig.specConfig as? CegarConfig)?.porLevel?.isDynamic == true && (config.backendConfig.specConfig as? CegarConfig)?.abstractorConfig?.search != Search.DFS
     }
     rule("SensibleLoopUnrollLimits") {
         config.frontendConfig.loopUnroll != -1 && config.frontendConfig.loopUnroll < config.frontendConfig.forceUnroll
@@ -181,7 +176,8 @@ fun frontend(config: XcfaConfig<*, *>, logger: Logger, uniqueLogger: Logger): Tr
     )
 
     logger.write(RESULT, "ParsingResult Success\n")
-    logger.write(RESULT,
+    logger.write(
+        RESULT,
         "Alias graph size: ${xcfa.pointsToGraph.size} -> ${xcfa.pointsToGraph.values.map { it.size }.toList()}\n"
     )
 
@@ -189,57 +185,53 @@ fun frontend(config: XcfaConfig<*, *>, logger: Logger, uniqueLogger: Logger): Tr
 }
 
 private fun backend(
-    xcfa: XCFA, mcm: MCM, parseContext: ParseContext, config: XcfaConfig<*, *>,
-    logger: Logger,
-    uniqueLogger: Logger,
+    xcfa: XCFA, mcm: MCM, parseContext: ParseContext, config: XcfaConfig<*, *>, logger: Logger, uniqueLogger: Logger,
     throwDontExit: Boolean
-): SafetyResult<*, *> =
-    if (config.backendConfig.backend == Backend.NONE) {
-        SafetyResult.unknown<EmptyWitness, EmptyCex>()
+): SafetyResult<*, *> = if (config.backendConfig.backend == Backend.NONE) {
+    SafetyResult.unknown<EmptyWitness, EmptyCex>()
+} else {
+    if (xcfa.procedures.all { it.errorLoc.isEmpty && config.inputConfig.property == ErrorDetection.ERROR_LOCATION }) {
+        val result = SafetyResult.safe<EmptyWitness, EmptyCex>(EmptyWitness.getInstance())
+        logger.write(Logger.Level.INFO, "Input is trivially safe\n")
+
+        logger.write(RESULT, result.toString() + "\n")
+        result
     } else {
-        if (xcfa.procedures.all { it.errorLoc.isEmpty && config.inputConfig.property == ErrorDetection.ERROR_LOCATION }) {
-            val result = SafetyResult.safe<EmptyWitness, EmptyCex>(EmptyWitness.getInstance())
-            logger.write(Logger.Level.INFO, "Input is trivially safe\n")
-
-            logger.write(RESULT, result.toString() + "\n")
-            result
-        } else {
-            val stopwatch = Stopwatch.createStarted()
-
-            logger.write(
-                Logger.Level.INFO,
-                "Starting verification of ${if (xcfa.name == "") "UnnamedXcfa" else xcfa.name} using ${config.backendConfig.backend}\n"
-            )
-
-            val checker = getChecker(xcfa, mcm, config, parseContext, logger, uniqueLogger)
-            val result = exitOnError(config.debugConfig.stacktrace, config.debugConfig.debug || throwDontExit) {
-                checker.check()
-            }.let { result ->
-                when {
-                    result.isSafe && LoopUnrollPass.FORCE_UNROLL_USED -> { // cannot report safe if force unroll was used
-                        logger.write(RESULT, "Incomplete loop unroll used: safe result is unreliable.\n")
-                        if (config.outputConfig.acceptUnreliableSafe) result // for comparison with BMC tools
-                        else SafetyResult.unknown<EmptyWitness, EmptyCex>()
-                    }
-
-                    else -> result
+        val stopwatch = Stopwatch.createStarted()
+
+        logger.write(
+            Logger.Level.INFO,
+            "Starting verification of ${if (xcfa.name == "") "UnnamedXcfa" else xcfa.name} using ${config.backendConfig.backend}\n"
+        )
+
+        val checker = getChecker(xcfa, mcm, config, parseContext, logger, uniqueLogger)
+        val result = exitOnError(config.debugConfig.stacktrace, config.debugConfig.debug || throwDontExit) {
+            checker.check()
+        }.let { result ->
+            when {
+                result.isSafe && LoopUnrollPass.FORCE_UNROLL_USED -> { // cannot report safe if force unroll was used
+                    logger.write(RESULT, "Incomplete loop unroll used: safe result is unreliable.\n")
+                    if (config.outputConfig.acceptUnreliableSafe) result // for comparison with BMC tools
+                    else SafetyResult.unknown<EmptyWitness, EmptyCex>()
                 }
+
+                else -> result
             }
+        }
 
-            logger.write(
-                Logger.Level.INFO, "Backend finished (in ${
-                    stopwatch.elapsed(TimeUnit.MILLISECONDS)
-                } ms)\n"
-            )
+        logger.write(
+            Logger.Level.INFO, "Backend finished (in ${
+                stopwatch.elapsed(TimeUnit.MILLISECONDS)
+            } ms)\n"
+        )
 
-            logger.write(RESULT, result.toString() + "\n")
-            result
-        }
+        logger.write(RESULT, result.toString() + "\n")
+        result
     }
+}
 
 private fun preVerificationLogging(
-    xcfa: XCFA, mcm: MCM, parseContext: ParseContext, config: XcfaConfig<*, *>,
-    logger: Logger, uniqueLogger: Logger
+    xcfa: XCFA, mcm: MCM, parseContext: ParseContext, config: XcfaConfig<*, *>, logger: Logger, uniqueLogger: Logger
 ) {
     if (config.outputConfig.enableOutput) {
         try {
@@ -247,8 +239,7 @@ private fun preVerificationLogging(
             resultFolder.mkdirs()
 
             logger.write(
-                Logger.Level.INFO,
-                "Writing pre-verification artifacts to directory ${resultFolder.absolutePath}\n"
+                Logger.Level.INFO, "Writing pre-verification artifacts to directory ${resultFolder.absolutePath}\n"
             )
 
             if (!config.outputConfig.chcOutputConfig.disable) {
@@ -292,8 +283,8 @@ private fun preVerificationLogging(
 }
 
 private fun postVerificationLogging(
-    safetyResult: SafetyResult<*, *>, mcm: MCM,
-    parseContext: ParseContext, config: XcfaConfig<*, *>, logger: Logger, uniqueLogger: Logger
+    safetyResult: SafetyResult<*, *>, mcm: MCM, parseContext: ParseContext, config: XcfaConfig<*, *>, logger: Logger,
+    uniqueLogger: Logger
 ) {
     if (config.outputConfig.enableOutput) {
         try {
@@ -306,8 +297,7 @@ private fun postVerificationLogging(
             resultFolder.mkdirs()
 
             logger.write(
-                Logger.Level.INFO,
-                "Writing post-verification artifacts to directory ${resultFolder.absolutePath}\n"
+                Logger.Level.INFO, "Writing post-verification artifacts to directory ${resultFolder.absolutePath}\n"
             )
 
             // TODO eliminate the need for the instanceof check
@@ -320,12 +310,10 @@ private fun postVerificationLogging(
             if (!config.outputConfig.witnessConfig.disable) {
                 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(
+                        safetyResult.asUnsafe().cex as Trace<XcfaState<PtrState<*>>, XcfaAction>?, getSolver(
                             config.outputConfig.witnessConfig.concretizerSolver,
                             config.outputConfig.witnessConfig.validateConcretizerSolver
-                        ),
-                        parseContext
+                        ), parseContext
                     )
 
                     val traceFile = File(resultFolder, "trace.dot")
@@ -334,8 +322,7 @@ private fun postVerificationLogging(
 
                     val sequenceFile = File(resultFolder, "trace.plantuml")
                     writeSequenceTrace(
-                        sequenceFile,
-                        safetyResult.asUnsafe().cex as Trace<XcfaState<ExplState>, XcfaAction>
+                        sequenceFile, safetyResult.asUnsafe().cex as Trace<XcfaState<ExplState>, XcfaAction>
                     ) { (_, act) ->
                         act.label.getFlatLabels().map(XcfaLabel::toString)
                     }
@@ -354,8 +341,7 @@ private fun postVerificationLogging(
                 }
                 val witnessFile = File(resultFolder, "witness.graphml")
                 XcfaWitnessWriter().writeWitness(
-                    safetyResult, config.inputConfig.input!!,
-                    getSolver(
+                    safetyResult, config.inputConfig.input!!, getSolver(
                         config.outputConfig.witnessConfig.concretizerSolver,
                         config.outputConfig.witnessConfig.validateConcretizerSolver
                     ), parseContext, witnessFile