diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/arg/ArgBuilder.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/arg/ArgBuilder.java
index a21c550fc1..a5371c6916 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/arg/ArgBuilder.java
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/arg/ArgBuilder.java
@@ -42,6 +42,14 @@ private ArgBuilder(
         this.excludeBottom = excludeBottom;
     }
 
+    public Analysis<S, ? super A, ? super P> getAnalysis() {
+        return analysis;
+    }
+
+    public Predicate<? super S> getTarget() {
+        return target;
+    }
+
     public static <S extends State, A extends Action, P extends Prec> ArgBuilder<S, A, P> create(
             final LTS<? super S, A> lts,
             final Analysis<S, ? super A, ? super P> analysis,
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedLtsChecker.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedLtsChecker.java
new file mode 100644
index 0000000000..a6de2ab88f
--- /dev/null
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/bounded/BoundedLtsChecker.java
@@ -0,0 +1,199 @@
+/*
+ *  Copyright 2025 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+package hu.bme.mit.theta.analysis.algorithm.bounded;
+
+import static com.google.common.base.Preconditions.checkNotNull;
+
+import hu.bme.mit.theta.analysis.Analysis;
+import hu.bme.mit.theta.analysis.LTS;
+import hu.bme.mit.theta.analysis.Prec;
+import hu.bme.mit.theta.analysis.Trace;
+import hu.bme.mit.theta.analysis.algorithm.EmptyProof;
+import hu.bme.mit.theta.analysis.algorithm.SafetyChecker;
+import hu.bme.mit.theta.analysis.algorithm.SafetyResult;
+import hu.bme.mit.theta.analysis.expr.ExprAction;
+import hu.bme.mit.theta.analysis.expr.ExprState;
+import hu.bme.mit.theta.core.model.ImmutableValuation;
+import hu.bme.mit.theta.core.type.Expr;
+import hu.bme.mit.theta.core.type.booltype.BoolLitExpr;
+import hu.bme.mit.theta.core.type.booltype.BoolType;
+import hu.bme.mit.theta.core.utils.ExprSimplifier;
+import hu.bme.mit.theta.core.utils.PathUtils;
+import hu.bme.mit.theta.core.utils.indexings.VarIndexing;
+import hu.bme.mit.theta.core.utils.indexings.VarIndexingFactory;
+import hu.bme.mit.theta.solver.Solver;
+import hu.bme.mit.theta.solver.utils.WithPushPop;
+import java.util.ArrayDeque;
+import java.util.Deque;
+import java.util.function.Predicate;
+
+public class BoundedLtsChecker<S extends ExprState, A extends ExprAction, P extends Prec>
+        implements SafetyChecker<EmptyProof, Trace<S, A>, P> {
+    private final Solver solver;
+    private final Analysis<S, A, ? super P> analysis;
+    private final Predicate<? super S> target;
+    private final LTS<? super S, A> lts;
+    private final int bound;
+    private final P defaultPrec;
+    private final Deque<Transition<S, A>> transitions;
+    private final ExprSimplifier simplifier = ExprSimplifier.create();
+
+    public BoundedLtsChecker(
+            LTS<? super S, A> lts,
+            Analysis<S, A, ? super P> analysis,
+            Predicate<? super S> target,
+            int bound,
+            Solver solver) {
+        this(lts, analysis, target, bound, null, solver);
+    }
+
+    public BoundedLtsChecker(
+            LTS<? super S, A> lts,
+            Analysis<S, A, ? super P> analysis,
+            Predicate<? super S> target,
+            int bound,
+            P defaultPrec,
+            Solver solver) {
+        this.solver = solver;
+        this.analysis = analysis;
+        this.target = target;
+        this.lts = lts;
+        this.bound = bound;
+        this.defaultPrec = defaultPrec;
+        transitions = new ArrayDeque<>(bound + 1);
+    }
+
+    private int depth() {
+        return transitions.size();
+    }
+
+    @Override
+    public SafetyResult<EmptyProof, Trace<S, A>> check(P prec) {
+        return doCheck(prec == null ? defaultPrec : prec);
+    }
+
+    private SafetyResult<EmptyProof, Trace<S, A>> doCheck(P prec) {
+        checkNotNull(prec, "No prec provided");
+        var indexing = VarIndexingFactory.indexing(0);
+        boolean safe = true;
+        for (var initialState : analysis.getInitFunc().getInitStates(prec)) {
+            if (initialState.isBottom()) {
+                continue;
+            }
+            try (var wpp = new WithPushPop(solver)) {
+                solver.add(PathUtils.unfold(initialState.toExpr(), indexing));
+                if (!solver.check().isSat()) {
+                    continue;
+                }
+                try {
+                    transitions.addLast(new Transition<>(null, initialState, indexing));
+                    var result = expand(prec);
+                    if (result.isUnsafe()) {
+                        return result;
+                    }
+                    if (!result.isSafe()) {
+                        safe = false;
+                    }
+                } finally {
+                    transitions.removeLast();
+                }
+            }
+        }
+        return getSafeResult(safe);
+    }
+
+    private SafetyResult<EmptyProof, Trace<S, A>> expand(P prec) {
+        var transition = transitions.peekLast();
+        assert transition != null : "No transition available";
+        var state = transition.succState();
+        if (target.test(state)) {
+            return getCex();
+        }
+        if (bound > 0 && depth() > bound) {
+            return SafetyResult.unknown();
+        }
+        var indexing = transition.succIndexing();
+        var actions = lts.getEnabledActionsFor(state);
+        boolean safe = true;
+        for (var action : actions) {
+            try (var wpp = new WithPushPop(solver)) {
+                solver.add(PathUtils.unfold(action.toExpr(), indexing));
+                if (!solver.check().isSat()) {
+                    continue;
+                }
+                var nextIndexing = action.nextIndexing();
+                for (var succState : analysis.getTransFunc().getSuccStates(state, action, prec)) {
+                    if (succState.isBottom()) {
+                        continue;
+                    }
+                    // Simplify the state expressions and do not call the SMT solver if it is
+                    // trivially satisfied. This reduces the number of SMT solver calls with,
+                    // e.g., UnitState, where the state expression is always trivial.
+                    var succExpr =
+                            simplifier.simplify(succState.toExpr(), ImmutableValuation.empty());
+                    boolean needsCheck = !isTrue(succExpr);
+                    if (needsCheck) {
+                        solver.push();
+                    }
+                    try {
+                        var succIndexing = indexing.add(nextIndexing);
+                        if (needsCheck) {
+                            solver.add(PathUtils.unfold(succExpr, succIndexing));
+                            if (!solver.check().isSat()) {
+                                continue;
+                            }
+                        }
+                        try {
+                            transitions.addLast(new Transition<>(action, succState, succIndexing));
+                            var result = expand(prec);
+                            if (result.isUnsafe()) {
+                                return result;
+                            }
+                            if (!result.isSafe()) {
+                                safe = false;
+                            }
+                        } finally {
+                            transitions.removeLast();
+                        }
+                    } finally {
+                        if (needsCheck) {
+                            solver.pop();
+                        }
+                    }
+                }
+            }
+        }
+        return getSafeResult(safe);
+    }
+
+    boolean isTrue(Expr<BoolType> expr) {
+        return expr instanceof BoolLitExpr boolLitExpr && boolLitExpr.getValue();
+    }
+
+    private SafetyResult<EmptyProof, Trace<S, A>> getCex() {
+        var states = transitions.stream().map(Transition::succState).toList();
+        var actions = transitions.stream().skip(1).map(Transition::action).toList();
+        var trace = Trace.of(states, actions);
+        return SafetyResult.unsafe(trace, EmptyProof.getInstance());
+    }
+
+    private SafetyResult<EmptyProof, Trace<S, A>> getSafeResult(boolean safe) {
+        return safe ? SafetyResult.safe(EmptyProof.getInstance()) : SafetyResult.unknown();
+    }
+
+    private record Transition<S extends ExprState, A extends ExprAction>(
+            A action, S succState, VarIndexing succIndexing) {}
+}
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/ArgAbstractor.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/ArgAbstractor.java
index bb692c52e7..36ca20e9d7 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/ArgAbstractor.java
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/ArgAbstractor.java
@@ -19,10 +19,13 @@
 import hu.bme.mit.theta.analysis.Prec;
 import hu.bme.mit.theta.analysis.State;
 import hu.bme.mit.theta.analysis.algorithm.arg.ARG;
+import hu.bme.mit.theta.analysis.algorithm.arg.ArgBuilder;
 
 /**
  * Common interface for the abstractor component. It can create an initial ARG and check an ARG with
  * a given precision.
  */
 public interface ArgAbstractor<S extends State, A extends Action, P extends Prec>
-        extends Abstractor<P, ARG<S, A>> {}
+        extends Abstractor<P, ARG<S, A>> {
+    ArgBuilder<S, A, P> getArgBuilder();
+}
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicArgAbstractor.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicArgAbstractor.java
index 54e37f1971..8e8271a824 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicArgAbstractor.java
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/cegar/BasicArgAbstractor.java
@@ -65,6 +65,11 @@ public static <S extends State, A extends Action, P extends Prec> Builder<S, A,
         return new Builder<>(argBuilder);
     }
 
+    @Override
+    public ArgBuilder<S, A, P> getArgBuilder() {
+        return argBuilder;
+    }
+
     @Override
     public ARG<S, A> createProof() {
         return argBuilder.createArg();
diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/ptr/PtrUtils.kt b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/ptr/PtrUtils.kt
index b090884c49..86965989fb 100644
--- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/ptr/PtrUtils.kt
+++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/ptr/PtrUtils.kt
@@ -22,6 +22,8 @@ import hu.bme.mit.theta.analysis.expl.ExplState
 import hu.bme.mit.theta.analysis.expr.ExprState
 import hu.bme.mit.theta.analysis.pred.PredPrec
 import hu.bme.mit.theta.analysis.pred.PredState
+import hu.bme.mit.theta.analysis.unit.UnitPrec
+import hu.bme.mit.theta.analysis.unit.UnitState
 import hu.bme.mit.theta.core.decl.VarDecl
 import hu.bme.mit.theta.core.stmt.*
 import hu.bme.mit.theta.core.stmt.Stmts.Assume
@@ -208,6 +210,7 @@ fun <S : ExprState> S.patch(writeTriples: WriteTriples): S =
   when (this) {
     is PredState -> PredState.of(preds.map { it.patch(writeTriples) }) as S
     is ExplState -> this
+    is UnitState -> this
     is PtrState<*> ->
       (this as PtrState<ExprState>).copy(innerState = innerState.patch(writeTriples)) as S
     else -> error("State $this is not supported")
@@ -217,6 +220,7 @@ fun <P : Prec> P.patch(writeTriples: WriteTriples): P =
   when (this) {
     is PredPrec -> PredPrec.of(preds.map { it.patch(writeTriples) }) as P
     is ExplPrec -> this
+    is UnitPrec -> this
     else -> error("Prec $this is not supported")
   }
 
@@ -231,6 +235,7 @@ fun <P : Prec> P.repatch(): P =
   when (this) {
     is PredPrec -> PredPrec.of(preds.map { it.repatch() }) as P
     is ExplPrec -> this
+    is UnitPrec -> this
     else -> error("Prec $this is not supported")
   }
 
@@ -238,6 +243,7 @@ fun <S : ExprState> S.repatch(): S =
   when (this) {
     is PredState -> PredState.of(preds.map(Expr<BoolType>::repatch)) as S
     is ExplState -> this
+    is UnitState -> this
     else -> error("State $this is not supported")
   }
 
diff --git a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt
index fab0b8df5d..4f9f19de17 100644
--- a/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt
+++ b/subprojects/xcfa/xcfa-analysis/src/main/java/hu/bme/mit/theta/xcfa/analysis/XcfaAnalysis.kt
@@ -18,6 +18,7 @@ package hu.bme.mit.theta.xcfa.analysis
 import hu.bme.mit.theta.analysis.*
 import hu.bme.mit.theta.analysis.algorithm.arg.ArgBuilder
 import hu.bme.mit.theta.analysis.algorithm.arg.ArgNode
+import hu.bme.mit.theta.analysis.algorithm.bounded.BoundedLtsChecker
 import hu.bme.mit.theta.analysis.algorithm.cegar.ArgAbstractor
 import hu.bme.mit.theta.analysis.algorithm.cegar.abstractor.StopCriterion
 import hu.bme.mit.theta.analysis.expl.ExplInitFunc
@@ -32,7 +33,9 @@ import hu.bme.mit.theta.analysis.pred.PredAbstractors.PredAbstractor
 import hu.bme.mit.theta.analysis.ptr.PtrPrec
 import hu.bme.mit.theta.analysis.ptr.PtrState
 import hu.bme.mit.theta.analysis.ptr.getPtrInitFunc
+import hu.bme.mit.theta.analysis.ptr.getPtrPartialOrd
 import hu.bme.mit.theta.analysis.ptr.getPtrTransFunc
+import hu.bme.mit.theta.analysis.unit.*
 import hu.bme.mit.theta.analysis.waitlist.Waitlist
 import hu.bme.mit.theta.common.Try
 import hu.bme.mit.theta.common.logging.Logger
@@ -431,3 +434,83 @@ class PredXcfaAnalysis(
     coreInitFunc = getPredXcfaInitFunc(xcfa, predAbstractor),
     coreTransFunc = getPredXcfaTransFunc(predAbstractor, isHavoc),
   )
+
+private fun getUnitXcfaPartialOrd(xcfa: XCFA): PartialOrd<XcfaState<PtrState<UnitState>>> {
+  val ptrPartialOrd = UnitAnalysis.getInstance().partialOrd.getPtrPartialOrd()
+  return if (xcfa.isInlined) {
+    getPartialOrder(ptrPartialOrd)
+  } else {
+    getStackPartialOrder(ptrPartialOrd)
+  }
+}
+
+private fun getUnitXcfaInitFunc(
+  xcfa: XCFA
+): (XcfaPrec<PtrPrec<UnitPrec>>) -> List<XcfaState<PtrState<UnitState>>> {
+  val processInitState =
+    xcfa.initProcedures
+      .mapIndexed { i, it ->
+        val initLocStack: LinkedList<XcfaLocation> = LinkedList()
+        initLocStack.add(it.first.initLoc)
+        Pair(
+          i,
+          XcfaProcessState(
+            initLocStack,
+            prefix = "T$i",
+            varLookup = LinkedList(listOf(createLookup(it.first, "T$i", ""))),
+          ),
+        )
+      }
+      .toMap()
+  return { p ->
+    InitFunc<UnitState, UnitPrec> { _ -> listOf(UnitState.getInstance()) }
+      .getPtrInitFunc()
+      .getInitStates(p.p)
+      .map { XcfaState(xcfa, processInitState, it) }
+  }
+}
+
+private fun getUnitXcfaTransFunc(
+  isHavoc: Boolean
+): (XcfaState<PtrState<UnitState>>, XcfaAction, XcfaPrec<PtrPrec<UnitPrec>>) -> List<
+    XcfaState<PtrState<UnitState>>
+  > {
+  val unitTransFunc =
+    TransFunc<UnitState, ExprAction, UnitPrec> { s, _, _ -> listOf(s) }.getPtrTransFunc(isHavoc)
+  return { s, a, p ->
+    val (newSt, newAct) = s.apply(a)
+    unitTransFunc.getSuccStates(s.sGlobal, newAct, p.p).map { newSt.withState(it) }
+  }
+}
+
+class UnitXcfaAnalysis(xcfa: XCFA, isHavoc: Boolean) :
+  XcfaAnalysis<UnitState, PtrPrec<UnitPrec>>(
+    corePartialOrd = getUnitXcfaPartialOrd(xcfa),
+    coreInitFunc = getUnitXcfaInitFunc(xcfa),
+    coreTransFunc = getUnitXcfaTransFunc(isHavoc),
+  )
+
+fun getBoundedXcfaChecker(
+  xcfa: XCFA,
+  errorDetection: ErrorDetection,
+  bound: Int,
+  solver: Solver,
+  isHavoc: Boolean = false,
+): BoundedLtsChecker<XcfaState<PtrState<UnitState>>, XcfaAction, XcfaPrec<PtrPrec<UnitPrec>>> {
+  val lts = getXcfaLts()
+  return getBoundedXcfaChecker(xcfa, lts, errorDetection, bound, solver, isHavoc)
+}
+
+fun getBoundedXcfaChecker(
+  xcfa: XCFA,
+  lts: LTS<XcfaState<out PtrState<out ExprState>>, XcfaAction>,
+  errorDetection: ErrorDetection,
+  bound: Int,
+  solver: Solver,
+  isHavoc: Boolean = false,
+): BoundedLtsChecker<XcfaState<PtrState<UnitState>>, XcfaAction, XcfaPrec<PtrPrec<UnitPrec>>> {
+  val analysis = UnitXcfaAnalysis(xcfa, isHavoc)
+  val target = getXcfaErrorPredicate(errorDetection)
+  val prec = XcfaPrec(PtrPrec(UnitPrec.getInstance()))
+  return BoundedLtsChecker(lts, analysis, target, bound, prec, solver)
+}
diff --git a/subprojects/xcfa/xcfa-analysis/src/test/java/hu/bme/mit/theta/xcfa/analysis/XcfaUnitAnalysisTest.kt b/subprojects/xcfa/xcfa-analysis/src/test/java/hu/bme/mit/theta/xcfa/analysis/XcfaUnitAnalysisTest.kt
new file mode 100644
index 0000000000..81e59596f7
--- /dev/null
+++ b/subprojects/xcfa/xcfa-analysis/src/test/java/hu/bme/mit/theta/xcfa/analysis/XcfaUnitAnalysisTest.kt
@@ -0,0 +1,81 @@
+/*
+ *  Copyright 2025 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+package hu.bme.mit.theta.xcfa.analysis
+
+import hu.bme.mit.theta.analysis.algorithm.SafetyResult
+import hu.bme.mit.theta.c2xcfa.getXcfaFromC
+import hu.bme.mit.theta.common.logging.NullLogger
+import hu.bme.mit.theta.frontend.ParseContext
+import hu.bme.mit.theta.solver.z3legacy.Z3LegacySolverFactory
+import hu.bme.mit.theta.xcfa.analysis.coi.ConeOfInfluence
+import hu.bme.mit.theta.xcfa.analysis.coi.XcfaCoiMultiThread
+import hu.bme.mit.theta.xcfa.analysis.por.XcfaSporLts
+import org.junit.jupiter.api.Assertions
+import org.junit.jupiter.params.ParameterizedTest
+import org.junit.jupiter.params.provider.MethodSource
+
+class XcfaUnitAnalysisTest {
+
+  companion object {
+    @JvmStatic
+    fun data(): Collection<Array<Any>> {
+      return listOf(
+        arrayOf("/00assignment.c", 8, SafetyResult<*, *>::isUnsafe),
+        arrayOf("/00assignment.c", 2, this::isUnknown),
+        arrayOf("/01function.c", 16, SafetyResult<*, *>::isUnsafe),
+        arrayOf("/02functionparam.c", 16, SafetyResult<*, *>::isSafe),
+        arrayOf("/03nondetfunction.c", 16, SafetyResult<*, *>::isUnsafe),
+        arrayOf("/04multithread.c", 40, SafetyResult<*, *>::isUnsafe),
+        arrayOf("/05assignment_safe.c", 16, SafetyResult<*, *>::isSafe),
+        arrayOf("/05assignment_safe.c", 2, this::isUnknown),
+      )
+    }
+
+    private fun isUnknown(safetyResult: SafetyResult<*, *>) =
+      !safetyResult.isSafe && !safetyResult.isUnsafe
+  }
+
+  @ParameterizedTest
+  @MethodSource("data")
+  fun testNoporBounded(filepath: String, bound: Int, verdict: (SafetyResult<*, *>) -> Boolean) {
+    println("Testing NOPOR on $filepath...")
+    val stream = javaClass.getResourceAsStream(filepath)
+    val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first
+    ConeOfInfluence = XcfaCoiMultiThread(xcfa)
+
+    val solver = Z3LegacySolverFactory.getInstance().createSolver()
+    val checker = getBoundedXcfaChecker(xcfa, ErrorDetection.ERROR_LOCATION, bound, solver)
+    val safetyResult = checker.check()
+
+    Assertions.assertTrue(verdict(safetyResult))
+  }
+
+  @ParameterizedTest
+  @MethodSource("data")
+  fun testSporBounded(filepath: String, bound: Int, verdict: (SafetyResult<*, *>) -> Boolean) {
+    println("Testing SPOR on $filepath...")
+    val stream = javaClass.getResourceAsStream(filepath)
+    val xcfa = getXcfaFromC(stream!!, ParseContext(), false, false, NullLogger.getInstance()).first
+    ConeOfInfluence = XcfaCoiMultiThread(xcfa)
+    val lts = XcfaSporLts(xcfa)
+
+    val solver = Z3LegacySolverFactory.getInstance().createSolver()
+    val checker = getBoundedXcfaChecker(xcfa, lts, ErrorDetection.ERROR_LOCATION, bound, solver)
+    val safetyResult = checker.check()
+
+    Assertions.assertTrue(verdict(safetyResult))
+  }
+}
diff --git a/subprojects/xcfa/xcfa-analysis/src/test/resources/05assignment_safe.c b/subprojects/xcfa/xcfa-analysis/src/test/resources/05assignment_safe.c
new file mode 100644
index 0000000000..106077f85c
--- /dev/null
+++ b/subprojects/xcfa/xcfa-analysis/src/test/resources/05assignment_safe.c
@@ -0,0 +1,5 @@
+void reach_error(){}
+int main() {
+    int a = 1;
+    if(!a) reach_error();
+}
\ No newline at end of file
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 43e3c5f00c..c34ac324e1 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
@@ -107,6 +107,13 @@ private fun propagateInputOptions(config: XcfaConfig<*, *>, logger: Logger, uniq
     XcfaSporLts.random = random
     XcfaDporLts.random = random
   }
+  if (config.backendConfig.backend == Backend.PATH_ENUMERATION) {
+    val pathEnumerationConfig = config.backendConfig.specConfig
+    pathEnumerationConfig as PathEnumerationConfig
+    val random = Random(pathEnumerationConfig.porRandomSeed)
+    XcfaSporLts.random = random
+    XcfaDporLts.random = random
+  }
   if (
     config.inputConfig.property == ErrorDetection.MEMSAFETY ||
       config.inputConfig.property == ErrorDetection.MEMCLEANUP
@@ -130,10 +137,21 @@ private fun validateInputOptions(config: XcfaConfig<*, *>, logger: Logger, uniqu
       (config.backendConfig.specConfig as? CegarConfig)?.coi != ConeOfInfluenceMode.NO_COI &&
       config.inputConfig.property == ErrorDetection.DATA_RACE
   }
+  rule("NoCoiWhenDataRacePathEnumeration") {
+    config.backendConfig.backend == Backend.PATH_ENUMERATION &&
+      (config.backendConfig.specConfig as? PathEnumerationConfig)?.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
   }
+  rule("NoAaporOrDporPathEnumeration") {
+    (config.backendConfig.specConfig as? PathEnumerationConfig)?.porLevel.let {
+      it != null && (it.isAbstractionAware || it.isDynamic)
+    }
+  }
   rule("DPORWithoutDFS") {
     (config.backendConfig.specConfig as? CegarConfig)?.porLevel?.isDynamic == true &&
       (config.backendConfig.specConfig as? CegarConfig)?.abstractorConfig?.search != Search.DFS
diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToChecker.kt
index 066406df7f..ddaf042d92 100644
--- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToChecker.kt
+++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToChecker.kt
@@ -51,6 +51,7 @@ fun getChecker(
       Backend.IMC,
       Backend.KINDIMC,
       Backend.BOUNDED -> getBoundedChecker(xcfa, parseContext, config, logger)
+      Backend.PATH_ENUMERATION -> getPathEnumerationChecker(xcfa, config, logger)
       Backend.OC -> getOcChecker(xcfa, mcm, config, logger)
       Backend.LAZY -> TODO()
       Backend.PORTFOLIO ->
diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToPathEnumerationChecker.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToPathEnumerationChecker.kt
new file mode 100644
index 0000000000..af92583f0b
--- /dev/null
+++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/checkers/ConfigToPathEnumerationChecker.kt
@@ -0,0 +1,116 @@
+/*
+ *  Copyright 2025 Budapest University of Technology and Economics
+ *
+ *  Licensed under the Apache License, Version 2.0 (the "License");
+ *  you may not use this file except in compliance with the License.
+ *  You may obtain a copy of the License at
+ *
+ *      http://www.apache.org/licenses/LICENSE-2.0
+ *
+ *  Unless required by applicable law or agreed to in writing, software
+ *  distributed under the License is distributed on an "AS IS" BASIS,
+ *  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+ *  See the License for the specific language governing permissions and
+ *  limitations under the License.
+ */
+package hu.bme.mit.theta.xcfa.cli.checkers
+
+import hu.bme.mit.theta.analysis.Analysis
+import hu.bme.mit.theta.analysis.PartialOrd
+import hu.bme.mit.theta.analysis.Prec
+import hu.bme.mit.theta.analysis.Trace
+import hu.bme.mit.theta.analysis.algorithm.EmptyProof
+import hu.bme.mit.theta.analysis.algorithm.SafetyChecker
+import hu.bme.mit.theta.analysis.algorithm.bounded.BoundedLtsChecker
+import hu.bme.mit.theta.analysis.algorithm.cegar.ArgAbstractor
+import hu.bme.mit.theta.analysis.algorithm.cegar.abstractor.StopCriterions
+import hu.bme.mit.theta.analysis.expr.ExprState
+import hu.bme.mit.theta.analysis.ptr.PtrPrec
+import hu.bme.mit.theta.analysis.ptr.PtrState
+import hu.bme.mit.theta.analysis.waitlist.PriorityWaitlist
+import hu.bme.mit.theta.common.logging.Logger
+import hu.bme.mit.theta.core.decl.VarDecl
+import hu.bme.mit.theta.solver.SolverFactory
+import hu.bme.mit.theta.xcfa.analysis.*
+import hu.bme.mit.theta.xcfa.cli.params.PathEnumerationConfig
+import hu.bme.mit.theta.xcfa.cli.params.XcfaConfig
+import hu.bme.mit.theta.xcfa.cli.utils.getSolver
+import hu.bme.mit.theta.xcfa.dereferences
+import hu.bme.mit.theta.xcfa.model.XCFA
+
+fun getPathEnumerationChecker(
+  xcfa: XCFA,
+  config: XcfaConfig<*, *>,
+  logger: Logger,
+): SafetyChecker<
+  EmptyProof,
+  Trace<XcfaState<PtrState<ExprState>>, XcfaAction>,
+  XcfaPrec<PtrPrec<Prec>>,
+> {
+  val pathEnumerationConfig = config.backendConfig.specConfig as PathEnumerationConfig
+  if (
+    config.inputConfig.property == ErrorDetection.DATA_RACE &&
+      xcfa.procedures.any { it.edges.any { it.label.dereferences.isNotEmpty() } }
+  ) {
+    throw RuntimeException("DATA_RACE cannot be checked when pointers exist in the file.")
+  }
+  if (pathEnumerationConfig.porLevel.isDynamic) {
+    throw RuntimeException("Path enumeration does not support DPOR.")
+  }
+  if (pathEnumerationConfig.porLevel.isAbstractionAware) {
+    throw RuntimeException("Path enumeration does not support AAPOR.")
+  }
+  val pathEnumerationSolverFactory: SolverFactory =
+    getSolver(
+      pathEnumerationConfig.pathEnumerationSolver,
+      pathEnumerationConfig.validatePathEnumerationSolver,
+    )
+  val abstractionSolverFactory: SolverFactory =
+    getSolver(
+      pathEnumerationConfig.abstractionSolver,
+      pathEnumerationConfig.validateAbstractionSolver,
+    )
+
+  val ignoredVarRegistry = mutableMapOf<VarDecl<*>, MutableSet<ExprState>>()
+  val lts =
+    pathEnumerationConfig.coi.getLts(xcfa, ignoredVarRegistry, pathEnumerationConfig.porLevel)
+
+  val abstractionSolverInstance = abstractionSolverFactory.createSolver()
+  val globalStatePartialOrd =
+    pathEnumerationConfig.domain.partialOrd(abstractionSolverInstance)
+      as PartialOrd<PtrState<ExprState>>
+  val corePartialOrd: PartialOrd<XcfaState<PtrState<ExprState>>> =
+    if (xcfa.isInlined) getPartialOrder(globalStatePartialOrd)
+    else getStackPartialOrder(globalStatePartialOrd)
+  val abstractor =
+    pathEnumerationConfig.domain.abstractor(
+      xcfa,
+      abstractionSolverInstance,
+      pathEnumerationConfig.maxEnum,
+      PriorityWaitlist.create(),
+      StopCriterions.fullExploration(),
+      logger,
+      lts,
+      config.inputConfig.property,
+      corePartialOrd,
+      pathEnumerationConfig.havocMemory,
+    ) as ArgAbstractor<XcfaState<PtrState<ExprState>>, XcfaAction, XcfaPrec<PtrPrec<Prec>>>
+  val argBuilder = abstractor.argBuilder
+  val analysis =
+    argBuilder.analysis
+      as Analysis<XcfaState<PtrState<ExprState>>, XcfaAction, XcfaPrec<PtrPrec<Prec>>>
+  val target = argBuilder.target
+  val prec =
+    pathEnumerationConfig.domain.initPrec(xcfa, pathEnumerationConfig.initPrec)
+      as XcfaPrec<PtrPrec<Prec>>
+
+  val pathEnumerationSolverInstance = pathEnumerationSolverFactory.createSolver()
+  return BoundedLtsChecker(
+    lts,
+    analysis,
+    target,
+    pathEnumerationConfig.maxBound,
+    prec,
+    pathEnumerationSolverInstance,
+  )
+}
diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ParamValues.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ParamValues.kt
index a945a0c05b..52720bf16e 100644
--- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ParamValues.kt
+++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ParamValues.kt
@@ -37,6 +37,9 @@ import hu.bme.mit.theta.analysis.ptr.ItpRefToPtrPrec
 import hu.bme.mit.theta.analysis.ptr.PtrPrec
 import hu.bme.mit.theta.analysis.ptr.PtrState
 import hu.bme.mit.theta.analysis.ptr.getPtrPartialOrd
+import hu.bme.mit.theta.analysis.unit.UnitAnalysis
+import hu.bme.mit.theta.analysis.unit.UnitPrec
+import hu.bme.mit.theta.analysis.unit.UnitState
 import hu.bme.mit.theta.analysis.waitlist.Waitlist
 import hu.bme.mit.theta.common.logging.Logger
 import hu.bme.mit.theta.core.decl.VarDecl
@@ -70,6 +73,7 @@ enum class Backend {
   KIND,
   IMC,
   KINDIMC,
+  PATH_ENUMERATION,
   CHC,
   OC,
   LAZY,
@@ -234,6 +238,26 @@ enum class Domain(
     nodePruner = AtomicNodePruner<XcfaState<PtrState<PredState>>, XcfaAction>(),
     stateType = TypeToken.get(PredState::class.java).type,
   ),
+  UNIT(
+    abstractor = { a, b, c, d, e, f, g, h, i, j ->
+      getXcfaAbstractor(UnitXcfaAnalysis(a, j), d, e, f, g, h)
+    },
+    itpPrecRefiner = {
+      XcfaPrecRefiner<PtrState<UnitState>, UnitPrec, ItpRefutation>(
+        ItpRefToPtrPrec(
+          object : RefutationToPrec<UnitPrec, ItpRefutation> {
+            override fun join(prec1: UnitPrec?, prec2: UnitPrec?) = UnitPrec.getInstance()
+
+            override fun toPrec(refutation: ItpRefutation?, index: Int) = UnitPrec.getInstance()
+          }
+        )
+      )
+    },
+    initPrec = { _, _ -> XcfaPrec(PtrPrec(UnitPrec.getInstance())) },
+    partialOrd = { UnitAnalysis.getInstance().partialOrd.getPtrPartialOrd() },
+    nodePruner = AtomicNodePruner<XcfaState<PtrState<UnitState>>, XcfaAction>(),
+    stateType = TypeToken.get(UnitState::class.java).type,
+  ),
 }
 
 enum class Refinement(
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 546a49821c..cb4e907879 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
@@ -216,6 +216,7 @@ data class BackendConfig<T : SpecBackendConfig>(
             as T
         Backend.KINDIMC -> BoundedConfig() as T
         Backend.BOUNDED -> BoundedConfig() as T
+        Backend.PATH_ENUMERATION -> PathEnumerationConfig() as T
         Backend.CHC -> HornConfig() as T
         Backend.OC -> OcConfig() as T
         Backend.LAZY -> null
@@ -573,3 +574,44 @@ data class DebugConfig(
   )
   var argToFile: Boolean = false,
 ) : Config
+
+data class PathEnumerationConfig(
+  @Parameter(names = ["--path-enumeration-solver"], description = "Path enumeration solver name")
+  var pathEnumerationSolver: String = "Z3",
+  @Parameter(
+    names = ["--validate-path-enumeration-solver"],
+    description =
+      "Activates a wrapper, which validates the assertions in the solver in each (SAT) check. Filters some solver issues.",
+  )
+  var validatePathEnumerationSolver: Boolean = false,
+  @Parameter(names = ["--max-bound"], description = "Maximum bound to check. Use 0 for no limit.")
+  var maxBound: Int = 0,
+  @Parameter(names = ["--prec"], description = "Precision") var initPrec: InitPrec = InitPrec.EMPTY,
+  @Parameter(names = ["--por-level"], description = "POR dependency level")
+  var porLevel: POR = POR.NOPOR,
+  @Parameter(names = ["--por-seed"], description = "Random seed used for DPOR")
+  var porRandomSeed: Int = -1,
+  @Parameter(names = ["--coi"], description = "Enable ConeOfInfluence")
+  var coi: ConeOfInfluenceMode = ConeOfInfluenceMode.NO_COI,
+  @Parameter(names = ["--abstraction-solver"], description = "Abstraction solver name")
+  var abstractionSolver: String = "Z3",
+  @Parameter(
+    names = ["--validate-abstraction-solver"],
+    description =
+      "Activates a wrapper, which validates the assertions in the solver in each (SAT) check. Filters some solver issues.",
+  )
+  var validateAbstractionSolver: Boolean = false,
+  @Parameter(names = ["--domain"], description = "Abstraction domain")
+  var domain: Domain = Domain.UNIT,
+  @Parameter(
+    names = ["--maxenum"],
+    description =
+      "How many successors to enumerate in a transition. Only relevant to the explicit domain. Use 0 for no limit.",
+  )
+  var maxEnum: Int = 1,
+  @Parameter(
+    names = ["--havoc-memory"],
+    description = "HAVOC memory model (do not track pointers in transition function)",
+  )
+  var havocMemory: Boolean = false,
+) : SpecBackendConfig