diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java
index 337032b176..a5f79f1502 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/configuration/OptionNames.java
@@ -36,7 +36,7 @@ public class OptionNames {
     public static final String REDUCE_SYMMETRY = "program.processing.reduceSymmetry";
     public static final String CONSTANT_PROPAGATION = "program.processing.constantPropagation";
     public static final String DEAD_ASSIGNMENT_ELIMINATION = "program.processing.dce";
-    public static final String DYNAMIC_PURE_LOOP_CUTTING = "program.processing.dplc";
+    public static final String DYNAMIC_SPINLOOP_DETECTION = "program.processing.spinloops";
     public static final String PROPAGATE_COPY_ASSIGNMENTS = "program.processing.propagateCopyAssignments";
     public static final String REMOVE_ASSERTION_OF_TYPE = "program.processing.skipAssertionsOfType";
 
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java
index bf5dd071f7..023a3d3b72 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/PropertyEncoder.java
@@ -414,7 +414,7 @@ in a deadlock without satisfying the stated conditions (e.g., while producing si
     */
     private class LivenessEncoder {
 
-        private class SpinIteration {
+        private static class SpinIteration {
             public final List<Load> containedLoads = new ArrayList<>();
             // Execution of the <boundJump> means the loop performed a side-effect-free
             // iteration without exiting. If such a jump is executed + all loads inside the loop
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/DominatorAnalysis.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/DominatorAnalysis.java
new file mode 100644
index 0000000000..3e62fa93a0
--- /dev/null
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/analysis/DominatorAnalysis.java
@@ -0,0 +1,54 @@
+package com.dat3m.dartagnan.program.analysis;
+
+import com.dat3m.dartagnan.program.IRHelper;
+import com.dat3m.dartagnan.program.event.Event;
+import com.dat3m.dartagnan.program.event.core.CondJump;
+import com.dat3m.dartagnan.program.event.core.Label;
+import com.dat3m.dartagnan.utils.DominatorTree;
+import com.google.common.base.Preconditions;
+import com.google.common.base.Predicate;
+import com.google.common.collect.Iterables;
+import com.google.common.collect.Sets;
+
+import java.util.List;
+import java.util.Set;
+
+public class DominatorAnalysis {
+
+    public static DominatorTree<Event> computePreDominatorTree(Event from, Event to) {
+        Preconditions.checkArgument(from.getFunction() == to.getFunction(),
+                "Cannot compute dominator tree between events of different functions.");
+        final Predicate<Event> isInRange = (e -> from.getGlobalId() <= e.getGlobalId() && e.getGlobalId() <= to.getGlobalId());
+        return new DominatorTree<>(from, e -> Iterables.filter(getSuccessors(e), isInRange));
+    }
+
+    public static DominatorTree<Event> computePostDominatorTree(Event from, Event to) {
+        Preconditions.checkArgument(from.getFunction() == to.getFunction(),
+                "Cannot compute dominator tree between events of different functions.");
+        final Predicate<Event> isInRange = (e -> from.getGlobalId() <= e.getGlobalId() && e.getGlobalId() <= to.getGlobalId());
+        return new DominatorTree<>(to, e -> Iterables.filter(getPredecessors(e), isInRange));
+    }
+
+    // ==============================================================================================================
+    // Internals
+
+    private static Iterable<? extends Event> getSuccessors(Event e) {
+        final boolean hasSucc = (e.getSuccessor() != null && !IRHelper.isAlwaysBranching(e));
+        if (e instanceof CondJump jump) {
+            return hasSucc ? List.of(jump.getSuccessor(), jump.getLabel()) : List.of(jump.getLabel());
+        } else {
+            return hasSucc ? List.of(e.getSuccessor()) : List.of();
+        }
+    }
+
+    private static Iterable<? extends Event> getPredecessors(Event e) {
+        final boolean hasPred = (e.getPredecessor() != null && !IRHelper.isAlwaysBranching(e.getPredecessor()));
+        if (e instanceof Label label) {
+            return hasPred ? Sets.union(label.getJumpSet(), Set.of(e.getPredecessor())) : label.getJumpSet();
+        } else {
+            return hasPred ? List.of(e.getPredecessor()) : List.of();
+        }
+    }
+
+
+}
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicPureLoopCutting.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicPureLoopCutting.java
deleted file mode 100644
index 382dfeb82b..0000000000
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicPureLoopCutting.java
+++ /dev/null
@@ -1,361 +0,0 @@
-package com.dat3m.dartagnan.program.processing;
-
-import com.dat3m.dartagnan.expression.Expression;
-import com.dat3m.dartagnan.expression.ExpressionFactory;
-import com.dat3m.dartagnan.expression.Type;
-import com.dat3m.dartagnan.expression.type.TypeFactory;
-import com.dat3m.dartagnan.program.Function;
-import com.dat3m.dartagnan.program.Program;
-import com.dat3m.dartagnan.program.Register;
-import com.dat3m.dartagnan.program.Thread;
-import com.dat3m.dartagnan.program.analysis.LoopAnalysis;
-import com.dat3m.dartagnan.program.event.*;
-import com.dat3m.dartagnan.program.event.core.CondJump;
-import com.dat3m.dartagnan.program.event.core.Label;
-import com.dat3m.dartagnan.program.event.functions.FunctionCall;
-import com.dat3m.dartagnan.program.event.metadata.UnrollingId;
-import com.google.common.base.Preconditions;
-import com.google.common.base.Verify;
-import com.google.common.collect.Iterables;
-import com.google.common.collect.Lists;
-import com.google.common.collect.Maps;
-import com.google.common.collect.Sets;
-import org.apache.logging.log4j.LogManager;
-import org.apache.logging.log4j.Logger;
-import org.sosy_lab.common.configuration.Configuration;
-
-import java.util.*;
-import java.util.function.BiPredicate;
-import java.util.stream.Collectors;
-import java.util.stream.IntStream;
-
-/*
-    This pass instruments loops that do not cause a side effect in an iteration to terminate, i.e., to avoid spinning.
-    In other words, only the last loop iteration is allowed to be side-effect free.
-
-    NOTE: This pass is required to detect liveness violations.
- */
-public class DynamicPureLoopCutting implements ProgramProcessor, FunctionProcessor {
-
-    private static final Logger logger = LogManager.getLogger(DynamicPureLoopCutting.class);
-
-    public static DynamicPureLoopCutting fromConfig(Configuration config) {
-        return new DynamicPureLoopCutting();
-    }
-
-    /*
-        We attach additional data to loop iterations for processing.
-     */
-    private static class IterationData {
-        private LoopAnalysis.LoopIterationInfo iterationInfo;
-        private final List<Event> sideEffects = new ArrayList<>();
-        private final List<Event> guaranteedExitPoints = new ArrayList<>();
-        private boolean isAlwaysSideEffectFull = false;
-    }
-
-    private record AnalysisStats(int numPotentialSpinLoops, int numStaticSpinLoops) {
-
-        private AnalysisStats add(AnalysisStats stats) {
-            return new AnalysisStats(this.numPotentialSpinLoops + stats.numPotentialSpinLoops,
-                    this.numStaticSpinLoops + stats.numStaticSpinLoops);
-        }
-    }
-
-    @Override
-    public void run(Program program) {
-        Preconditions.checkArgument(program.isCompiled(),
-                "DynamicPureLoopCutting can only be run on compiled programs.");
-
-        AnalysisStats stats = new AnalysisStats(0, 0);
-        final LoopAnalysis loopAnalysis = LoopAnalysis.newInstance(program);
-        for (Function func : Iterables.concat(program.getThreads(), program.getFunctions())) {
-            final List<IterationData> iterationData = computeIterationDataList(func, loopAnalysis);
-            iterationData.forEach(this::reduceToDominatingSideEffects);
-            iterationData.forEach(this::insertSideEffectChecks);
-            stats = stats.add(collectStats(iterationData));
-        }
-
-        // NOTE: We log "potential spin loops" as only those that are not also "static".
-        logger.info("Found {} static spin loops and {} potential spin loops.",
-                stats.numStaticSpinLoops, (stats.numPotentialSpinLoops - stats.numStaticSpinLoops));
-    }
-
-    @Override
-    public void run(Function function) {
-        final LoopAnalysis loopAnalysis = LoopAnalysis.onFunction(function);
-        final List<IterationData> iterationData = computeIterationDataList(function, loopAnalysis);
-        iterationData.forEach(this::reduceToDominatingSideEffects);
-        iterationData.forEach(this::insertSideEffectChecks);
-    }
-
-    private AnalysisStats collectStats(List<IterationData> iterDataList) {
-        int numPotentialSpinLoops = 0;
-        int numStaticSpinLoops = 0;
-        Set<UnrollingId> alreadyDetectedLoops = new HashSet<>(); // To avoid counting the same loop multiple times
-        for (IterationData data : iterDataList) {
-            if (!data.isAlwaysSideEffectFull) {
-                // Potential spinning iteration
-                final UnrollingId uIdOfLoop = data.iterationInfo.getIterationStart().getMetadata(UnrollingId.class);
-                assert uIdOfLoop != null;
-                if (alreadyDetectedLoops.add(uIdOfLoop)) {
-                    // A loop we did not count before
-                    numPotentialSpinLoops++;
-                    if (data.sideEffects.isEmpty()) {
-                        numStaticSpinLoops++;
-                    }
-                }
-            }
-        }
-        return new AnalysisStats(numPotentialSpinLoops, numStaticSpinLoops);
-    }
-
-    private void insertSideEffectChecks(IterationData iter) {
-        if (iter.isAlwaysSideEffectFull) {
-            // No need to insert checks if the iteration is guaranteed to have side effects
-            return;
-        }
-        final LoopAnalysis.LoopIterationInfo iterInfo = iter.iterationInfo;
-        final Function func = iterInfo.getContainingLoop().function();
-        final int loopNumber = iterInfo.getContainingLoop().loopNumber();
-        final int iterNumber = iterInfo.getIterationNumber();
-        final List<Event> sideEffects = iter.sideEffects;
-
-        final List<Register> trackingRegs = new ArrayList<>();
-        final Type type = TypeFactory.getInstance().getBooleanType();
-        Event insertionPoint = iterInfo.getIterationEnd();
-        for (int i = 0; i < sideEffects.size(); i++) {
-            final Event sideEffect = sideEffects.get(i);
-            final Register trackingReg = func.newRegister(String.format("Loop%s_%s_%s", loopNumber, iterNumber, i), type);
-            trackingRegs.add(trackingReg);
-
-            final Event execCheck = EventFactory.newExecutionStatus(trackingReg, sideEffect);
-            insertionPoint.insertAfter(execCheck);
-            insertionPoint = execCheck;
-        }
-
-        final ExpressionFactory expressionFactory = ExpressionFactory.getInstance();
-        final Expression noSideEffect = trackingRegs.stream()
-                .map(Expression.class::cast)
-                .reduce(expressionFactory.makeTrue(), expressionFactory::makeAnd);
-        final Event assumeSideEffect = newSpinTerminator(noSideEffect, func);
-        assumeSideEffect.addTags(Tag.SPINLOOP, Tag.EARLYTERMINATION, Tag.NOOPT);
-        final Event spinloopStart = iterInfo.getIterationStart();
-        assumeSideEffect.copyAllMetadataFrom(spinloopStart);
-        insertionPoint.insertAfter(assumeSideEffect);
-    }
-
-    private Event newSpinTerminator(Expression guard, Function func) {
-        return func instanceof Thread thread ?
-                EventFactory.newJump(guard, (Label) thread.getExit())
-                : EventFactory.newAbortIf(guard);
-    }
-
-    // ============================= Actual logic =============================
-
-    private List<IterationData> computeIterationDataList(Function function, LoopAnalysis loopAnalysis) {
-        final List<IterationData> dataList = loopAnalysis.getLoopsOfFunction(function).stream()
-                    .flatMap(loop -> loop.iterations().stream())
-                    .map(this::computeIterationData)
-                    .collect(Collectors.toList());
-        return dataList;
-    }
-
-    private IterationData computeIterationData(LoopAnalysis.LoopIterationInfo iteration) {
-        final Event iterStart = iteration.getIterationStart();
-        final Event iterEnd = iteration.getIterationEnd();
-
-        final IterationData data = new IterationData();
-        data.iterationInfo = iteration;
-        data.sideEffects.addAll(collectSideEffects(iterStart, iterEnd));
-        iteration.computeBody().stream()
-                .filter(CondJump.class::isInstance).map(CondJump.class::cast)
-                .filter(j -> j.isGoto() && j.getLabel().getGlobalId() > iterEnd.getGlobalId())
-                .forEach(data.guaranteedExitPoints::add);
-
-        return data;
-    }
-
-    private List<Event> collectSideEffects(Event iterStart, Event iterEnd) {
-        List<Event> sideEffects = new ArrayList<>();
-        // Unsafe means the loop read from the registers before writing to them.
-        Set<Register> unsafeRegisters = new HashSet<>();
-        // Safe means the loop wrote to these register before using them
-        Set<Register> safeRegisters = new HashSet<>();
-
-        Event cur = iterStart;
-        do {
-            if (cur.hasTag(Tag.WRITE) || (cur instanceof FunctionCall call
-                    && (!call.isDirectCall() || call.getCalledFunction().getIntrinsicInfo().writesMemory()))) {
-                // We assume side effects for all writes, writing intrinsics, or unresolved function calls.
-                sideEffects.add(cur);
-                continue;
-            }
-
-            if (cur instanceof RegReader regReader) {
-                final Set<Register> dataRegs = regReader.getRegisterReads().stream()
-                        .map(Register.Read::register).collect(Collectors.toSet());
-                unsafeRegisters.addAll(Sets.difference(dataRegs, safeRegisters));
-            }
-
-            if (cur instanceof RegWriter writer) {
-                if (unsafeRegisters.contains(writer.getResultRegister())) {
-                    // The loop writes to a register it previously read from.
-                    // This means the next loop iteration will observe the newly written value,
-                    // hence the loop is not side effect free.
-                    sideEffects.add(cur);
-                } else {
-                    safeRegisters.add(writer.getResultRegister());
-                }
-            }
-        } while ((cur = cur.getSuccessor()) != iterEnd.getSuccessor());
-        return sideEffects;
-    }
-
-    // ----------------------- Dominator-related -----------------------
-
-    private void reduceToDominatingSideEffects(IterationData data) {
-        final LoopAnalysis.LoopIterationInfo iter = data.iterationInfo;
-        final Event start = iter.getIterationStart();
-        final Event end = iter.getIterationEnd();
-
-        if (start.hasTag(Tag.SPINLOOP)) {
-            // If the iteration start is tagged as "SPINLOOP", we treat the iteration as side effect free
-            data.isAlwaysSideEffectFull = false;
-            data.sideEffects.clear();
-            return;
-        }
-
-        final List<Event> iterBody = iter.computeBody();
-        // to compute the pre-dominator tree ...
-        final Map<Event, List<Event>> immPredMap = new HashMap<>();
-        immPredMap.put(iterBody.get(0), List.of());
-        for (Event e : iterBody.subList(1, iterBody.size())) {
-            final List<Event> preds = new ArrayList<>();
-            final Event pred = e.getPredecessor();
-            if (!(pred instanceof CondJump jump && jump.isGoto())) {
-                preds.add(pred);
-            }
-            if (e instanceof Label label) {
-                preds.addAll(label.getJumpSet());
-            }
-            immPredMap.put(e, preds);
-        }
-
-        // to compute the post-dominator tree ...
-        final List<Event> reversedOrderEvents = new ArrayList<>(Lists.reverse(iterBody));
-        final Map<Event, List<Event>> immSuccMap = new HashMap<>();
-        immSuccMap.put(reversedOrderEvents.get(0), List.of());
-        for (Event e : iterBody) {
-            for (Event pred : immPredMap.get(e)) {
-                immSuccMap.computeIfAbsent(pred, key -> new ArrayList<>()).add(e);
-            }
-        }
-
-        // We delete all side effects that are guaranteed to lead to an exit point, i.e.,
-        // those that never reach a subsequent iteration.
-        reversedOrderEvents.forEach(e -> immSuccMap.putIfAbsent(e, List.of()));
-        List<Event> exitPoints = new ArrayList<>(data.guaranteedExitPoints);
-        boolean changed = true;
-        while (changed) {
-            changed = !exitPoints.isEmpty();
-            for (Event exit : exitPoints) {
-                assert immSuccMap.get(exit).isEmpty();
-                immSuccMap.remove(exit);
-                immPredMap.get(exit).forEach(pred -> immSuccMap.get(pred).remove(exit));
-            }
-            exitPoints = immSuccMap.keySet().stream().filter(e -> e != end && immSuccMap.get(e).isEmpty()).collect(Collectors.toList());
-        }
-        reversedOrderEvents.removeIf(e -> ! immSuccMap.containsKey(e));
-
-
-        final Map<Event, Event> preDominatorTree = computeDominatorTree(iterBody, immPredMap::get);
-
-        {
-            // Check if always side-effect-full
-            // This is an approximation: If the end of the iteration is predominated by some side effect
-            // then we always observe side effects.
-            Event dom = end;
-            do {
-                if (data.sideEffects.contains(dom)) {
-                    // A special case where the loop is always side-effect-full
-                    // There is no need to proceed further
-                    data.isAlwaysSideEffectFull = true;
-                    return;
-                }
-            } while ((dom = preDominatorTree.get(dom)) != start);
-        }
-
-        // Remove all side effects that are guaranteed to exit the loop.
-        data.sideEffects.removeIf(e -> !immSuccMap.containsKey(e));
-
-        // Delete all pre-dominated side effects
-        for (final Event e : List.copyOf(data.sideEffects)) {
-            Event dom = e;
-            while ((dom = preDominatorTree.get(dom)) != start) {
-                assert dom != null;
-                if (data.sideEffects.contains(dom)) {
-                    data.sideEffects.remove(e);
-                    break;
-                }
-            }
-        }
-
-        // Delete all post-dominated side effects
-        final Map<Event, Event> postDominatorTree = computeDominatorTree(reversedOrderEvents, immSuccMap::get);
-        for (final Event e : List.copyOf(data.sideEffects)) {
-            Event dom = e;
-            while ((dom = postDominatorTree.get(dom)) != end) {
-                assert dom != null;
-                if (data.sideEffects.contains(dom)) {
-                    data.sideEffects.remove(e);
-                    break;
-                }
-            }
-        }
-    }
-
-    private Map<Event, Event> computeDominatorTree(List<Event> events,
-                                                   java.util.function.Function<Event, ? extends Collection<Event>> predsFunc) {
-        Preconditions.checkNotNull(events);
-        Preconditions.checkNotNull(predsFunc);
-        if (events.isEmpty()) {
-            return Map.of();
-        }
-
-        // Compute natural ordering on <events>
-        final Map<Event, Integer> orderingMap = Maps.uniqueIndex(IntStream.range(0, events.size()).boxed()::iterator, events::get);
-        @SuppressWarnings("ConstantConditions")
-        final BiPredicate<Event, Event> leq = (x, y) -> orderingMap.get(x) <= orderingMap.get(y);
-
-        // Compute actual dominator tree
-        final Map<Event, Event> dominatorTree = new HashMap<>();
-        dominatorTree.put(events.get(0), events.get(0));
-        for (Event cur : events.subList(1, events.size())) {
-            final Collection<Event> preds = predsFunc.apply(cur);
-            Verify.verify(preds.stream().allMatch(dominatorTree::containsKey),
-                    "Error: detected predecessor outside of the provided event list.");
-            final Event immDom = preds.stream().reduce(null, (x, y) -> commonDominator(x, y, dominatorTree, leq));
-            dominatorTree.put(cur, immDom);
-        }
-
-        return dominatorTree;
-    }
-
-    private Event commonDominator(Event a, Event b, Map<Event, Event> dominatorTree, BiPredicate<Event, Event> leq) {
-        Preconditions.checkArgument(a != null || b != null);
-        if (a == null) {
-            return b;
-        } else if (b == null) {
-            return a;
-        }
-
-        while (a != b) {
-            if (leq.test(a, b)) {
-                b = dominatorTree.get(b);
-            } else {
-                a = dominatorTree.get(a);
-            }
-        }
-        return a; // a==b
-    }
-}
\ No newline at end of file
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicSpinLoopDetection.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicSpinLoopDetection.java
new file mode 100644
index 0000000000..835ba3e2ae
--- /dev/null
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/DynamicSpinLoopDetection.java
@@ -0,0 +1,246 @@
+package com.dat3m.dartagnan.program.processing;
+
+import com.dat3m.dartagnan.expression.Expression;
+import com.dat3m.dartagnan.expression.ExpressionFactory;
+import com.dat3m.dartagnan.expression.type.TypeFactory;
+import com.dat3m.dartagnan.program.Function;
+import com.dat3m.dartagnan.program.Program;
+import com.dat3m.dartagnan.program.Register;
+import com.dat3m.dartagnan.program.Thread;
+import com.dat3m.dartagnan.program.analysis.DominatorAnalysis;
+import com.dat3m.dartagnan.program.analysis.LoopAnalysis;
+import com.dat3m.dartagnan.program.event.*;
+import com.dat3m.dartagnan.program.event.core.Label;
+import com.dat3m.dartagnan.program.event.functions.FunctionCall;
+import com.dat3m.dartagnan.program.event.lang.svcomp.SpinStart;
+import com.dat3m.dartagnan.utils.DominatorTree;
+import com.google.common.base.Preconditions;
+import com.google.common.collect.Iterables;
+import com.google.common.collect.Sets;
+import com.google.common.collect.Streams;
+import org.apache.logging.log4j.LogManager;
+import org.apache.logging.log4j.Logger;
+import org.sosy_lab.common.configuration.Configuration;
+
+import java.util.ArrayList;
+import java.util.HashSet;
+import java.util.List;
+import java.util.Set;
+import java.util.function.Predicate;
+import java.util.stream.Collectors;
+
+/*
+    This pass instruments loops that do not cause a side effect in an iteration to terminate, i.e., to avoid spinning.
+    In other words, only the last loop iteration is allowed to be side-effect free.
+
+    NOTE: This pass is required to detect liveness violations.
+ */
+public class DynamicSpinLoopDetection implements ProgramProcessor {
+
+    private static final Logger logger = LogManager.getLogger(DynamicSpinLoopDetection.class);
+
+    public static DynamicSpinLoopDetection fromConfig(Configuration config) {
+        return new DynamicSpinLoopDetection();
+    }
+
+    @Override
+    public void run(Program program) {
+        Preconditions.checkArgument(!program.isUnrolled(),
+                "DynamicSpinLoopDetection cannot be run on already unrolled programs.");
+
+        final LoopAnalysis loopAnalysis = LoopAnalysis.newInstance(program);
+        AnalysisStats stats = new AnalysisStats(0, 0);
+        for (Function func : Iterables.concat(program.getFunctions(), program.getThreads())) {
+            final List<LoopData> loops = computeLoopData(func, loopAnalysis);
+            loops.forEach(this::collectSideEffects);
+            loops.forEach(this::reduceToDominatingSideEffects);
+            loops.forEach(this::instrumentLoop);
+            stats = stats.add(collectStats(loops));
+        }
+        IdReassignment.newInstance().run(program); // Reassign ids for the instrumented code.
+
+        // NOTE: We log "potential spin loops" as only those that are not also "static".
+        logger.info("Found {} static spin loops and {} potential spin loops.",
+                stats.numStaticSpinLoops, (stats.numPotentialSpinLoops - stats.numStaticSpinLoops));
+    }
+
+    // ==================================================================================================
+    // Internals
+
+    private List<LoopData> computeLoopData(Function func, LoopAnalysis loopAnalysis) {
+        final List<LoopAnalysis.LoopInfo> loops = loopAnalysis.getLoopsOfFunction(func);
+        return loops.stream().map(LoopData::new).toList();
+    }
+
+    private void collectSideEffects(LoopData loop) {
+        if (loop.getStart().getSuccessor() instanceof SpinStart) {
+            // A user-placed annotation guarantees absence of side effects.
+
+            // This checks assumes the following implementation of await_while
+            // #define await_while(cond)                                                  \
+            // for (int tmp = (__VERIFIER_loop_begin(), 0); __VERIFIER_spin_start(),  \
+            //     tmp = cond, __VERIFIER_spin_end(!tmp), tmp;)
+            return;
+        }
+
+        // FIXME: The reasoning about safe/unsafe registers is not correct because
+        //  we do not traverse the control-flow but naively go top-down through the loop.
+        //  We need to use proper dominator reasoning!
+
+        // Unsafe means the loop reads from the registers before writing to them.
+        Set<Register> unsafeRegisters = new HashSet<>();
+        // Safe means the loop wrote to these register before using them
+        Set<Register> safeRegisters = new HashSet<>();
+
+        Event cur = loop.getStart();
+        do {
+            if (cur.hasTag(Tag.WRITE) || (cur instanceof FunctionCall call &&
+                    (!call.isDirectCall()
+                            || !call.getCalledFunction().isIntrinsic()
+                            || call.getCalledFunction().getIntrinsicInfo().writesMemory()))) {
+                // We assume side effects for all writes, writing intrinsics, and non-intrinsic function calls.
+                loop.sideEffects.add(cur);
+                continue;
+            }
+
+            if (cur instanceof RegReader regReader) {
+                final Set<Register> dataRegs = regReader.getRegisterReads().stream()
+                        .map(Register.Read::register).collect(Collectors.toSet());
+                unsafeRegisters.addAll(Sets.difference(dataRegs, safeRegisters));
+            }
+
+            if (cur instanceof RegWriter writer) {
+                if (unsafeRegisters.contains(writer.getResultRegister())) {
+                    // The loop writes to a register it previously read from.
+                    // This means the next loop iteration will observe the newly written value,
+                    // hence the loop is not side effect free.
+                    loop.sideEffects.add(cur);
+                } else {
+                    safeRegisters.add(writer.getResultRegister());
+                }
+            }
+        } while ((cur = cur.getSuccessor()) != loop.getEnd().getSuccessor());
+
+    }
+
+    private void reduceToDominatingSideEffects(LoopData loop) {
+        if (loop.sideEffects.isEmpty()) {
+            return;
+        }
+
+        final List<Event> sideEffects = loop.sideEffects;
+        final Event start = loop.getStart();
+        final Event end = loop.getEnd();
+
+        final DominatorTree<Event> preDominatorTree = DominatorAnalysis.computePreDominatorTree(start, end);
+        final DominatorTree<Event> postDominatorTree = DominatorAnalysis.computePostDominatorTree(start, end);
+
+        // (1) Delete all side effects that are on exit paths (those have no dominator in the post-dominator tree
+        // because they are no predecessor of the end of the loop body).
+        final Predicate<Event> isOnExitPath = (e -> postDominatorTree.getImmediateDominator(e) == null);
+        sideEffects.removeIf(isOnExitPath);
+
+        // (2) Check if always side-effect-full at the end of an iteration directly before entering the next one.
+        // This is an approximation: If the end of the iteration is predominated by some side effect
+        // then we always observe side effects.
+        loop.isAlwaysSideEffectful = Streams.stream(preDominatorTree.getDominators(end)).anyMatch(sideEffects::contains);
+        if (loop.isAlwaysSideEffectful) {
+            return;
+        }
+
+        // (3) Delete all side effects that are dominated by another one
+        // NOTE: This can be implemented more efficiently, but maybe we don't need to.
+        for (int i = sideEffects.size() - 1; i >= 0; i--) {
+            final Event sideEffect = sideEffects.get(i);
+            final Iterable<Event> dominators = Iterables.concat(
+                    preDominatorTree.getStrictDominators(sideEffect),
+                    postDominatorTree.getStrictDominators(sideEffect)
+            );
+            final boolean isDominated = Iterables.tryFind(dominators, sideEffects::contains).isPresent();
+            if (isDominated) {
+                sideEffects.remove(i);
+            }
+        }
+    }
+
+    private void instrumentLoop(LoopData loop) {
+        if (loop.isAlwaysSideEffectful) {
+            return;
+        }
+
+        final TypeFactory types = TypeFactory.getInstance();
+        final ExpressionFactory expressions = ExpressionFactory.getInstance();
+        final Function func = loop.loopInfo.function();
+        final int loopNum = loop.loopInfo.loopNumber();
+        final Register trackingReg = func.newRegister("__sideEffect#" + loopNum, types.getBooleanType());
+
+        final Event init = EventFactory.newLocal(trackingReg, expressions.makeFalse());
+        loop.getStart().insertAfter(init);
+        for (Event sideEffect : loop.sideEffects) {
+            final Event updateSideEffect = EventFactory.newLocal(trackingReg, expressions.makeTrue());
+            sideEffect.getPredecessor().insertAfter(updateSideEffect);
+        }
+
+        final Event assumeSideEffect = newSpinTerminator(expressions.makeNot(trackingReg), func);
+        assumeSideEffect.copyAllMetadataFrom(loop.getStart());
+        loop.getEnd().getPredecessor().insertAfter(assumeSideEffect);
+
+        // Special case: If the loop is fully side-effect-free, we can set its unrolling bound to 1.
+        if (loop.sideEffects.isEmpty()) {
+            final Event loopBound = EventFactory.Svcomp.newLoopBound(expressions.makeValue(1, types.getArchType()));
+            loop.getStart().getPredecessor().insertAfter(loopBound);
+        }
+    }
+
+    private Event newSpinTerminator(Expression guard, Function func) {
+        final Event terminator = func instanceof Thread thread ?
+                EventFactory.newJump(guard, (Label) thread.getExit())
+                : EventFactory.newAbortIf(guard);
+        terminator.addTags(Tag.SPINLOOP, Tag.EARLYTERMINATION, Tag.NOOPT);
+        return terminator;
+    }
+
+    private AnalysisStats collectStats(List<LoopData> loops) {
+        int numPotentialSpinLoops = 0;
+        int numStaticSpinLoops = 0;
+        for (LoopData loop : loops) {
+            if (!loop.isAlwaysSideEffectful) {
+                numPotentialSpinLoops++;
+                if (loop.sideEffects.isEmpty()) {
+                    numStaticSpinLoops++;
+                }
+            }
+        }
+        return new AnalysisStats(numPotentialSpinLoops, numStaticSpinLoops);
+    }
+
+    // ==================================================================================================
+    // Inner data structures
+
+    private static class LoopData {
+        private final LoopAnalysis.LoopInfo loopInfo;
+        private final List<Event> sideEffects = new ArrayList<>();
+        private boolean isAlwaysSideEffectful = false;
+
+        private LoopData(LoopAnalysis.LoopInfo loopInfo) {
+            this.loopInfo = loopInfo;
+        }
+
+        private Event getStart() { return loopInfo.iterations().get(0).getIterationStart(); }
+        private Event getEnd() { return loopInfo.iterations().get(0).getIterationEnd(); }
+
+        @Override
+        public String toString() {
+            return String.format("(%d: %s) --to--> (%d: %s)",
+                    getStart().getGlobalId(), getStart(), getEnd().getGlobalId(), getEnd());
+        }
+    }
+
+    private record AnalysisStats(int numPotentialSpinLoops, int numStaticSpinLoops) {
+
+        private AnalysisStats add(AnalysisStats stats) {
+            return new AnalysisStats(this.numPotentialSpinLoops + stats.numPotentialSpinLoops,
+                    this.numStaticSpinLoops + stats.numStaticSpinLoops);
+        }
+    }
+}
\ No newline at end of file
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java
index aec3c20e41..159c072757 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/ProcessingManager.java
@@ -37,10 +37,10 @@ public class ProcessingManager implements ProgramProcessor {
             secure = true)
     private boolean dce = true;
 
-    @Option(name = DYNAMIC_PURE_LOOP_CUTTING,
+    @Option(name = DYNAMIC_SPINLOOP_DETECTION,
             description = "Instruments loops to terminate early when spinning.",
             secure = true)
-    private boolean dynamicPureLoopCutting = true;
+    private boolean dynamicSpinLoopDetection = true;
 
     // =================== Debugging options ===================
 
@@ -98,14 +98,10 @@ private ProcessingManager(Configuration config) throws InvalidConfigurationExcep
                 Compilation.fromConfig(config), // We keep compilation global for now
                 printAfterCompilation ? DebugPrint.withHeader("After compilation", Printer.Mode.ALL) : null,
                 ProgramProcessor.fromFunctionProcessor(MemToReg.fromConfig(config), Target.FUNCTIONS, true),
-                ProgramProcessor.fromFunctionProcessor(
-                        SimpleSpinLoopDetection.fromConfig(config),
-                        Target.FUNCTIONS, false
-                ),
                 ProgramProcessor.fromFunctionProcessor(sccp, Target.FUNCTIONS, false),
+                dynamicSpinLoopDetection ? DynamicSpinLoopDetection.fromConfig(config) : null,
                 LoopUnrolling.fromConfig(config), // We keep unrolling global for now
                 printAfterUnrolling ? DebugPrint.withHeader("After loop unrolling", Printer.Mode.ALL) : null,
-                dynamicPureLoopCutting ? DynamicPureLoopCutting.fromConfig(config) : null,
                 ProgramProcessor.fromFunctionProcessor(
                         FunctionProcessor.chain(
                                 ResolveLLVMObjectSizeCalls.fromConfig(config),
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/SimpleSpinLoopDetection.java b/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/SimpleSpinLoopDetection.java
deleted file mode 100644
index c0ed74d766..0000000000
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/program/processing/SimpleSpinLoopDetection.java
+++ /dev/null
@@ -1,125 +0,0 @@
-package com.dat3m.dartagnan.program.processing;
-
-import com.dat3m.dartagnan.program.Function;
-import com.dat3m.dartagnan.program.Register;
-import com.dat3m.dartagnan.program.event.Event;
-import com.dat3m.dartagnan.program.event.RegReader;
-import com.dat3m.dartagnan.program.event.RegWriter;
-import com.dat3m.dartagnan.program.event.Tag;
-import com.dat3m.dartagnan.program.event.core.CondJump;
-import com.dat3m.dartagnan.program.event.core.Label;
-import com.dat3m.dartagnan.program.event.functions.FunctionCall;
-import com.dat3m.dartagnan.program.event.lang.svcomp.SpinStart;
-import com.google.common.collect.Sets;
-import org.sosy_lab.common.configuration.Configuration;
-import org.sosy_lab.common.configuration.InvalidConfigurationException;
-
-import java.util.HashSet;
-import java.util.List;
-import java.util.Set;
-import java.util.stream.Collectors;
-
-/*
-    This pass finds and marks simple loops that are totally side-effect-free (simple spin loops).
-    It will also mark side-effect-full loops if they are annotated by a SpinStart event
-    (we assume the user guarantees the correctness of the annotation)
-
-    The pass is unable to detect complex types of loops that may spin endlessly (i.e. run into a deadlock)
-    while producing side effects. It will also fail to mark loops with conditional side effects.
-
-    TODO: Instead of tagging labels as spinning and checking for that tag during loop unrolling
-          we could let this pass produce LoopBound-Annotations to guide the unrolling implicitly.
-
-    TODO 2: Intrinsic calls need to get special treatment as they might be side-effect-full
-     (for now, all our intrinsics are side-effect-free, so it works fine).
- */
-public class SimpleSpinLoopDetection implements FunctionProcessor {
-
-    private SimpleSpinLoopDetection() { }
-
-    public static SimpleSpinLoopDetection newInstance() {
-        return new SimpleSpinLoopDetection();
-    }
-
-    public static SimpleSpinLoopDetection fromConfig(Configuration config) throws InvalidConfigurationException {
-        return newInstance();
-    }
-
-    // --------------------------------------------------------------
-
-    @Override
-    public void run(Function function) {
-        if (function.hasBody()) {
-            detectAndMarkSpinLoops(function);
-        }
-    }
-
-    private int detectAndMarkSpinLoops(Function function) {
-        final List<Label> unmarkedLabels = function.getEvents(Label.class).stream()
-                .filter(e -> !e.hasTag(Tag.SPINLOOP)).toList();
-
-        int spinloopCounter = 0;
-        for (final Label label : unmarkedLabels) {
-            final List<CondJump> backjumps = label.getJumpSet()
-                    .stream().filter(x -> x.getGlobalId() > label.getGlobalId())
-                    .toList();
-            final boolean isLoop = !backjumps.isEmpty();
-
-            if (isLoop) {
-                assert backjumps.size() == 1; // Invariant holds for all normalized loops
-                final CondJump backjump = backjumps.get(0);
-                if (isSideEffectFree(label, backjump)) {
-                    label.addTags(Tag.SPINLOOP, Tag.NOOPT);
-                    backjump.addTags(Tag.SPINLOOP, Tag.NOOPT);
-                    spinloopCounter++;
-                }
-            }
-        }
-        return spinloopCounter;
-    }
-
-    private boolean isSideEffectFree(Label loopBegin, CondJump loopEnd) {
-        if (loopBegin.getSuccessor() instanceof SpinStart) {
-            // No need to check if the loop is side effect free,
-            // the user guarantees this by using the annotation.
-
-            // This checks assumes the following implementation of await_while
-            // #define await_while(cond)                                                  \
-            // for (int tmp = (__VERIFIER_loop_begin(), 0); __VERIFIER_spin_start(),  \
-            //     tmp = cond, __VERIFIER_spin_end(!tmp), tmp;)
-            return true;
-        }
-
-        // Unsafe means the loop read from the registers before writing to them.
-        Set<Register> unsafeRegisters = new HashSet<>();
-        // Safe means the loop wrote to these register before using them
-        Set<Register> safeRegisters = new HashSet<>();
-
-        Event cur = loopBegin;
-        while ((cur = cur.getSuccessor()) != loopEnd) {
-            if (cur.hasTag(Tag.WRITE) || (cur instanceof FunctionCall call
-                    && (!call.isDirectCall() || call.getCalledFunction().getIntrinsicInfo().writesMemory()))) {
-                // We assume side effects for all writes, writing intrinsics, or unresolved function calls.
-                return false;
-            }
-
-            if (cur instanceof RegReader regReader) {
-                final Set<Register> readRegs = regReader.getRegisterReads().stream()
-                        .map(Register.Read::register).collect(Collectors.toSet());
-                unsafeRegisters.addAll(Sets.difference(readRegs, safeRegisters));
-            }
-
-            if (cur instanceof RegWriter writer) {
-                if (unsafeRegisters.contains(writer.getResultRegister())) {
-                    // The loop writes to a register it previously read from.
-                    // This means the next loop iteration will observe the newly written value,
-                    // hence the loop is not side effect free.
-                    return false;
-                } else {
-                    safeRegisters.add(writer.getResultRegister());
-                }
-            }
-        }
-        return true;
-    }
-}
\ No newline at end of file
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/utils/DominatorTree.java b/dartagnan/src/main/java/com/dat3m/dartagnan/utils/DominatorTree.java
new file mode 100644
index 0000000000..0a7be37e86
--- /dev/null
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/utils/DominatorTree.java
@@ -0,0 +1,178 @@
+package com.dat3m.dartagnan.utils;
+
+import com.google.common.collect.Iterables;
+import com.google.common.collect.Lists;
+
+import java.util.*;
+import java.util.function.Function;
+
+/*
+    Description of dominator trees.
+
+    Let G = (V, A, r) be a directed graph rooted in r.
+    NOTE: In the following description we assume that all nodes in V are reachable from r.
+
+    DEFINITION (Domination): A node w is dominated by v if all paths from r to w pass through v, i.e.,
+    all those paths have the shape r ->* v ->* w.
+    Note that every node v has dominators Dom(v), containing at least itself and the root.
+
+    PROPOSITION: For every node that is not the root, there is a unique "closest/nearest" dominator,
+                 the immediate dominator.
+
+    DEFINITION (Dominator tree): The "immediate-dominator-relation" induces the dominator tree (rooted at r).
+    A node w is strictly dominated by v if v is an ancestor in this tree (Dom(w) = {w} + all its ancestors).
+
+
+   IMPLEMENTATION NOTES:
+        - Based on Cooper's iterative algorithm.
+        - There are more efficient implementations like SLT (Simple Lengauer-Tarjan)
+          and Semi-NCA, but those are harder to implement.
+
+ */
+public final class DominatorTree<TNode> {
+
+    private final TNode root;
+    private final Comparator<TNode> reversePostOrder;
+    private final Map<TNode, TNode> immDominator;
+
+    public DominatorTree(TNode root, Function<TNode, ? extends Iterable<? extends TNode>> successors) {
+        final List<TNode> reversePostOrderNodes = Lists.reverse(computePostOrder(root, successors));
+        final Map<TNode, List<TNode>> predecessorMap = computePredecessorMap(root, successors);
+
+        this.root = root;
+        this.reversePostOrder = computeOrderFromSequence(reversePostOrderNodes);
+        this.immDominator = computeDominatorTree(root, reversePostOrderNodes, predecessorMap, reversePostOrder);
+    }
+
+    public TNode getRoot() {
+        return root;
+    }
+
+    public boolean isDominatedBy(TNode node, TNode dominator) {
+        return getNearestCommonDominator(node, dominator) == dominator;
+    }
+
+    public TNode getImmediateDominator(TNode node) {
+        return immDominator.get(node);
+    }
+
+    public TNode getNearestCommonDominator(TNode a, TNode b) {
+        return intersect(a, b, immDominator, reversePostOrder);
+    }
+
+    public Iterable<TNode> getDominators(TNode node) {
+        return () -> new Iterator<>() {
+            TNode cur = node;
+            @Override
+            public boolean hasNext() { return cur != null; }
+            @Override
+            public TNode next() {
+                final TNode ret = cur;
+                cur = (cur == root) ? null : getImmediateDominator(cur);
+                return ret;
+            }
+        };
+    }
+
+    public Iterable<TNode> getStrictDominators(TNode node) {
+        return Iterables.skip(getDominators(node), 1);
+    }
+
+    // ===============================================================================================================
+    // Internals
+
+    private List<TNode> computePostOrder(TNode root, Function<TNode, ? extends Iterable<? extends TNode>> successors) {
+        List<TNode> order = new ArrayList<>();
+        Map<TNode, TNode> parentMap = new HashMap<>();
+
+        parentMap.put(root, null);
+        TNode cur = root;
+        while (cur != null) {
+            boolean childrenTraversed = true;
+            for (TNode succ : successors.apply(cur)) {
+                if (!parentMap.containsKey(succ)) {
+                    parentMap.put(succ, cur);
+                    cur = succ;
+                    childrenTraversed = false;
+                }
+            }
+            if (childrenTraversed) {
+                order.add(cur);
+                cur = parentMap.get(cur);
+            }
+        }
+
+        assert order.get(order.size() - 1) == root;
+        return order;
+    }
+
+    private Map<TNode, TNode> computeDominatorTree(
+            TNode root,
+            List<TNode> nodes,
+            Map<TNode, List<TNode>> predecessorMap,
+            Comparator<TNode> reversePostOrder
+    ) {
+
+        final Map<TNode, TNode> immDom = new HashMap<>();
+        immDom.put(root, root);
+
+        boolean changed = true;
+        while (changed) {
+            changed = false;
+            for (TNode node : nodes) {
+                if (node == root) {
+                    continue;
+                }
+                TNode newDom = null;
+                for (TNode pred : predecessorMap.get(node)) {
+                    if (immDom.containsKey(pred)) {
+                        newDom = (newDom == null) ? pred : intersect(newDom, pred, immDom, reversePostOrder);
+                    }
+                }
+                if (immDom.get(node) != newDom) {
+                    immDom.put(node, newDom);
+                    changed = true;
+                }
+            }
+        }
+
+        return immDom;
+    }
+
+    private TNode intersect(TNode a, TNode b, Map<TNode, TNode> immDom, Comparator<? super TNode> reversePostOrder) {
+        while (a != b) {
+            if (reversePostOrder.compare(a, b) < 0) {
+                b = immDom.get(b);
+            } else {
+                a = immDom.get(a);
+            }
+        }
+        return a;
+    }
+
+    private Map<TNode, List<TNode>> computePredecessorMap(TNode root, Function<TNode, ? extends Iterable<? extends TNode>> successors) {
+        Set<TNode> processed = new HashSet<>();
+        Map<TNode, List<TNode>> predecessorMap = new HashMap<>();
+        Deque<TNode> workqueue = new ArrayDeque<>();
+
+        workqueue.add(root);
+        while (!workqueue.isEmpty()) {
+            final TNode cur = workqueue.remove();
+            processed.add(cur);
+            for (TNode succ : successors.apply(cur)) {
+                predecessorMap.computeIfAbsent(succ, key -> new ArrayList<>()).add(cur);
+                if (!processed.contains(succ)) {
+                    workqueue.add(succ);
+                }
+            }
+        }
+
+        return predecessorMap;
+    }
+
+    private Comparator<TNode> computeOrderFromSequence(Iterable<TNode> seq) {
+        final Map<TNode, Integer> orderNumbers = new HashMap<>();
+        seq.forEach(n -> orderNumbers.put(n, orderNumbers.size()));
+        return Comparator.comparingInt(orderNumbers::get);
+    }
+}