diff --git a/benchmarks/progress/progressHSA2.c b/benchmarks/progress/progressFair.c
similarity index 74%
rename from benchmarks/progress/progressHSA2.c
rename to benchmarks/progress/progressFair.c
index 972a7ad841..b747c239f0 100644
--- a/benchmarks/progress/progressHSA2.c
+++ b/benchmarks/progress/progressFair.c
@@ -3,19 +3,19 @@
 #include <assert.h>
 #include <stdatomic.h>
 
+// Required progress: fair
+
 atomic_int x = 0;
 
 void *thread_1(void *unused)
 {
-    while (x != 0);
+    while (x != 1);
     return 0;
 }
 
 void *thread_2(void *unused)
 {
-    x = 1;
-    // HSA may stop here causing a liveness issue (OBE cannot do this)
-    x = 0;
+    x = 1; // May not get scheduled under any weak progress model
 }
 
 int main()
diff --git a/benchmarks/progress/progressHSA.c b/benchmarks/progress/progressHSA.c
index 28cc7e7696..533cea6c68 100644
--- a/benchmarks/progress/progressHSA.c
+++ b/benchmarks/progress/progressHSA.c
@@ -3,28 +3,25 @@
 #include <assert.h>
 #include <stdatomic.h>
 
+// Required progress: HSA
+
 atomic_int x = 0;
 
 void *thread_1(void *unused)
 {
-    while (x != 1);
-    return 0;
+    x = 1; // OBE might not schedule this thread
 }
 
 void *thread_2(void *unused)
 {
-    x = 1; // May not get scheduled under HSA
+    while (x != 1);
+    return 0;
 }
 
 int main()
 {
     pthread_t t1, t2;
-#ifndef FAIL
-    pthread_create(&t2, NULL, thread_2, NULL);
-    pthread_create(&t1, NULL, thread_1, NULL);
-#else
     pthread_create(&t1, NULL, thread_1, NULL);
     pthread_create(&t2, NULL, thread_2, NULL);
-#endif
     return 0;
 }
diff --git a/benchmarks/progress/progressUnfair2.c b/benchmarks/progress/progressOBE-HSA.c
similarity index 86%
rename from benchmarks/progress/progressUnfair2.c
rename to benchmarks/progress/progressOBE-HSA.c
index 9196bcb955..3e37c2c673 100644
--- a/benchmarks/progress/progressUnfair2.c
+++ b/benchmarks/progress/progressOBE-HSA.c
@@ -3,6 +3,8 @@
 #include <assert.h>
 #include <stdatomic.h>
 
+// Required progress: HSA or OBE (stronger than unfair)
+
 atomic_int x = 0;
 
 void *thread_1(void *unused)
diff --git a/benchmarks/progress/progressOBE.c b/benchmarks/progress/progressOBE.c
index 03a72de133..a3bb6d058f 100644
--- a/benchmarks/progress/progressOBE.c
+++ b/benchmarks/progress/progressOBE.c
@@ -3,23 +3,27 @@
 #include <assert.h>
 #include <stdatomic.h>
 
+// Required progress: OBE
+
 atomic_int x = 0;
 
 void *thread_1(void *unused)
 {
-    while (x != 1);
+    while (x != 0);
     return 0;
 }
 
 void *thread_2(void *unused)
 {
     x = 1;
+    // HSA may stop here causing a liveness issue (OBE cannot do this)
+    x = 0;
 }
 
 int main()
 {
     pthread_t t1, t2;
-    pthread_create(&t2, NULL, thread_2, NULL); // May not get scheduled under OBE, but would under HSA
     pthread_create(&t1, NULL, thread_1, NULL);
+    pthread_create(&t2, NULL, thread_2, NULL);
     return 0;
 }
diff --git a/benchmarks/progress/progressUnfair.c b/benchmarks/progress/progressUnfair.c
index e61e0d03bd..d68058e029 100644
--- a/benchmarks/progress/progressUnfair.c
+++ b/benchmarks/progress/progressUnfair.c
@@ -5,6 +5,8 @@
 
 atomic_int x = 0;
 
+// Required progress: Unfair (terminates under all progress models)
+
 void *thread_1(void *unused)
 {
     while (x != 1);
@@ -14,13 +16,7 @@ void *thread_1(void *unused)
 int main()
 {
     pthread_t t1, t2;
-#ifndef FAIL
     x = 1;
     pthread_create(&t1, NULL, thread_1, NULL);
-#else
-    pthread_create(&t1, NULL, thread_1, NULL);
-    // Under totally unfair scheduling, we can stop here, never signaling T1
-    x = 1;
-#endif
     return 0;
 }
diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/c/AbstractCTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/c/AbstractCTest.java
index 986af60fb3..6279a4c64a 100644
--- a/dartagnan/src/test/java/com/dat3m/dartagnan/c/AbstractCTest.java
+++ b/dartagnan/src/test/java/com/dat3m/dartagnan/c/AbstractCTest.java
@@ -71,6 +71,10 @@ protected Provider<Configuration> getConfigurationProvider() {
         return Provider.fromSupplier(this::getConfiguration);
     }
 
+    protected Provider<ProgressModel> getProgressModelProvider() {
+        return () -> ProgressModel.FAIR;
+    }
+
     // =============================================================
 
     // Provider rules
@@ -80,7 +84,7 @@ protected Provider<Configuration> getConfigurationProvider() {
     protected final Provider<Integer> boundProvider = getBoundProvider();
     protected final Provider<Program> programProvider = Providers.createProgramFromPath(filePathProvider);
     protected final Provider<Wmm> wmmProvider = getWmmProvider();
-    protected final Provider<ProgressModel> progressModelProvider = () -> ProgressModel.FAIR;
+    protected final Provider<ProgressModel> progressModelProvider = getProgressModelProvider();
     protected final Provider<Solvers> solverProvider = getSolverProvider();
     protected final Provider<EnumSet<Property>> propertyProvider = getPropertyProvider();
     protected final Provider<Configuration> configurationProvider = getConfigurationProvider();
diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/c/CProgressTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/c/CProgressTest.java
new file mode 100644
index 0000000000..4744418956
--- /dev/null
+++ b/dartagnan/src/test/java/com/dat3m/dartagnan/c/CProgressTest.java
@@ -0,0 +1,102 @@
+package com.dat3m.dartagnan.c;
+
+import com.dat3m.dartagnan.configuration.ProgressModel;
+import com.dat3m.dartagnan.configuration.Property;
+import com.dat3m.dartagnan.utils.Result;
+import com.dat3m.dartagnan.utils.rules.Provider;
+import com.dat3m.dartagnan.utils.rules.Providers;
+import com.dat3m.dartagnan.verification.solving.AssumeSolver;
+import com.dat3m.dartagnan.verification.solving.RefinementSolver;
+import com.dat3m.dartagnan.wmm.Wmm;
+import org.junit.Test;
+import org.junit.runner.RunWith;
+import org.junit.runners.Parameterized;
+
+import java.io.IOException;
+import java.util.Arrays;
+import java.util.EnumSet;
+
+import static com.dat3m.dartagnan.configuration.Arch.C11;
+import static com.dat3m.dartagnan.configuration.ProgressModel.*;
+import static com.dat3m.dartagnan.utils.ResourceHelper.getTestResourcePath;
+import static com.dat3m.dartagnan.utils.Result.FAIL;
+import static com.dat3m.dartagnan.utils.Result.PASS;
+import static org.junit.Assert.assertEquals;
+
+@RunWith(Parameterized.class)
+public class CProgressTest extends AbstractCTest {
+
+    protected ProgressModel progressModel;
+
+    public CProgressTest(String name, ProgressModel progressModel, Result expected) {
+        super(name, C11, expected);
+        this.progressModel = progressModel;
+    }
+
+    @Override
+    protected Provider<String> getProgramPathProvider() {
+        return () -> getTestResourcePath("progress/" + name + ".ll");
+    }
+
+    @Override
+    protected Provider<ProgressModel> getProgressModelProvider() {
+        return () -> progressModel;
+    }
+
+    @Override
+    protected Provider<Wmm> getWmmProvider() {
+        return Providers.createWmmFromName(() -> "imm");
+    }
+
+    @Override
+    protected Provider<EnumSet<Property>> getPropertyProvider() {
+        return () -> EnumSet.of(Property.LIVENESS);
+    }
+
+    @Override
+    protected long getTimeout() {
+        return 10000;
+    }
+
+    @Parameterized.Parameters(name = "{index}: {0}, progress={1}")
+    public static Iterable<Object[]> data() throws IOException {
+        return Arrays.asList(new Object[][]{
+                {"progressFair", FAIR, PASS},
+                {"progressFair", HSA, FAIL},
+                {"progressFair", OBE, FAIL},
+                {"progressFair", UNFAIR, FAIL},
+                // ---------------------------
+                {"progressHSA", FAIR, PASS},
+                {"progressHSA", HSA, PASS},
+                {"progressHSA", OBE, FAIL},
+                {"progressHSA", UNFAIR, FAIL},
+                // ---------------------------
+                {"progressOBE", FAIR, PASS},
+                {"progressOBE", HSA, FAIL},
+                {"progressOBE", OBE, PASS},
+                {"progressOBE", UNFAIR, FAIL},
+                // ---------------------------
+                {"progressOBE-HSA", FAIR, PASS},
+                {"progressOBE-HSA", HSA, PASS},
+                {"progressOBE-HSA", OBE, PASS},
+                {"progressOBE-HSA", UNFAIR, FAIL},
+                // ---------------------------
+                {"progressUnfair", FAIR, PASS},
+                {"progressUnfair", HSA, PASS},
+                {"progressUnfair", OBE, PASS},
+                {"progressUnfair", UNFAIR, PASS},
+        });
+    }
+
+    @Test
+    public void testAssume() throws Exception {
+        AssumeSolver s = AssumeSolver.run(contextProvider.get(), proverProvider.get(), taskProvider.get());
+        assertEquals(expected, s.getResult());
+    }
+
+    @Test
+    public void testRefinement() throws Exception {
+        RefinementSolver s = RefinementSolver.run(contextProvider.get(), proverProvider.get(), taskProvider.get());
+        assertEquals(expected, s.getResult());
+    }
+}
\ No newline at end of file
diff --git a/dartagnan/src/test/resources/progress/progressFair.ll b/dartagnan/src/test/resources/progress/progressFair.ll
new file mode 100644
index 0000000000..5e7bdfe0fc
--- /dev/null
+++ b/dartagnan/src/test/resources/progress/progressFair.ll
@@ -0,0 +1,134 @@
+; ModuleID = '/Users/thomashaas/IdeaProjects/Dat3M/output/progressFair.ll'
+source_filename = "/Users/thomashaas/IdeaProjects/Dat3M/benchmarks/progress/progressFair.c"
+target datalayout = "e-m:o-i64:64-i128:128-n32:64-S128"
+target triple = "arm64-apple-macosx14.0.0"
+
+%struct._opaque_pthread_t = type { i64, %struct.__darwin_pthread_handler_rec*, [8176 x i8] }
+%struct.__darwin_pthread_handler_rec = type { void (i8*)*, i8*, %struct.__darwin_pthread_handler_rec* }
+%struct._opaque_pthread_attr_t = type { i64, [56 x i8] }
+
+@x = global i32 0, align 4, !dbg !0
+
+; Function Attrs: noinline nounwind ssp uwtable
+define i8* @thread_1(i8* noundef %0) #0 !dbg !23 {
+  call void @llvm.dbg.value(metadata i8* %0, metadata !27, metadata !DIExpression()), !dbg !28
+  br label %2, !dbg !29
+
+2:                                                ; preds = %2, %1
+  %3 = load atomic i32, i32* @x seq_cst, align 4, !dbg !30
+  %4 = icmp ne i32 %3, 1, !dbg !31
+  br i1 %4, label %2, label %5, !dbg !29, !llvm.loop !32
+
+5:                                                ; preds = %2
+  ret i8* null, !dbg !35
+}
+
+; Function Attrs: nofree nosync nounwind readnone speculatable willreturn
+declare void @llvm.dbg.declare(metadata, metadata, metadata) #1
+
+; Function Attrs: noinline nounwind ssp uwtable
+define i8* @thread_2(i8* noundef %0) #0 !dbg !36 {
+  call void @llvm.dbg.value(metadata i8* %0, metadata !37, metadata !DIExpression()), !dbg !38
+  store atomic i32 1, i32* @x seq_cst, align 4, !dbg !39
+  ret i8* undef, !dbg !40
+}
+
+; Function Attrs: noinline nounwind ssp uwtable
+define i32 @main() #0 !dbg !41 {
+  %1 = alloca %struct._opaque_pthread_t*, align 8
+  %2 = alloca %struct._opaque_pthread_t*, align 8
+  call void @llvm.dbg.declare(metadata %struct._opaque_pthread_t** %1, metadata !44, metadata !DIExpression()), !dbg !69
+  call void @llvm.dbg.declare(metadata %struct._opaque_pthread_t** %2, metadata !70, metadata !DIExpression()), !dbg !71
+  %3 = call i32 @pthread_create(%struct._opaque_pthread_t** noundef %1, %struct._opaque_pthread_attr_t* noundef null, i8* (i8*)* noundef @thread_1, i8* noundef null), !dbg !72
+  %4 = call i32 @pthread_create(%struct._opaque_pthread_t** noundef %2, %struct._opaque_pthread_attr_t* noundef null, i8* (i8*)* noundef @thread_2, i8* noundef null), !dbg !73
+  ret i32 0, !dbg !74
+}
+
+declare i32 @pthread_create(%struct._opaque_pthread_t** noundef, %struct._opaque_pthread_attr_t* noundef, i8* (i8*)* noundef, i8* noundef) #2
+
+; Function Attrs: nofree nosync nounwind readnone speculatable willreturn
+declare void @llvm.dbg.value(metadata, metadata, metadata) #1
+
+attributes #0 = { noinline nounwind ssp uwtable "frame-pointer"="non-leaf" "min-legal-vector-width"="0" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="apple-m1" "target-features"="+aes,+crc,+crypto,+dotprod,+fp-armv8,+fp16fml,+fullfp16,+lse,+neon,+ras,+rcpc,+rdm,+sha2,+v8.5a,+zcm,+zcz" }
+attributes #1 = { nofree nosync nounwind readnone speculatable willreturn }
+attributes #2 = { "frame-pointer"="non-leaf" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="apple-m1" "target-features"="+aes,+crc,+crypto,+dotprod,+fp-armv8,+fp16fml,+fullfp16,+lse,+neon,+ras,+rcpc,+rdm,+sha2,+v8.5a,+zcm,+zcz" }
+
+!llvm.dbg.cu = !{!2}
+!llvm.module.flags = !{!12, !13, !14, !15, !16, !17, !18, !19, !20, !21}
+!llvm.ident = !{!22}
+
+!0 = !DIGlobalVariableExpression(var: !1, expr: !DIExpression())
+!1 = distinct !DIGlobalVariable(name: "x", scope: !2, file: !7, line: 8, type: !8, isLocal: false, isDefinition: true)
+!2 = distinct !DICompileUnit(language: DW_LANG_C99, file: !3, producer: "Homebrew clang version 14.0.6", isOptimized: false, runtimeVersion: 0, emissionKind: FullDebug, retainedTypes: !4, globals: !6, splitDebugInlining: false, nameTableKind: None, sysroot: "/Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk", sdk: "MacOSX13.sdk")
+!3 = !DIFile(filename: "/Users/thomashaas/IdeaProjects/Dat3M/benchmarks/progress/progressFair.c", directory: "/Users/thomashaas/IdeaProjects/Dat3M")
+!4 = !{!5}
+!5 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: null, size: 64)
+!6 = !{!0}
+!7 = !DIFile(filename: "benchmarks/progress/progressFair.c", directory: "/Users/thomashaas/IdeaProjects/Dat3M")
+!8 = !DIDerivedType(tag: DW_TAG_typedef, name: "atomic_int", file: !9, line: 92, baseType: !10)
+!9 = !DIFile(filename: "/opt/homebrew/Cellar/llvm@14/14.0.6/lib/clang/14.0.6/include/stdatomic.h", directory: "")
+!10 = !DIDerivedType(tag: DW_TAG_atomic_type, baseType: !11)
+!11 = !DIBasicType(name: "int", size: 32, encoding: DW_ATE_signed)
+!12 = !{i32 7, !"Dwarf Version", i32 4}
+!13 = !{i32 2, !"Debug Info Version", i32 3}
+!14 = !{i32 1, !"wchar_size", i32 4}
+!15 = !{i32 1, !"branch-target-enforcement", i32 0}
+!16 = !{i32 1, !"sign-return-address", i32 0}
+!17 = !{i32 1, !"sign-return-address-all", i32 0}
+!18 = !{i32 1, !"sign-return-address-with-bkey", i32 0}
+!19 = !{i32 7, !"PIC Level", i32 2}
+!20 = !{i32 7, !"uwtable", i32 1}
+!21 = !{i32 7, !"frame-pointer", i32 1}
+!22 = !{!"Homebrew clang version 14.0.6"}
+!23 = distinct !DISubprogram(name: "thread_1", scope: !7, file: !7, line: 10, type: !24, scopeLine: 11, flags: DIFlagPrototyped, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !26)
+!24 = !DISubroutineType(types: !25)
+!25 = !{!5, !5}
+!26 = !{}
+!27 = !DILocalVariable(name: "unused", arg: 1, scope: !23, file: !7, line: 10, type: !5)
+!28 = !DILocation(line: 0, scope: !23)
+!29 = !DILocation(line: 12, column: 5, scope: !23)
+!30 = !DILocation(line: 12, column: 12, scope: !23)
+!31 = !DILocation(line: 12, column: 14, scope: !23)
+!32 = distinct !{!32, !29, !33, !34}
+!33 = !DILocation(line: 12, column: 19, scope: !23)
+!34 = !{!"llvm.loop.mustprogress"}
+!35 = !DILocation(line: 13, column: 5, scope: !23)
+!36 = distinct !DISubprogram(name: "thread_2", scope: !7, file: !7, line: 16, type: !24, scopeLine: 17, flags: DIFlagPrototyped, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !26)
+!37 = !DILocalVariable(name: "unused", arg: 1, scope: !36, file: !7, line: 16, type: !5)
+!38 = !DILocation(line: 0, scope: !36)
+!39 = !DILocation(line: 18, column: 7, scope: !36)
+!40 = !DILocation(line: 19, column: 1, scope: !36)
+!41 = distinct !DISubprogram(name: "main", scope: !7, file: !7, line: 21, type: !42, scopeLine: 22, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !26)
+!42 = !DISubroutineType(types: !43)
+!43 = !{!11}
+!44 = !DILocalVariable(name: "t1", scope: !41, file: !7, line: 23, type: !45)
+!45 = !DIDerivedType(tag: DW_TAG_typedef, name: "pthread_t", file: !46, line: 31, baseType: !47)
+!46 = !DIFile(filename: "/Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk/usr/include/sys/_pthread/_pthread_t.h", directory: "")
+!47 = !DIDerivedType(tag: DW_TAG_typedef, name: "__darwin_pthread_t", file: !48, line: 118, baseType: !49)
+!48 = !DIFile(filename: "/Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk/usr/include/sys/_pthread/_pthread_types.h", directory: "")
+!49 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: !50, size: 64)
+!50 = distinct !DICompositeType(tag: DW_TAG_structure_type, name: "_opaque_pthread_t", file: !48, line: 103, size: 65536, elements: !51)
+!51 = !{!52, !54, !64}
+!52 = !DIDerivedType(tag: DW_TAG_member, name: "__sig", scope: !50, file: !48, line: 104, baseType: !53, size: 64)
+!53 = !DIBasicType(name: "long", size: 64, encoding: DW_ATE_signed)
+!54 = !DIDerivedType(tag: DW_TAG_member, name: "__cleanup_stack", scope: !50, file: !48, line: 105, baseType: !55, size: 64, offset: 64)
+!55 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: !56, size: 64)
+!56 = distinct !DICompositeType(tag: DW_TAG_structure_type, name: "__darwin_pthread_handler_rec", file: !48, line: 57, size: 192, elements: !57)
+!57 = !{!58, !62, !63}
+!58 = !DIDerivedType(tag: DW_TAG_member, name: "__routine", scope: !56, file: !48, line: 58, baseType: !59, size: 64)
+!59 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: !60, size: 64)
+!60 = !DISubroutineType(types: !61)
+!61 = !{null, !5}
+!62 = !DIDerivedType(tag: DW_TAG_member, name: "__arg", scope: !56, file: !48, line: 59, baseType: !5, size: 64, offset: 64)
+!63 = !DIDerivedType(tag: DW_TAG_member, name: "__next", scope: !56, file: !48, line: 60, baseType: !55, size: 64, offset: 128)
+!64 = !DIDerivedType(tag: DW_TAG_member, name: "__opaque", scope: !50, file: !48, line: 106, baseType: !65, size: 65408, offset: 128)
+!65 = !DICompositeType(tag: DW_TAG_array_type, baseType: !66, size: 65408, elements: !67)
+!66 = !DIBasicType(name: "char", size: 8, encoding: DW_ATE_signed_char)
+!67 = !{!68}
+!68 = !DISubrange(count: 8176)
+!69 = !DILocation(line: 23, column: 15, scope: !41)
+!70 = !DILocalVariable(name: "t2", scope: !41, file: !7, line: 23, type: !45)
+!71 = !DILocation(line: 23, column: 19, scope: !41)
+!72 = !DILocation(line: 24, column: 5, scope: !41)
+!73 = !DILocation(line: 25, column: 5, scope: !41)
+!74 = !DILocation(line: 26, column: 5, scope: !41)
diff --git a/dartagnan/src/test/resources/progress/progressHSA.ll b/dartagnan/src/test/resources/progress/progressHSA.ll
new file mode 100644
index 0000000000..f3a2447fda
--- /dev/null
+++ b/dartagnan/src/test/resources/progress/progressHSA.ll
@@ -0,0 +1,134 @@
+; ModuleID = '/Users/thomashaas/IdeaProjects/Dat3M/output/progressHSA.ll'
+source_filename = "/Users/thomashaas/IdeaProjects/Dat3M/benchmarks/progress/progressHSA.c"
+target datalayout = "e-m:o-i64:64-i128:128-n32:64-S128"
+target triple = "arm64-apple-macosx14.0.0"
+
+%struct._opaque_pthread_t = type { i64, %struct.__darwin_pthread_handler_rec*, [8176 x i8] }
+%struct.__darwin_pthread_handler_rec = type { void (i8*)*, i8*, %struct.__darwin_pthread_handler_rec* }
+%struct._opaque_pthread_attr_t = type { i64, [56 x i8] }
+
+@x = global i32 0, align 4, !dbg !0
+
+; Function Attrs: noinline nounwind ssp uwtable
+define i8* @thread_1(i8* noundef %0) #0 !dbg !23 {
+  call void @llvm.dbg.value(metadata i8* %0, metadata !27, metadata !DIExpression()), !dbg !28
+  store atomic i32 1, i32* @x seq_cst, align 4, !dbg !29
+  ret i8* undef, !dbg !30
+}
+
+; Function Attrs: nofree nosync nounwind readnone speculatable willreturn
+declare void @llvm.dbg.declare(metadata, metadata, metadata) #1
+
+; Function Attrs: noinline nounwind ssp uwtable
+define i8* @thread_2(i8* noundef %0) #0 !dbg !31 {
+  call void @llvm.dbg.value(metadata i8* %0, metadata !32, metadata !DIExpression()), !dbg !33
+  br label %2, !dbg !34
+
+2:                                                ; preds = %2, %1
+  %3 = load atomic i32, i32* @x seq_cst, align 4, !dbg !35
+  %4 = icmp ne i32 %3, 1, !dbg !36
+  br i1 %4, label %2, label %5, !dbg !34, !llvm.loop !37
+
+5:                                                ; preds = %2
+  ret i8* null, !dbg !40
+}
+
+; Function Attrs: noinline nounwind ssp uwtable
+define i32 @main() #0 !dbg !41 {
+  %1 = alloca %struct._opaque_pthread_t*, align 8
+  %2 = alloca %struct._opaque_pthread_t*, align 8
+  call void @llvm.dbg.declare(metadata %struct._opaque_pthread_t** %1, metadata !44, metadata !DIExpression()), !dbg !69
+  call void @llvm.dbg.declare(metadata %struct._opaque_pthread_t** %2, metadata !70, metadata !DIExpression()), !dbg !71
+  %3 = call i32 @pthread_create(%struct._opaque_pthread_t** noundef %1, %struct._opaque_pthread_attr_t* noundef null, i8* (i8*)* noundef @thread_1, i8* noundef null), !dbg !72
+  %4 = call i32 @pthread_create(%struct._opaque_pthread_t** noundef %2, %struct._opaque_pthread_attr_t* noundef null, i8* (i8*)* noundef @thread_2, i8* noundef null), !dbg !73
+  ret i32 0, !dbg !74
+}
+
+declare i32 @pthread_create(%struct._opaque_pthread_t** noundef, %struct._opaque_pthread_attr_t* noundef, i8* (i8*)* noundef, i8* noundef) #2
+
+; Function Attrs: nofree nosync nounwind readnone speculatable willreturn
+declare void @llvm.dbg.value(metadata, metadata, metadata) #1
+
+attributes #0 = { noinline nounwind ssp uwtable "frame-pointer"="non-leaf" "min-legal-vector-width"="0" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="apple-m1" "target-features"="+aes,+crc,+crypto,+dotprod,+fp-armv8,+fp16fml,+fullfp16,+lse,+neon,+ras,+rcpc,+rdm,+sha2,+v8.5a,+zcm,+zcz" }
+attributes #1 = { nofree nosync nounwind readnone speculatable willreturn }
+attributes #2 = { "frame-pointer"="non-leaf" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="apple-m1" "target-features"="+aes,+crc,+crypto,+dotprod,+fp-armv8,+fp16fml,+fullfp16,+lse,+neon,+ras,+rcpc,+rdm,+sha2,+v8.5a,+zcm,+zcz" }
+
+!llvm.dbg.cu = !{!2}
+!llvm.module.flags = !{!12, !13, !14, !15, !16, !17, !18, !19, !20, !21}
+!llvm.ident = !{!22}
+
+!0 = !DIGlobalVariableExpression(var: !1, expr: !DIExpression())
+!1 = distinct !DIGlobalVariable(name: "x", scope: !2, file: !7, line: 8, type: !8, isLocal: false, isDefinition: true)
+!2 = distinct !DICompileUnit(language: DW_LANG_C99, file: !3, producer: "Homebrew clang version 14.0.6", isOptimized: false, runtimeVersion: 0, emissionKind: FullDebug, retainedTypes: !4, globals: !6, splitDebugInlining: false, nameTableKind: None, sysroot: "/Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk", sdk: "MacOSX13.sdk")
+!3 = !DIFile(filename: "/Users/thomashaas/IdeaProjects/Dat3M/benchmarks/progress/progressHSA.c", directory: "/Users/thomashaas/IdeaProjects/Dat3M")
+!4 = !{!5}
+!5 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: null, size: 64)
+!6 = !{!0}
+!7 = !DIFile(filename: "benchmarks/progress/progressHSA.c", directory: "/Users/thomashaas/IdeaProjects/Dat3M")
+!8 = !DIDerivedType(tag: DW_TAG_typedef, name: "atomic_int", file: !9, line: 92, baseType: !10)
+!9 = !DIFile(filename: "/opt/homebrew/Cellar/llvm@14/14.0.6/lib/clang/14.0.6/include/stdatomic.h", directory: "")
+!10 = !DIDerivedType(tag: DW_TAG_atomic_type, baseType: !11)
+!11 = !DIBasicType(name: "int", size: 32, encoding: DW_ATE_signed)
+!12 = !{i32 7, !"Dwarf Version", i32 4}
+!13 = !{i32 2, !"Debug Info Version", i32 3}
+!14 = !{i32 1, !"wchar_size", i32 4}
+!15 = !{i32 1, !"branch-target-enforcement", i32 0}
+!16 = !{i32 1, !"sign-return-address", i32 0}
+!17 = !{i32 1, !"sign-return-address-all", i32 0}
+!18 = !{i32 1, !"sign-return-address-with-bkey", i32 0}
+!19 = !{i32 7, !"PIC Level", i32 2}
+!20 = !{i32 7, !"uwtable", i32 1}
+!21 = !{i32 7, !"frame-pointer", i32 1}
+!22 = !{!"Homebrew clang version 14.0.6"}
+!23 = distinct !DISubprogram(name: "thread_1", scope: !7, file: !7, line: 10, type: !24, scopeLine: 11, flags: DIFlagPrototyped, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !26)
+!24 = !DISubroutineType(types: !25)
+!25 = !{!5, !5}
+!26 = !{}
+!27 = !DILocalVariable(name: "unused", arg: 1, scope: !23, file: !7, line: 10, type: !5)
+!28 = !DILocation(line: 0, scope: !23)
+!29 = !DILocation(line: 12, column: 7, scope: !23)
+!30 = !DILocation(line: 13, column: 1, scope: !23)
+!31 = distinct !DISubprogram(name: "thread_2", scope: !7, file: !7, line: 15, type: !24, scopeLine: 16, flags: DIFlagPrototyped, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !26)
+!32 = !DILocalVariable(name: "unused", arg: 1, scope: !31, file: !7, line: 15, type: !5)
+!33 = !DILocation(line: 0, scope: !31)
+!34 = !DILocation(line: 17, column: 5, scope: !31)
+!35 = !DILocation(line: 17, column: 12, scope: !31)
+!36 = !DILocation(line: 17, column: 14, scope: !31)
+!37 = distinct !{!37, !34, !38, !39}
+!38 = !DILocation(line: 17, column: 19, scope: !31)
+!39 = !{!"llvm.loop.mustprogress"}
+!40 = !DILocation(line: 18, column: 5, scope: !31)
+!41 = distinct !DISubprogram(name: "main", scope: !7, file: !7, line: 21, type: !42, scopeLine: 22, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !26)
+!42 = !DISubroutineType(types: !43)
+!43 = !{!11}
+!44 = !DILocalVariable(name: "t1", scope: !41, file: !7, line: 23, type: !45)
+!45 = !DIDerivedType(tag: DW_TAG_typedef, name: "pthread_t", file: !46, line: 31, baseType: !47)
+!46 = !DIFile(filename: "/Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk/usr/include/sys/_pthread/_pthread_t.h", directory: "")
+!47 = !DIDerivedType(tag: DW_TAG_typedef, name: "__darwin_pthread_t", file: !48, line: 118, baseType: !49)
+!48 = !DIFile(filename: "/Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk/usr/include/sys/_pthread/_pthread_types.h", directory: "")
+!49 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: !50, size: 64)
+!50 = distinct !DICompositeType(tag: DW_TAG_structure_type, name: "_opaque_pthread_t", file: !48, line: 103, size: 65536, elements: !51)
+!51 = !{!52, !54, !64}
+!52 = !DIDerivedType(tag: DW_TAG_member, name: "__sig", scope: !50, file: !48, line: 104, baseType: !53, size: 64)
+!53 = !DIBasicType(name: "long", size: 64, encoding: DW_ATE_signed)
+!54 = !DIDerivedType(tag: DW_TAG_member, name: "__cleanup_stack", scope: !50, file: !48, line: 105, baseType: !55, size: 64, offset: 64)
+!55 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: !56, size: 64)
+!56 = distinct !DICompositeType(tag: DW_TAG_structure_type, name: "__darwin_pthread_handler_rec", file: !48, line: 57, size: 192, elements: !57)
+!57 = !{!58, !62, !63}
+!58 = !DIDerivedType(tag: DW_TAG_member, name: "__routine", scope: !56, file: !48, line: 58, baseType: !59, size: 64)
+!59 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: !60, size: 64)
+!60 = !DISubroutineType(types: !61)
+!61 = !{null, !5}
+!62 = !DIDerivedType(tag: DW_TAG_member, name: "__arg", scope: !56, file: !48, line: 59, baseType: !5, size: 64, offset: 64)
+!63 = !DIDerivedType(tag: DW_TAG_member, name: "__next", scope: !56, file: !48, line: 60, baseType: !55, size: 64, offset: 128)
+!64 = !DIDerivedType(tag: DW_TAG_member, name: "__opaque", scope: !50, file: !48, line: 106, baseType: !65, size: 65408, offset: 128)
+!65 = !DICompositeType(tag: DW_TAG_array_type, baseType: !66, size: 65408, elements: !67)
+!66 = !DIBasicType(name: "char", size: 8, encoding: DW_ATE_signed_char)
+!67 = !{!68}
+!68 = !DISubrange(count: 8176)
+!69 = !DILocation(line: 23, column: 15, scope: !41)
+!70 = !DILocalVariable(name: "t2", scope: !41, file: !7, line: 23, type: !45)
+!71 = !DILocation(line: 23, column: 19, scope: !41)
+!72 = !DILocation(line: 24, column: 5, scope: !41)
+!73 = !DILocation(line: 25, column: 5, scope: !41)
+!74 = !DILocation(line: 26, column: 5, scope: !41)
diff --git a/dartagnan/src/test/resources/progress/progressOBE-HSA.ll b/dartagnan/src/test/resources/progress/progressOBE-HSA.ll
new file mode 100644
index 0000000000..fcbc352d76
--- /dev/null
+++ b/dartagnan/src/test/resources/progress/progressOBE-HSA.ll
@@ -0,0 +1,123 @@
+; ModuleID = '/Users/thomashaas/IdeaProjects/Dat3M/output/progressOBE-HSA.ll'
+source_filename = "/Users/thomashaas/IdeaProjects/Dat3M/benchmarks/progress/progressOBE-HSA.c"
+target datalayout = "e-m:o-i64:64-i128:128-n32:64-S128"
+target triple = "arm64-apple-macosx14.0.0"
+
+%struct._opaque_pthread_t = type { i64, %struct.__darwin_pthread_handler_rec*, [8176 x i8] }
+%struct.__darwin_pthread_handler_rec = type { void (i8*)*, i8*, %struct.__darwin_pthread_handler_rec* }
+%struct._opaque_pthread_attr_t = type { i64, [56 x i8] }
+
+@x = global i32 0, align 4, !dbg !0
+
+; Function Attrs: noinline nounwind ssp uwtable
+define i8* @thread_1(i8* noundef %0) #0 !dbg !23 {
+  call void @llvm.dbg.value(metadata i8* %0, metadata !27, metadata !DIExpression()), !dbg !28
+  br label %2, !dbg !29
+
+2:                                                ; preds = %2, %1
+  %3 = load atomic i32, i32* @x seq_cst, align 4, !dbg !30
+  %4 = icmp ne i32 %3, 0, !dbg !31
+  br i1 %4, label %2, label %5, !dbg !29, !llvm.loop !32
+
+5:                                                ; preds = %2
+  ret i8* null, !dbg !35
+}
+
+; Function Attrs: nofree nosync nounwind readnone speculatable willreturn
+declare void @llvm.dbg.declare(metadata, metadata, metadata) #1
+
+; Function Attrs: noinline nounwind ssp uwtable
+define i32 @main() #0 !dbg !36 {
+  %1 = alloca %struct._opaque_pthread_t*, align 8
+  call void @llvm.dbg.declare(metadata %struct._opaque_pthread_t** %1, metadata !39, metadata !DIExpression()), !dbg !64
+  call void @llvm.dbg.declare(metadata %struct._opaque_pthread_t** undef, metadata !65, metadata !DIExpression()), !dbg !66
+  %2 = call i32 @pthread_create(%struct._opaque_pthread_t** noundef %1, %struct._opaque_pthread_attr_t* noundef null, i8* (i8*)* noundef @thread_1, i8* noundef null), !dbg !67
+  store atomic i32 1, i32* @x seq_cst, align 4, !dbg !68
+  store atomic i32 0, i32* @x seq_cst, align 4, !dbg !69
+  ret i32 0, !dbg !70
+}
+
+declare i32 @pthread_create(%struct._opaque_pthread_t** noundef, %struct._opaque_pthread_attr_t* noundef, i8* (i8*)* noundef, i8* noundef) #2
+
+; Function Attrs: nofree nosync nounwind readnone speculatable willreturn
+declare void @llvm.dbg.value(metadata, metadata, metadata) #1
+
+attributes #0 = { noinline nounwind ssp uwtable "frame-pointer"="non-leaf" "min-legal-vector-width"="0" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="apple-m1" "target-features"="+aes,+crc,+crypto,+dotprod,+fp-armv8,+fp16fml,+fullfp16,+lse,+neon,+ras,+rcpc,+rdm,+sha2,+v8.5a,+zcm,+zcz" }
+attributes #1 = { nofree nosync nounwind readnone speculatable willreturn }
+attributes #2 = { "frame-pointer"="non-leaf" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="apple-m1" "target-features"="+aes,+crc,+crypto,+dotprod,+fp-armv8,+fp16fml,+fullfp16,+lse,+neon,+ras,+rcpc,+rdm,+sha2,+v8.5a,+zcm,+zcz" }
+
+!llvm.dbg.cu = !{!2}
+!llvm.module.flags = !{!12, !13, !14, !15, !16, !17, !18, !19, !20, !21}
+!llvm.ident = !{!22}
+
+!0 = !DIGlobalVariableExpression(var: !1, expr: !DIExpression())
+!1 = distinct !DIGlobalVariable(name: "x", scope: !2, file: !7, line: 8, type: !8, isLocal: false, isDefinition: true)
+!2 = distinct !DICompileUnit(language: DW_LANG_C99, file: !3, producer: "Homebrew clang version 14.0.6", isOptimized: false, runtimeVersion: 0, emissionKind: FullDebug, retainedTypes: !4, globals: !6, splitDebugInlining: false, nameTableKind: None, sysroot: "/Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk", sdk: "MacOSX13.sdk")
+!3 = !DIFile(filename: "/Users/thomashaas/IdeaProjects/Dat3M/benchmarks/progress/progressOBE-HSA.c", directory: "/Users/thomashaas/IdeaProjects/Dat3M")
+!4 = !{!5}
+!5 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: null, size: 64)
+!6 = !{!0}
+!7 = !DIFile(filename: "benchmarks/progress/progressOBE-HSA.c", directory: "/Users/thomashaas/IdeaProjects/Dat3M")
+!8 = !DIDerivedType(tag: DW_TAG_typedef, name: "atomic_int", file: !9, line: 92, baseType: !10)
+!9 = !DIFile(filename: "/opt/homebrew/Cellar/llvm@14/14.0.6/lib/clang/14.0.6/include/stdatomic.h", directory: "")
+!10 = !DIDerivedType(tag: DW_TAG_atomic_type, baseType: !11)
+!11 = !DIBasicType(name: "int", size: 32, encoding: DW_ATE_signed)
+!12 = !{i32 7, !"Dwarf Version", i32 4}
+!13 = !{i32 2, !"Debug Info Version", i32 3}
+!14 = !{i32 1, !"wchar_size", i32 4}
+!15 = !{i32 1, !"branch-target-enforcement", i32 0}
+!16 = !{i32 1, !"sign-return-address", i32 0}
+!17 = !{i32 1, !"sign-return-address-all", i32 0}
+!18 = !{i32 1, !"sign-return-address-with-bkey", i32 0}
+!19 = !{i32 7, !"PIC Level", i32 2}
+!20 = !{i32 7, !"uwtable", i32 1}
+!21 = !{i32 7, !"frame-pointer", i32 1}
+!22 = !{!"Homebrew clang version 14.0.6"}
+!23 = distinct !DISubprogram(name: "thread_1", scope: !7, file: !7, line: 10, type: !24, scopeLine: 11, flags: DIFlagPrototyped, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !26)
+!24 = !DISubroutineType(types: !25)
+!25 = !{!5, !5}
+!26 = !{}
+!27 = !DILocalVariable(name: "unused", arg: 1, scope: !23, file: !7, line: 10, type: !5)
+!28 = !DILocation(line: 0, scope: !23)
+!29 = !DILocation(line: 12, column: 5, scope: !23)
+!30 = !DILocation(line: 12, column: 12, scope: !23)
+!31 = !DILocation(line: 12, column: 14, scope: !23)
+!32 = distinct !{!32, !29, !33, !34}
+!33 = !DILocation(line: 12, column: 19, scope: !23)
+!34 = !{!"llvm.loop.mustprogress"}
+!35 = !DILocation(line: 13, column: 5, scope: !23)
+!36 = distinct !DISubprogram(name: "main", scope: !7, file: !7, line: 16, type: !37, scopeLine: 17, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !26)
+!37 = !DISubroutineType(types: !38)
+!38 = !{!11}
+!39 = !DILocalVariable(name: "t1", scope: !36, file: !7, line: 18, type: !40)
+!40 = !DIDerivedType(tag: DW_TAG_typedef, name: "pthread_t", file: !41, line: 31, baseType: !42)
+!41 = !DIFile(filename: "/Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk/usr/include/sys/_pthread/_pthread_t.h", directory: "")
+!42 = !DIDerivedType(tag: DW_TAG_typedef, name: "__darwin_pthread_t", file: !43, line: 118, baseType: !44)
+!43 = !DIFile(filename: "/Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk/usr/include/sys/_pthread/_pthread_types.h", directory: "")
+!44 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: !45, size: 64)
+!45 = distinct !DICompositeType(tag: DW_TAG_structure_type, name: "_opaque_pthread_t", file: !43, line: 103, size: 65536, elements: !46)
+!46 = !{!47, !49, !59}
+!47 = !DIDerivedType(tag: DW_TAG_member, name: "__sig", scope: !45, file: !43, line: 104, baseType: !48, size: 64)
+!48 = !DIBasicType(name: "long", size: 64, encoding: DW_ATE_signed)
+!49 = !DIDerivedType(tag: DW_TAG_member, name: "__cleanup_stack", scope: !45, file: !43, line: 105, baseType: !50, size: 64, offset: 64)
+!50 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: !51, size: 64)
+!51 = distinct !DICompositeType(tag: DW_TAG_structure_type, name: "__darwin_pthread_handler_rec", file: !43, line: 57, size: 192, elements: !52)
+!52 = !{!53, !57, !58}
+!53 = !DIDerivedType(tag: DW_TAG_member, name: "__routine", scope: !51, file: !43, line: 58, baseType: !54, size: 64)
+!54 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: !55, size: 64)
+!55 = !DISubroutineType(types: !56)
+!56 = !{null, !5}
+!57 = !DIDerivedType(tag: DW_TAG_member, name: "__arg", scope: !51, file: !43, line: 59, baseType: !5, size: 64, offset: 64)
+!58 = !DIDerivedType(tag: DW_TAG_member, name: "__next", scope: !51, file: !43, line: 60, baseType: !50, size: 64, offset: 128)
+!59 = !DIDerivedType(tag: DW_TAG_member, name: "__opaque", scope: !45, file: !43, line: 106, baseType: !60, size: 65408, offset: 128)
+!60 = !DICompositeType(tag: DW_TAG_array_type, baseType: !61, size: 65408, elements: !62)
+!61 = !DIBasicType(name: "char", size: 8, encoding: DW_ATE_signed_char)
+!62 = !{!63}
+!63 = !DISubrange(count: 8176)
+!64 = !DILocation(line: 18, column: 15, scope: !36)
+!65 = !DILocalVariable(name: "t2", scope: !36, file: !7, line: 18, type: !40)
+!66 = !DILocation(line: 18, column: 19, scope: !36)
+!67 = !DILocation(line: 19, column: 5, scope: !36)
+!68 = !DILocation(line: 20, column: 7, scope: !36)
+!69 = !DILocation(line: 22, column: 7, scope: !36)
+!70 = !DILocation(line: 23, column: 5, scope: !36)
diff --git a/dartagnan/src/test/resources/progress/progressOBE.ll b/dartagnan/src/test/resources/progress/progressOBE.ll
new file mode 100644
index 0000000000..28c25a00fc
--- /dev/null
+++ b/dartagnan/src/test/resources/progress/progressOBE.ll
@@ -0,0 +1,136 @@
+; ModuleID = '/Users/thomashaas/IdeaProjects/Dat3M/output/progressOBE.ll'
+source_filename = "/Users/thomashaas/IdeaProjects/Dat3M/benchmarks/progress/progressOBE.c"
+target datalayout = "e-m:o-i64:64-i128:128-n32:64-S128"
+target triple = "arm64-apple-macosx14.0.0"
+
+%struct._opaque_pthread_t = type { i64, %struct.__darwin_pthread_handler_rec*, [8176 x i8] }
+%struct.__darwin_pthread_handler_rec = type { void (i8*)*, i8*, %struct.__darwin_pthread_handler_rec* }
+%struct._opaque_pthread_attr_t = type { i64, [56 x i8] }
+
+@x = global i32 0, align 4, !dbg !0
+
+; Function Attrs: noinline nounwind ssp uwtable
+define i8* @thread_1(i8* noundef %0) #0 !dbg !23 {
+  call void @llvm.dbg.value(metadata i8* %0, metadata !27, metadata !DIExpression()), !dbg !28
+  br label %2, !dbg !29
+
+2:                                                ; preds = %2, %1
+  %3 = load atomic i32, i32* @x seq_cst, align 4, !dbg !30
+  %4 = icmp ne i32 %3, 0, !dbg !31
+  br i1 %4, label %2, label %5, !dbg !29, !llvm.loop !32
+
+5:                                                ; preds = %2
+  ret i8* null, !dbg !35
+}
+
+; Function Attrs: nofree nosync nounwind readnone speculatable willreturn
+declare void @llvm.dbg.declare(metadata, metadata, metadata) #1
+
+; Function Attrs: noinline nounwind ssp uwtable
+define i8* @thread_2(i8* noundef %0) #0 !dbg !36 {
+  call void @llvm.dbg.value(metadata i8* %0, metadata !37, metadata !DIExpression()), !dbg !38
+  store atomic i32 1, i32* @x seq_cst, align 4, !dbg !39
+  store atomic i32 0, i32* @x seq_cst, align 4, !dbg !40
+  ret i8* undef, !dbg !41
+}
+
+; Function Attrs: noinline nounwind ssp uwtable
+define i32 @main() #0 !dbg !42 {
+  %1 = alloca %struct._opaque_pthread_t*, align 8
+  %2 = alloca %struct._opaque_pthread_t*, align 8
+  call void @llvm.dbg.declare(metadata %struct._opaque_pthread_t** %1, metadata !45, metadata !DIExpression()), !dbg !70
+  call void @llvm.dbg.declare(metadata %struct._opaque_pthread_t** %2, metadata !71, metadata !DIExpression()), !dbg !72
+  %3 = call i32 @pthread_create(%struct._opaque_pthread_t** noundef %1, %struct._opaque_pthread_attr_t* noundef null, i8* (i8*)* noundef @thread_1, i8* noundef null), !dbg !73
+  %4 = call i32 @pthread_create(%struct._opaque_pthread_t** noundef %2, %struct._opaque_pthread_attr_t* noundef null, i8* (i8*)* noundef @thread_2, i8* noundef null), !dbg !74
+  ret i32 0, !dbg !75
+}
+
+declare i32 @pthread_create(%struct._opaque_pthread_t** noundef, %struct._opaque_pthread_attr_t* noundef, i8* (i8*)* noundef, i8* noundef) #2
+
+; Function Attrs: nofree nosync nounwind readnone speculatable willreturn
+declare void @llvm.dbg.value(metadata, metadata, metadata) #1
+
+attributes #0 = { noinline nounwind ssp uwtable "frame-pointer"="non-leaf" "min-legal-vector-width"="0" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="apple-m1" "target-features"="+aes,+crc,+crypto,+dotprod,+fp-armv8,+fp16fml,+fullfp16,+lse,+neon,+ras,+rcpc,+rdm,+sha2,+v8.5a,+zcm,+zcz" }
+attributes #1 = { nofree nosync nounwind readnone speculatable willreturn }
+attributes #2 = { "frame-pointer"="non-leaf" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="apple-m1" "target-features"="+aes,+crc,+crypto,+dotprod,+fp-armv8,+fp16fml,+fullfp16,+lse,+neon,+ras,+rcpc,+rdm,+sha2,+v8.5a,+zcm,+zcz" }
+
+!llvm.dbg.cu = !{!2}
+!llvm.module.flags = !{!12, !13, !14, !15, !16, !17, !18, !19, !20, !21}
+!llvm.ident = !{!22}
+
+!0 = !DIGlobalVariableExpression(var: !1, expr: !DIExpression())
+!1 = distinct !DIGlobalVariable(name: "x", scope: !2, file: !7, line: 8, type: !8, isLocal: false, isDefinition: true)
+!2 = distinct !DICompileUnit(language: DW_LANG_C99, file: !3, producer: "Homebrew clang version 14.0.6", isOptimized: false, runtimeVersion: 0, emissionKind: FullDebug, retainedTypes: !4, globals: !6, splitDebugInlining: false, nameTableKind: None, sysroot: "/Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk", sdk: "MacOSX13.sdk")
+!3 = !DIFile(filename: "/Users/thomashaas/IdeaProjects/Dat3M/benchmarks/progress/progressOBE.c", directory: "/Users/thomashaas/IdeaProjects/Dat3M")
+!4 = !{!5}
+!5 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: null, size: 64)
+!6 = !{!0}
+!7 = !DIFile(filename: "benchmarks/progress/progressOBE.c", directory: "/Users/thomashaas/IdeaProjects/Dat3M")
+!8 = !DIDerivedType(tag: DW_TAG_typedef, name: "atomic_int", file: !9, line: 92, baseType: !10)
+!9 = !DIFile(filename: "/opt/homebrew/Cellar/llvm@14/14.0.6/lib/clang/14.0.6/include/stdatomic.h", directory: "")
+!10 = !DIDerivedType(tag: DW_TAG_atomic_type, baseType: !11)
+!11 = !DIBasicType(name: "int", size: 32, encoding: DW_ATE_signed)
+!12 = !{i32 7, !"Dwarf Version", i32 4}
+!13 = !{i32 2, !"Debug Info Version", i32 3}
+!14 = !{i32 1, !"wchar_size", i32 4}
+!15 = !{i32 1, !"branch-target-enforcement", i32 0}
+!16 = !{i32 1, !"sign-return-address", i32 0}
+!17 = !{i32 1, !"sign-return-address-all", i32 0}
+!18 = !{i32 1, !"sign-return-address-with-bkey", i32 0}
+!19 = !{i32 7, !"PIC Level", i32 2}
+!20 = !{i32 7, !"uwtable", i32 1}
+!21 = !{i32 7, !"frame-pointer", i32 1}
+!22 = !{!"Homebrew clang version 14.0.6"}
+!23 = distinct !DISubprogram(name: "thread_1", scope: !7, file: !7, line: 10, type: !24, scopeLine: 11, flags: DIFlagPrototyped, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !26)
+!24 = !DISubroutineType(types: !25)
+!25 = !{!5, !5}
+!26 = !{}
+!27 = !DILocalVariable(name: "unused", arg: 1, scope: !23, file: !7, line: 10, type: !5)
+!28 = !DILocation(line: 0, scope: !23)
+!29 = !DILocation(line: 12, column: 5, scope: !23)
+!30 = !DILocation(line: 12, column: 12, scope: !23)
+!31 = !DILocation(line: 12, column: 14, scope: !23)
+!32 = distinct !{!32, !29, !33, !34}
+!33 = !DILocation(line: 12, column: 19, scope: !23)
+!34 = !{!"llvm.loop.mustprogress"}
+!35 = !DILocation(line: 13, column: 5, scope: !23)
+!36 = distinct !DISubprogram(name: "thread_2", scope: !7, file: !7, line: 16, type: !24, scopeLine: 17, flags: DIFlagPrototyped, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !26)
+!37 = !DILocalVariable(name: "unused", arg: 1, scope: !36, file: !7, line: 16, type: !5)
+!38 = !DILocation(line: 0, scope: !36)
+!39 = !DILocation(line: 18, column: 7, scope: !36)
+!40 = !DILocation(line: 20, column: 7, scope: !36)
+!41 = !DILocation(line: 21, column: 1, scope: !36)
+!42 = distinct !DISubprogram(name: "main", scope: !7, file: !7, line: 23, type: !43, scopeLine: 24, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !26)
+!43 = !DISubroutineType(types: !44)
+!44 = !{!11}
+!45 = !DILocalVariable(name: "t1", scope: !42, file: !7, line: 25, type: !46)
+!46 = !DIDerivedType(tag: DW_TAG_typedef, name: "pthread_t", file: !47, line: 31, baseType: !48)
+!47 = !DIFile(filename: "/Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk/usr/include/sys/_pthread/_pthread_t.h", directory: "")
+!48 = !DIDerivedType(tag: DW_TAG_typedef, name: "__darwin_pthread_t", file: !49, line: 118, baseType: !50)
+!49 = !DIFile(filename: "/Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk/usr/include/sys/_pthread/_pthread_types.h", directory: "")
+!50 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: !51, size: 64)
+!51 = distinct !DICompositeType(tag: DW_TAG_structure_type, name: "_opaque_pthread_t", file: !49, line: 103, size: 65536, elements: !52)
+!52 = !{!53, !55, !65}
+!53 = !DIDerivedType(tag: DW_TAG_member, name: "__sig", scope: !51, file: !49, line: 104, baseType: !54, size: 64)
+!54 = !DIBasicType(name: "long", size: 64, encoding: DW_ATE_signed)
+!55 = !DIDerivedType(tag: DW_TAG_member, name: "__cleanup_stack", scope: !51, file: !49, line: 105, baseType: !56, size: 64, offset: 64)
+!56 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: !57, size: 64)
+!57 = distinct !DICompositeType(tag: DW_TAG_structure_type, name: "__darwin_pthread_handler_rec", file: !49, line: 57, size: 192, elements: !58)
+!58 = !{!59, !63, !64}
+!59 = !DIDerivedType(tag: DW_TAG_member, name: "__routine", scope: !57, file: !49, line: 58, baseType: !60, size: 64)
+!60 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: !61, size: 64)
+!61 = !DISubroutineType(types: !62)
+!62 = !{null, !5}
+!63 = !DIDerivedType(tag: DW_TAG_member, name: "__arg", scope: !57, file: !49, line: 59, baseType: !5, size: 64, offset: 64)
+!64 = !DIDerivedType(tag: DW_TAG_member, name: "__next", scope: !57, file: !49, line: 60, baseType: !56, size: 64, offset: 128)
+!65 = !DIDerivedType(tag: DW_TAG_member, name: "__opaque", scope: !51, file: !49, line: 106, baseType: !66, size: 65408, offset: 128)
+!66 = !DICompositeType(tag: DW_TAG_array_type, baseType: !67, size: 65408, elements: !68)
+!67 = !DIBasicType(name: "char", size: 8, encoding: DW_ATE_signed_char)
+!68 = !{!69}
+!69 = !DISubrange(count: 8176)
+!70 = !DILocation(line: 25, column: 15, scope: !42)
+!71 = !DILocalVariable(name: "t2", scope: !42, file: !7, line: 25, type: !46)
+!72 = !DILocation(line: 25, column: 19, scope: !42)
+!73 = !DILocation(line: 26, column: 5, scope: !42)
+!74 = !DILocation(line: 27, column: 5, scope: !42)
+!75 = !DILocation(line: 28, column: 5, scope: !42)
diff --git a/dartagnan/src/test/resources/progress/progressUnfair.ll b/dartagnan/src/test/resources/progress/progressUnfair.ll
new file mode 100644
index 0000000000..12eb796dd9
--- /dev/null
+++ b/dartagnan/src/test/resources/progress/progressUnfair.ll
@@ -0,0 +1,121 @@
+; ModuleID = '/Users/thomashaas/IdeaProjects/Dat3M/output/progressUnfair.ll'
+source_filename = "/Users/thomashaas/IdeaProjects/Dat3M/benchmarks/progress/progressUnfair.c"
+target datalayout = "e-m:o-i64:64-i128:128-n32:64-S128"
+target triple = "arm64-apple-macosx14.0.0"
+
+%struct._opaque_pthread_t = type { i64, %struct.__darwin_pthread_handler_rec*, [8176 x i8] }
+%struct.__darwin_pthread_handler_rec = type { void (i8*)*, i8*, %struct.__darwin_pthread_handler_rec* }
+%struct._opaque_pthread_attr_t = type { i64, [56 x i8] }
+
+@x = global i32 0, align 4, !dbg !0
+
+; Function Attrs: noinline nounwind ssp uwtable
+define i8* @thread_1(i8* noundef %0) #0 !dbg !23 {
+  call void @llvm.dbg.value(metadata i8* %0, metadata !27, metadata !DIExpression()), !dbg !28
+  br label %2, !dbg !29
+
+2:                                                ; preds = %2, %1
+  %3 = load atomic i32, i32* @x seq_cst, align 4, !dbg !30
+  %4 = icmp ne i32 %3, 1, !dbg !31
+  br i1 %4, label %2, label %5, !dbg !29, !llvm.loop !32
+
+5:                                                ; preds = %2
+  ret i8* null, !dbg !35
+}
+
+; Function Attrs: nofree nosync nounwind readnone speculatable willreturn
+declare void @llvm.dbg.declare(metadata, metadata, metadata) #1
+
+; Function Attrs: noinline nounwind ssp uwtable
+define i32 @main() #0 !dbg !36 {
+  %1 = alloca %struct._opaque_pthread_t*, align 8
+  call void @llvm.dbg.declare(metadata %struct._opaque_pthread_t** %1, metadata !39, metadata !DIExpression()), !dbg !64
+  call void @llvm.dbg.declare(metadata %struct._opaque_pthread_t** undef, metadata !65, metadata !DIExpression()), !dbg !66
+  store atomic i32 1, i32* @x seq_cst, align 4, !dbg !67
+  %2 = call i32 @pthread_create(%struct._opaque_pthread_t** noundef %1, %struct._opaque_pthread_attr_t* noundef null, i8* (i8*)* noundef @thread_1, i8* noundef null), !dbg !68
+  ret i32 0, !dbg !69
+}
+
+declare i32 @pthread_create(%struct._opaque_pthread_t** noundef, %struct._opaque_pthread_attr_t* noundef, i8* (i8*)* noundef, i8* noundef) #2
+
+; Function Attrs: nofree nosync nounwind readnone speculatable willreturn
+declare void @llvm.dbg.value(metadata, metadata, metadata) #1
+
+attributes #0 = { noinline nounwind ssp uwtable "frame-pointer"="non-leaf" "min-legal-vector-width"="0" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="apple-m1" "target-features"="+aes,+crc,+crypto,+dotprod,+fp-armv8,+fp16fml,+fullfp16,+lse,+neon,+ras,+rcpc,+rdm,+sha2,+v8.5a,+zcm,+zcz" }
+attributes #1 = { nofree nosync nounwind readnone speculatable willreturn }
+attributes #2 = { "frame-pointer"="non-leaf" "no-trapping-math"="true" "stack-protector-buffer-size"="8" "target-cpu"="apple-m1" "target-features"="+aes,+crc,+crypto,+dotprod,+fp-armv8,+fp16fml,+fullfp16,+lse,+neon,+ras,+rcpc,+rdm,+sha2,+v8.5a,+zcm,+zcz" }
+
+!llvm.dbg.cu = !{!2}
+!llvm.module.flags = !{!12, !13, !14, !15, !16, !17, !18, !19, !20, !21}
+!llvm.ident = !{!22}
+
+!0 = !DIGlobalVariableExpression(var: !1, expr: !DIExpression())
+!1 = distinct !DIGlobalVariable(name: "x", scope: !2, file: !7, line: 6, type: !8, isLocal: false, isDefinition: true)
+!2 = distinct !DICompileUnit(language: DW_LANG_C99, file: !3, producer: "Homebrew clang version 14.0.6", isOptimized: false, runtimeVersion: 0, emissionKind: FullDebug, retainedTypes: !4, globals: !6, splitDebugInlining: false, nameTableKind: None, sysroot: "/Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk", sdk: "MacOSX13.sdk")
+!3 = !DIFile(filename: "/Users/thomashaas/IdeaProjects/Dat3M/benchmarks/progress/progressUnfair.c", directory: "/Users/thomashaas/IdeaProjects/Dat3M")
+!4 = !{!5}
+!5 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: null, size: 64)
+!6 = !{!0}
+!7 = !DIFile(filename: "benchmarks/progress/progressUnfair.c", directory: "/Users/thomashaas/IdeaProjects/Dat3M")
+!8 = !DIDerivedType(tag: DW_TAG_typedef, name: "atomic_int", file: !9, line: 92, baseType: !10)
+!9 = !DIFile(filename: "/opt/homebrew/Cellar/llvm@14/14.0.6/lib/clang/14.0.6/include/stdatomic.h", directory: "")
+!10 = !DIDerivedType(tag: DW_TAG_atomic_type, baseType: !11)
+!11 = !DIBasicType(name: "int", size: 32, encoding: DW_ATE_signed)
+!12 = !{i32 7, !"Dwarf Version", i32 4}
+!13 = !{i32 2, !"Debug Info Version", i32 3}
+!14 = !{i32 1, !"wchar_size", i32 4}
+!15 = !{i32 1, !"branch-target-enforcement", i32 0}
+!16 = !{i32 1, !"sign-return-address", i32 0}
+!17 = !{i32 1, !"sign-return-address-all", i32 0}
+!18 = !{i32 1, !"sign-return-address-with-bkey", i32 0}
+!19 = !{i32 7, !"PIC Level", i32 2}
+!20 = !{i32 7, !"uwtable", i32 1}
+!21 = !{i32 7, !"frame-pointer", i32 1}
+!22 = !{!"Homebrew clang version 14.0.6"}
+!23 = distinct !DISubprogram(name: "thread_1", scope: !7, file: !7, line: 10, type: !24, scopeLine: 11, flags: DIFlagPrototyped, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !26)
+!24 = !DISubroutineType(types: !25)
+!25 = !{!5, !5}
+!26 = !{}
+!27 = !DILocalVariable(name: "unused", arg: 1, scope: !23, file: !7, line: 10, type: !5)
+!28 = !DILocation(line: 0, scope: !23)
+!29 = !DILocation(line: 12, column: 5, scope: !23)
+!30 = !DILocation(line: 12, column: 12, scope: !23)
+!31 = !DILocation(line: 12, column: 14, scope: !23)
+!32 = distinct !{!32, !29, !33, !34}
+!33 = !DILocation(line: 12, column: 19, scope: !23)
+!34 = !{!"llvm.loop.mustprogress"}
+!35 = !DILocation(line: 13, column: 5, scope: !23)
+!36 = distinct !DISubprogram(name: "main", scope: !7, file: !7, line: 16, type: !37, scopeLine: 17, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !26)
+!37 = !DISubroutineType(types: !38)
+!38 = !{!11}
+!39 = !DILocalVariable(name: "t1", scope: !36, file: !7, line: 18, type: !40)
+!40 = !DIDerivedType(tag: DW_TAG_typedef, name: "pthread_t", file: !41, line: 31, baseType: !42)
+!41 = !DIFile(filename: "/Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk/usr/include/sys/_pthread/_pthread_t.h", directory: "")
+!42 = !DIDerivedType(tag: DW_TAG_typedef, name: "__darwin_pthread_t", file: !43, line: 118, baseType: !44)
+!43 = !DIFile(filename: "/Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk/usr/include/sys/_pthread/_pthread_types.h", directory: "")
+!44 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: !45, size: 64)
+!45 = distinct !DICompositeType(tag: DW_TAG_structure_type, name: "_opaque_pthread_t", file: !43, line: 103, size: 65536, elements: !46)
+!46 = !{!47, !49, !59}
+!47 = !DIDerivedType(tag: DW_TAG_member, name: "__sig", scope: !45, file: !43, line: 104, baseType: !48, size: 64)
+!48 = !DIBasicType(name: "long", size: 64, encoding: DW_ATE_signed)
+!49 = !DIDerivedType(tag: DW_TAG_member, name: "__cleanup_stack", scope: !45, file: !43, line: 105, baseType: !50, size: 64, offset: 64)
+!50 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: !51, size: 64)
+!51 = distinct !DICompositeType(tag: DW_TAG_structure_type, name: "__darwin_pthread_handler_rec", file: !43, line: 57, size: 192, elements: !52)
+!52 = !{!53, !57, !58}
+!53 = !DIDerivedType(tag: DW_TAG_member, name: "__routine", scope: !51, file: !43, line: 58, baseType: !54, size: 64)
+!54 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: !55, size: 64)
+!55 = !DISubroutineType(types: !56)
+!56 = !{null, !5}
+!57 = !DIDerivedType(tag: DW_TAG_member, name: "__arg", scope: !51, file: !43, line: 59, baseType: !5, size: 64, offset: 64)
+!58 = !DIDerivedType(tag: DW_TAG_member, name: "__next", scope: !51, file: !43, line: 60, baseType: !50, size: 64, offset: 128)
+!59 = !DIDerivedType(tag: DW_TAG_member, name: "__opaque", scope: !45, file: !43, line: 106, baseType: !60, size: 65408, offset: 128)
+!60 = !DICompositeType(tag: DW_TAG_array_type, baseType: !61, size: 65408, elements: !62)
+!61 = !DIBasicType(name: "char", size: 8, encoding: DW_ATE_signed_char)
+!62 = !{!63}
+!63 = !DISubrange(count: 8176)
+!64 = !DILocation(line: 18, column: 15, scope: !36)
+!65 = !DILocalVariable(name: "t2", scope: !36, file: !7, line: 18, type: !40)
+!66 = !DILocation(line: 18, column: 19, scope: !36)
+!67 = !DILocation(line: 19, column: 7, scope: !36)
+!68 = !DILocation(line: 20, column: 5, scope: !36)
+!69 = !DILocation(line: 21, column: 5, scope: !36)