diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/analysis/FiniteStateChecker.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/analysis/FiniteStateChecker.kt
index 477c589620..76cde6ac78 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/analysis/FiniteStateChecker.kt
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/mcm/analysis/FiniteStateChecker.kt
@@ -52,7 +52,7 @@ class FiniteStateChecker<S : ExplState, A : StmtAction, T>(
         initStates.forEach { lastIds[it] = initId }
         while (initStates.isNotEmpty()) {
             val state = initStates.pop()
-            val lastId = lastIds[state]!!
+            val lastId = checkNotNull(lastIds[state])
             val actions = actionFunc.getEnabledActionsFor(state)
 
             val nextStates = actions.map { a ->
diff --git a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/compilers/pattern2expr/Pattern2ExprCompiler.kt b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/compilers/pattern2expr/Pattern2ExprCompiler.kt
index 3767881d9d..ab0360fbad 100644
--- a/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/compilers/pattern2expr/Pattern2ExprCompiler.kt
+++ b/subprojects/solver/graph-solver/src/main/java/hu/bme/mit/theta/graphsolver/compilers/pattern2expr/Pattern2ExprCompiler.kt
@@ -154,7 +154,7 @@ class Pattern2ExprCompiler : GraphPatternCompiler<Expr<BoolType>, Map<Tuple, Exp
         val opCompiled = pattern.op.accept(this)
         return events.map { a ->
             events.map { b ->
-                Pair(Tuple2.of(a, b), if (a == b) True() else opCompiled[Tuple2.of(a, b)]!!)
+                Pair(Tuple2.of(a, b), if (a == b) True() else checkNotNull(opCompiled[Tuple2.of(a, b)]))
             }
         }.flatten().toMap()
     }
@@ -181,7 +181,8 @@ class Pattern2ExprCompiler : GraphPatternCompiler<Expr<BoolType>, Map<Tuple, Exp
 
     override fun compile(pattern: Inverse): Map<Tuple, Expr<BoolType>> {
         val opCompiled = pattern.op.accept(this)
-        return events.map { a -> events.map { b -> Pair(Tuple2.of(a, b), opCompiled[Tuple2.of(b, a)]!!) } }.flatten()
+        return events.map { a -> events.map { b -> Pair(Tuple2.of(a, b), checkNotNull(opCompiled[Tuple2.of(b, a)])) } }
+            .flatten()
             .toMap()
     }
 
@@ -213,16 +214,16 @@ class Pattern2ExprCompiler : GraphPatternCompiler<Expr<BoolType>, Map<Tuple, Exp
             events.map { b ->
                 Iff(Or(opCompiled[Tuple2.of(a, b)], Or(events.map { c ->
                     Or(
-                        And(opCompiled[Tuple2.of(a, c)], consts[Tuple2.of(c, b)]!!.ref),
-                        And(consts[Tuple2.of(a, c)]!!.ref, opCompiled[Tuple2.of(c, b)])
+                        And(opCompiled[Tuple2.of(a, c)], checkNotNull(consts[Tuple2.of(c, b)]).ref),
+                        And(checkNotNull(consts[Tuple2.of(a, c)]).ref, opCompiled[Tuple2.of(c, b)])
                     )
-                })), consts[Tuple2.of(a, b)]!!.ref)
+                })), checkNotNull(consts[Tuple2.of(a, b)]).ref)
             }
         }.flatten())
         transitiveConstraints.add(constraints)
         val ret = events.map { a ->
             events.map { b ->
-                Pair(Tuple2.of(a, b), if (a == b) True() else consts[Tuple2.of(a, b)]!!.ref)
+                Pair(Tuple2.of(a, b), if (a == b) True() else checkNotNull(consts[Tuple2.of(a, b)]).ref)
             }
         }
         return ret.flatten().toMap()
@@ -249,7 +250,7 @@ class Pattern2ExprCompiler : GraphPatternCompiler<Expr<BoolType>, Map<Tuple, Exp
         val opCompiled = pattern.op.accept(this)
         val ret = events.map { a ->
             events.map { b ->
-                Pair(Tuple2.of(a, b), if (a == b) opCompiled[Tuple1.of(a)]!! else False())
+                Pair(Tuple2.of(a, b), if (a == b) checkNotNull(opCompiled[Tuple1.of(a)]) else False())
             }
         }
         return ret.flatten().toMap()
@@ -276,14 +277,18 @@ class Pattern2ExprCompiler : GraphPatternCompiler<Expr<BoolType>, Map<Tuple, Exp
             events.map { b ->
                 Iff(Or(opCompiled[Tuple2.of(a, b)], Or(events.filter { c -> a != c && b != c }.map { c ->
                     Or(
-                        And(opCompiled[Tuple2.of(a, c)], consts[Tuple2.of(c, b)]!!.ref),
-                        And(consts[Tuple2.of(a, c)]!!.ref, opCompiled[Tuple2.of(c, b)])
+                        And(opCompiled[Tuple2.of(a, c)], checkNotNull(consts[Tuple2.of(c, b)]).ref),
+                        And(checkNotNull(consts[Tuple2.of(a, c)]).ref, opCompiled[Tuple2.of(c, b)])
                     )
-                })), consts[Tuple2.of(a, b)]!!.ref)
+                })), checkNotNull(consts[Tuple2.of(a, b)]).ref)
             }
         }.flatten())
         transitiveConstraints.add(constraints)
-        val ret = events.map { a -> events.map { b -> Pair(Tuple2.of(a, b), consts[Tuple2.of(a, b)]!!.ref) } }
+        val ret = events.map { a ->
+            events.map { b ->
+                Pair(Tuple2.of(a, b), checkNotNull(consts[Tuple2.of(a, b)]).ref)
+            }
+        }
         return ret.flatten().toMap()
     }
 
diff --git a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/Utils.kt b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/Utils.kt
index 0fcfe1ab25..b3db63ef51 100644
--- a/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/Utils.kt
+++ b/subprojects/xcfa/xcfa/src/main/java/hu/bme/mit/theta/xcfa/Utils.kt
@@ -241,10 +241,10 @@ private fun getAtomicBlockInnerLocations(initialLocation: XcfaLocation): List<Xc
     isAtomic[initialLocation] = false
     while (!locationsToVisit.isEmpty()) {
         val visiting = locationsToVisit.removeAt(0)
-        if (isAtomic[visiting]!!) atomicLocations.add(visiting)
+        if (checkNotNull(isAtomic[visiting])) atomicLocations.add(visiting)
         visitedLocations.add(visiting)
         for (outEdge in visiting.outgoingEdges) {
-            var isNextAtomic = isAtomic[visiting]!!
+            var isNextAtomic = checkNotNull(isAtomic[visiting])
             if (outEdge.getFlatLabels().stream().anyMatch { label ->
                     label is FenceLabel && label.labels.contains("ATOMIC_BEGIN")
                 }) {