diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt index 7cbe0ca397..667514fd03 100644 --- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt +++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/oc/XcfaOcChecker.kt @@ -154,7 +154,7 @@ class XcfaOcChecker( } .also { logger.writeln(Logger.Level.MAINSTEP, "OC checker result: $it") - if (xcfa.unsafeUnrollUsed && !acceptUnreliableSafe) { + if (it.isSafe && xcfa.unsafeUnrollUsed && !acceptUnreliableSafe) { logger.writeln( Logger.Level.MAINSTEP, "Incomplete loop unroll used: safe result is unreliable.",