diff --git a/benchmarks/nontermination/nontermination.c b/benchmarks/nontermination/nontermination.c
index 641d5b2e84..d1660c206f 100644
--- a/benchmarks/nontermination/nontermination.c
+++ b/benchmarks/nontermination/nontermination.c
@@ -1,12 +1,13 @@
 #include <pthread.h>
+#include <stdatomic.h>
 
 /*
     Test case: Oscillating memory value but the same value is constantly observed
     Expected result: FAIL under all memory models.
 */
 
-volatile int x = 0;
-volatile int y = 0;
+atomic_int x = 0;
+atomic_int y = 0;
 
 void *thread(void *unused)
 {
@@ -14,11 +15,13 @@ void *thread(void *unused)
         x = 1;
         x = 2;
     }
+    return 0;
 }
 
 void *thread2(void *unused) {
     while (x != 2) { }
     y = 1;
+    return 0;
 }
 
 int main()
diff --git a/benchmarks/nontermination/nontermination_complex.c b/benchmarks/nontermination/nontermination_complex.c
index b372e87e20..ba666e083c 100644
--- a/benchmarks/nontermination/nontermination_complex.c
+++ b/benchmarks/nontermination/nontermination_complex.c
@@ -1,4 +1,5 @@
 #include <pthread.h>
+#include <stdatomic.h>
 
 /*
     Test case: Three loops that interfere with each other..
@@ -6,9 +7,9 @@
     NOTE: Any pair of loops would terminate, only all three together fail.
 */
 
-volatile int x = 0;
-volatile int y = 0;
-volatile int z = 0;
+atomic_int x = 0;
+atomic_int y = 0;
+atomic_int z = 0;
 
 void *thread(void *unused)
 {
@@ -17,6 +18,7 @@ void *thread(void *unused)
         x = 0;
         y = 1;
     }
+    return 0;
 }
 
 void *thread2(void *unused) {
@@ -25,6 +27,7 @@ void *thread2(void *unused) {
             z = i;
         }
     }
+    return 0;
 }
 
 void *thread3(void *unused) {
@@ -32,7 +35,7 @@ void *thread3(void *unused) {
         y = 0;
         z = 0;
     }
-
+    return 0;
 }
 
 int main()
diff --git a/benchmarks/nontermination/nontermination_weak.c b/benchmarks/nontermination/nontermination_weak.c
index 11fd0a4d2e..af77a4a2c5 100644
--- a/benchmarks/nontermination/nontermination_weak.c
+++ b/benchmarks/nontermination/nontermination_weak.c
@@ -7,24 +7,26 @@
 */
 
 volatile int x = 0;
-volatile int signal = 0;
-volatile int success = 0;
+atomic_int signal = 0;
+atomic_int success = 0;
 
 void *thread(void *unused)
 {
     while(!success) {
         x = 1;
-        signal = 1;
+        atomic_store_explicit(&signal, 1, memory_order_relaxed);
     }
+    return 0;
 }
 
 void *thread2(void *unused) {
-    while (signal == 1 && x == 0) {
+    while (atomic_load_explicit(&signal, memory_order_relaxed) == 1 && x == 0) {
         // Message was wrong, reset and wait for new one.
         x = 0;
         signal = 0;
     }
     success = 1;
+    return 0;
 }
 
 int main()
diff --git a/benchmarks/nontermination/nontermination_xchg.c b/benchmarks/nontermination/nontermination_xchg.c
index 92ab55ca14..63bdba4dae 100644
--- a/benchmarks/nontermination/nontermination_xchg.c
+++ b/benchmarks/nontermination/nontermination_xchg.c
@@ -10,11 +10,13 @@ atomic_int lock;
 
 void *thread(void *unused)
 {
-    while (atomic_exchange(&lock, 1) == 1);
+    while (atomic_exchange(&lock, 1) != 0);
+    return 0;
 }
 
 void *thread2(void *unused) {
-    lock = 1;
+    atomic_exchange(&lock, 1);
+    return 0;
 }
 
 int main()
diff --git a/benchmarks/nontermination/nontermination_zero_effect.c b/benchmarks/nontermination/nontermination_zero_effect.c
index ad031adc11..1f751711e6 100644
--- a/benchmarks/nontermination/nontermination_zero_effect.c
+++ b/benchmarks/nontermination/nontermination_zero_effect.c
@@ -25,6 +25,7 @@ void *thread(void *unused)
 {
     acquireLock();
     releaseLock();
+    return 0;
 }
 
 int main()
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/NonTerminationEncoder.java b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/NonTerminationEncoder.java
index 5a3e3f4406..d38f649a94 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/NonTerminationEncoder.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/encoding/NonTerminationEncoder.java
@@ -192,16 +192,27 @@ private void computeEventToCaseInformation() {
     public BooleanFormula encodeNontermination() {
         final BooleanFormulaManager bmgr = context.getBooleanFormulaManager();
         final BooleanFormula atLeastOneStuckLoop = encodeLoopsAreStuck();
+        final BooleanFormula noExceptionalTermination = encodeNoExceptionalTermination();
         final BooleanFormula infixSuffixEquivalence = encodeInfixSuffixEquivalence();
         final BooleanFormula strongSuffixExtension = encodeStrongSuffixExtension();
 
         return bmgr.and(
+                noExceptionalTermination,
                 atLeastOneStuckLoop,
                 infixSuffixEquivalence,
                 strongSuffixExtension
         );
     }
 
+    private BooleanFormula encodeNoExceptionalTermination() {
+        final BooleanFormulaManager bmgr = context.getBooleanFormulaManager();
+        final BooleanFormula noExceptionalTermination = task.getProgram()
+                .getThreadEventsWithAllTags(Tag.EXCEPTIONAL_TERMINATION).stream()
+                .map(e -> bmgr.not(context.execution(e)))
+                .reduce(bmgr.makeTrue(), bmgr::and);
+        return noExceptionalTermination;
+    }
+
     private BooleanFormula encodeLoopsAreStuck() {
         final BooleanFormulaManager bmgr = context.getBooleanFormulaManager();
         final BooleanFormula atLeastOneNontermination = bound2Case.values().stream()
diff --git a/dartagnan/src/test/java/com/dat3m/dartagnan/c/LivenessTest.java b/dartagnan/src/test/java/com/dat3m/dartagnan/c/LivenessTest.java
index a2f6c1010c..b480c22bdf 100644
--- a/dartagnan/src/test/java/com/dat3m/dartagnan/c/LivenessTest.java
+++ b/dartagnan/src/test/java/com/dat3m/dartagnan/c/LivenessTest.java
@@ -103,13 +103,13 @@ public static Iterable<Object[]> data() throws IOException {
                 {"locks/linuxrwlock", POWER, UNKNOWN},
                 {"locks/linuxrwlock", RISCV, UNKNOWN},
                 {"locks/linuxrwlock-acq2rx", TSO, UNKNOWN},
-                {"locks/linuxrwlock-acq2rx", ARM8, FAIL},
-                {"locks/linuxrwlock-acq2rx", POWER, FAIL},
-                {"locks/linuxrwlock-acq2rx", RISCV, FAIL},
+                {"locks/linuxrwlock-acq2rx", ARM8, UNKNOWN},
+                {"locks/linuxrwlock-acq2rx", POWER, UNKNOWN},
+                {"locks/linuxrwlock-acq2rx", RISCV, UNKNOWN},
                 {"locks/linuxrwlock-rel2rx", TSO, UNKNOWN},
-                {"locks/linuxrwlock-rel2rx", ARM8, FAIL},
-                {"locks/linuxrwlock-rel2rx", POWER, FAIL},
-                {"locks/linuxrwlock-rel2rx", RISCV, FAIL},
+                {"locks/linuxrwlock-rel2rx", ARM8, UNKNOWN},
+                {"locks/linuxrwlock-rel2rx", POWER, UNKNOWN},
+                {"locks/linuxrwlock-rel2rx", RISCV, UNKNOWN},
                 {"locks/mutex_musl", TSO, UNKNOWN},
                 {"locks/mutex_musl", ARM8, UNKNOWN},
                 {"locks/mutex_musl", POWER, UNKNOWN},
diff --git a/dartagnan/src/test/resources/nontermination/nontermination.ll b/dartagnan/src/test/resources/nontermination/nontermination.ll
index 41332c74f3..161fc4af78 100644
--- a/dartagnan/src/test/resources/nontermination/nontermination.ll
+++ b/dartagnan/src/test/resources/nontermination/nontermination.ll
@@ -11,64 +11,60 @@ target triple = "arm64-apple-macosx14.0.0"
 @y = global i32 0, align 4, !dbg !7
 
 ; Function Attrs: noinline nounwind ssp uwtable
-define i8* @thread(i8* noundef %0) #0 !dbg !23 {
+define i8* @thread(i8* noundef %0) #0 !dbg !25 {
   %2 = alloca i8*, align 8
-  %3 = alloca i8*, align 8
-  store i8* %0, i8** %3, align 8
-  call void @llvm.dbg.declare(metadata i8** %3, metadata !27, metadata !DIExpression()), !dbg !28
-  br label %4, !dbg !29
-
-4:                                                ; preds = %7, %1
-  %5 = load volatile i32, i32* @y, align 4, !dbg !30
-  %6 = icmp ne i32 %5, 1, !dbg !31
-  br i1 %6, label %7, label %8, !dbg !29
-
-7:                                                ; preds = %4
-  store volatile i32 1, i32* @x, align 4, !dbg !32
-  store volatile i32 2, i32* @x, align 4, !dbg !34
-  br label %4, !dbg !29, !llvm.loop !35
-
-8:                                                ; preds = %4
-  %9 = load i8*, i8** %2, align 8, !dbg !38
-  ret i8* %9, !dbg !38
+  store i8* %0, i8** %2, align 8
+  call void @llvm.dbg.declare(metadata i8** %2, metadata !29, metadata !DIExpression()), !dbg !30
+  br label %3, !dbg !31
+
+3:                                                ; preds = %6, %1
+  %4 = load atomic i32, i32* @y seq_cst, align 4, !dbg !32
+  %5 = icmp ne i32 %4, 1, !dbg !33
+  br i1 %5, label %6, label %7, !dbg !31
+
+6:                                                ; preds = %3
+  store atomic i32 1, i32* @x seq_cst, align 4, !dbg !34
+  store atomic i32 2, i32* @x seq_cst, align 4, !dbg !36
+  br label %3, !dbg !31, !llvm.loop !37
+
+7:                                                ; preds = %3
+  ret i8* null, !dbg !40
 }
 
 ; 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* @thread2(i8* noundef %0) #0 !dbg !39 {
+define i8* @thread2(i8* noundef %0) #0 !dbg !41 {
   %2 = alloca i8*, align 8
-  %3 = alloca i8*, align 8
-  store i8* %0, i8** %3, align 8
-  call void @llvm.dbg.declare(metadata i8** %3, metadata !40, metadata !DIExpression()), !dbg !41
-  br label %4, !dbg !42
-
-4:                                                ; preds = %7, %1
-  %5 = load volatile i32, i32* @x, align 4, !dbg !43
-  %6 = icmp ne i32 %5, 2, !dbg !44
-  br i1 %6, label %7, label %8, !dbg !42
-
-7:                                                ; preds = %4
-  br label %4, !dbg !42, !llvm.loop !45
-
-8:                                                ; preds = %4
-  store volatile i32 1, i32* @y, align 4, !dbg !47
-  %9 = load i8*, i8** %2, align 8, !dbg !48
-  ret i8* %9, !dbg !48
+  store i8* %0, i8** %2, align 8
+  call void @llvm.dbg.declare(metadata i8** %2, metadata !42, metadata !DIExpression()), !dbg !43
+  br label %3, !dbg !44
+
+3:                                                ; preds = %6, %1
+  %4 = load atomic i32, i32* @x seq_cst, align 4, !dbg !45
+  %5 = icmp ne i32 %4, 2, !dbg !46
+  br i1 %5, label %6, label %7, !dbg !44
+
+6:                                                ; preds = %3
+  br label %3, !dbg !44, !llvm.loop !47
+
+7:                                                ; preds = %3
+  store atomic i32 1, i32* @y seq_cst, align 4, !dbg !49
+  ret i8* null, !dbg !50
 }
 
 ; Function Attrs: noinline nounwind ssp uwtable
-define i32 @main() #0 !dbg !49 {
+define i32 @main() #0 !dbg !51 {
   %1 = alloca i32, align 4
   %2 = alloca %struct._opaque_pthread_t*, align 8
   %3 = alloca %struct._opaque_pthread_t*, align 8
   store i32 0, i32* %1, align 4
-  call void @llvm.dbg.declare(metadata %struct._opaque_pthread_t** %2, metadata !52, metadata !DIExpression()), !dbg !77
-  call void @llvm.dbg.declare(metadata %struct._opaque_pthread_t** %3, metadata !78, metadata !DIExpression()), !dbg !79
-  %4 = call i32 @pthread_create(%struct._opaque_pthread_t** noundef %2, %struct._opaque_pthread_attr_t* noundef null, i8* (i8*)* noundef @thread, i8* noundef null), !dbg !80
-  %5 = call i32 @pthread_create(%struct._opaque_pthread_t** noundef %3, %struct._opaque_pthread_attr_t* noundef null, i8* (i8*)* noundef @thread2, i8* noundef null), !dbg !81
-  ret i32 0, !dbg !82
+  call void @llvm.dbg.declare(metadata %struct._opaque_pthread_t** %2, metadata !54, metadata !DIExpression()), !dbg !79
+  call void @llvm.dbg.declare(metadata %struct._opaque_pthread_t** %3, metadata !80, metadata !DIExpression()), !dbg !81
+  %4 = call i32 @pthread_create(%struct._opaque_pthread_t** noundef %2, %struct._opaque_pthread_attr_t* noundef null, i8* (i8*)* noundef @thread, i8* noundef null), !dbg !82
+  %5 = call i32 @pthread_create(%struct._opaque_pthread_t** noundef %3, %struct._opaque_pthread_attr_t* noundef null, i8* (i8*)* noundef @thread2, i8* noundef null), !dbg !83
+  ret i32 0, !dbg !84
 }
 
 declare i32 @pthread_create(%struct._opaque_pthread_t** noundef, %struct._opaque_pthread_attr_t* noundef, i8* (i8*)* noundef, i8* noundef) #2
@@ -78,89 +74,91 @@ 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}
+!llvm.module.flags = !{!14, !15, !16, !17, !18, !19, !20, !21, !22, !23}
+!llvm.ident = !{!24}
 
 !0 = !DIGlobalVariableExpression(var: !1, expr: !DIExpression())
-!1 = distinct !DIGlobalVariable(name: "x", scope: !2, file: !9, line: 8, type: !10, isLocal: false, isDefinition: true)
+!1 = distinct !DIGlobalVariable(name: "x", scope: !2, file: !9, line: 9, type: !10, 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/nontermination/nontermination.c", directory: "/Users/thomashaas/IdeaProjects/Dat3M")
 !4 = !{!5}
 !5 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: null, size: 64)
 !6 = !{!0, !7}
 !7 = !DIGlobalVariableExpression(var: !8, expr: !DIExpression())
-!8 = distinct !DIGlobalVariable(name: "y", scope: !2, file: !9, line: 9, type: !10, isLocal: false, isDefinition: true)
+!8 = distinct !DIGlobalVariable(name: "y", scope: !2, file: !9, line: 10, type: !10, isLocal: false, isDefinition: true)
 !9 = !DIFile(filename: "benchmarks/nontermination/nontermination.c", directory: "/Users/thomashaas/IdeaProjects/Dat3M")
-!10 = !DIDerivedType(tag: DW_TAG_volatile_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", scope: !9, file: !9, line: 11, type: !24, scopeLine: 12, 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: !9, line: 11, type: !5)
-!28 = !DILocation(line: 11, column: 20, scope: !23)
-!29 = !DILocation(line: 13, column: 5, scope: !23)
-!30 = !DILocation(line: 13, column: 11, scope: !23)
-!31 = !DILocation(line: 13, column: 13, scope: !23)
-!32 = !DILocation(line: 14, column: 11, scope: !33)
-!33 = distinct !DILexicalBlock(scope: !23, file: !9, line: 13, column: 19)
-!34 = !DILocation(line: 15, column: 11, scope: !33)
-!35 = distinct !{!35, !29, !36, !37}
-!36 = !DILocation(line: 16, column: 5, scope: !23)
-!37 = !{!"llvm.loop.mustprogress"}
-!38 = !DILocation(line: 17, column: 1, scope: !23)
-!39 = distinct !DISubprogram(name: "thread2", scope: !9, file: !9, line: 19, type: !24, scopeLine: 19, flags: DIFlagPrototyped, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !26)
-!40 = !DILocalVariable(name: "unused", arg: 1, scope: !39, file: !9, line: 19, type: !5)
-!41 = !DILocation(line: 19, column: 21, scope: !39)
-!42 = !DILocation(line: 20, column: 5, scope: !39)
-!43 = !DILocation(line: 20, column: 12, scope: !39)
-!44 = !DILocation(line: 20, column: 14, scope: !39)
-!45 = distinct !{!45, !42, !46, !37}
-!46 = !DILocation(line: 20, column: 22, scope: !39)
-!47 = !DILocation(line: 21, column: 7, scope: !39)
-!48 = !DILocation(line: 22, column: 1, scope: !39)
-!49 = distinct !DISubprogram(name: "main", scope: !9, file: !9, line: 24, type: !50, scopeLine: 25, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !26)
-!50 = !DISubroutineType(types: !51)
-!51 = !{!11}
-!52 = !DILocalVariable(name: "t1", scope: !49, file: !9, line: 26, type: !53)
-!53 = !DIDerivedType(tag: DW_TAG_typedef, name: "pthread_t", file: !54, line: 31, baseType: !55)
-!54 = !DIFile(filename: "/Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk/usr/include/sys/_pthread/_pthread_t.h", directory: "")
-!55 = !DIDerivedType(tag: DW_TAG_typedef, name: "__darwin_pthread_t", file: !56, line: 118, baseType: !57)
-!56 = !DIFile(filename: "/Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk/usr/include/sys/_pthread/_pthread_types.h", directory: "")
-!57 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: !58, size: 64)
-!58 = distinct !DICompositeType(tag: DW_TAG_structure_type, name: "_opaque_pthread_t", file: !56, line: 103, size: 65536, elements: !59)
-!59 = !{!60, !62, !72}
-!60 = !DIDerivedType(tag: DW_TAG_member, name: "__sig", scope: !58, file: !56, line: 104, baseType: !61, size: 64)
-!61 = !DIBasicType(name: "long", size: 64, encoding: DW_ATE_signed)
-!62 = !DIDerivedType(tag: DW_TAG_member, name: "__cleanup_stack", scope: !58, file: !56, line: 105, baseType: !63, size: 64, offset: 64)
-!63 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: !64, size: 64)
-!64 = distinct !DICompositeType(tag: DW_TAG_structure_type, name: "__darwin_pthread_handler_rec", file: !56, line: 57, size: 192, elements: !65)
-!65 = !{!66, !70, !71}
-!66 = !DIDerivedType(tag: DW_TAG_member, name: "__routine", scope: !64, file: !56, line: 58, baseType: !67, size: 64)
-!67 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: !68, size: 64)
-!68 = !DISubroutineType(types: !69)
-!69 = !{null, !5}
-!70 = !DIDerivedType(tag: DW_TAG_member, name: "__arg", scope: !64, file: !56, line: 59, baseType: !5, size: 64, offset: 64)
-!71 = !DIDerivedType(tag: DW_TAG_member, name: "__next", scope: !64, file: !56, line: 60, baseType: !63, size: 64, offset: 128)
-!72 = !DIDerivedType(tag: DW_TAG_member, name: "__opaque", scope: !58, file: !56, line: 106, baseType: !73, size: 65408, offset: 128)
-!73 = !DICompositeType(tag: DW_TAG_array_type, baseType: !74, size: 65408, elements: !75)
-!74 = !DIBasicType(name: "char", size: 8, encoding: DW_ATE_signed_char)
-!75 = !{!76}
-!76 = !DISubrange(count: 8176)
-!77 = !DILocation(line: 26, column: 15, scope: !49)
-!78 = !DILocalVariable(name: "t2", scope: !49, file: !9, line: 26, type: !53)
-!79 = !DILocation(line: 26, column: 19, scope: !49)
-!80 = !DILocation(line: 27, column: 5, scope: !49)
-!81 = !DILocation(line: 28, column: 5, scope: !49)
-!82 = !DILocation(line: 30, column: 5, scope: !49)
+!10 = !DIDerivedType(tag: DW_TAG_typedef, name: "atomic_int", file: !11, line: 92, baseType: !12)
+!11 = !DIFile(filename: "/opt/homebrew/Cellar/llvm@14/14.0.6/lib/clang/14.0.6/include/stdatomic.h", directory: "")
+!12 = !DIDerivedType(tag: DW_TAG_atomic_type, baseType: !13)
+!13 = !DIBasicType(name: "int", size: 32, encoding: DW_ATE_signed)
+!14 = !{i32 7, !"Dwarf Version", i32 4}
+!15 = !{i32 2, !"Debug Info Version", i32 3}
+!16 = !{i32 1, !"wchar_size", i32 4}
+!17 = !{i32 1, !"branch-target-enforcement", i32 0}
+!18 = !{i32 1, !"sign-return-address", i32 0}
+!19 = !{i32 1, !"sign-return-address-all", i32 0}
+!20 = !{i32 1, !"sign-return-address-with-bkey", i32 0}
+!21 = !{i32 7, !"PIC Level", i32 2}
+!22 = !{i32 7, !"uwtable", i32 1}
+!23 = !{i32 7, !"frame-pointer", i32 1}
+!24 = !{!"Homebrew clang version 14.0.6"}
+!25 = distinct !DISubprogram(name: "thread", scope: !9, file: !9, line: 12, type: !26, scopeLine: 13, flags: DIFlagPrototyped, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !28)
+!26 = !DISubroutineType(types: !27)
+!27 = !{!5, !5}
+!28 = !{}
+!29 = !DILocalVariable(name: "unused", arg: 1, scope: !25, file: !9, line: 12, type: !5)
+!30 = !DILocation(line: 12, column: 20, scope: !25)
+!31 = !DILocation(line: 14, column: 5, scope: !25)
+!32 = !DILocation(line: 14, column: 11, scope: !25)
+!33 = !DILocation(line: 14, column: 13, scope: !25)
+!34 = !DILocation(line: 15, column: 11, scope: !35)
+!35 = distinct !DILexicalBlock(scope: !25, file: !9, line: 14, column: 19)
+!36 = !DILocation(line: 16, column: 11, scope: !35)
+!37 = distinct !{!37, !31, !38, !39}
+!38 = !DILocation(line: 17, column: 5, scope: !25)
+!39 = !{!"llvm.loop.mustprogress"}
+!40 = !DILocation(line: 18, column: 5, scope: !25)
+!41 = distinct !DISubprogram(name: "thread2", scope: !9, file: !9, line: 21, type: !26, scopeLine: 21, flags: DIFlagPrototyped, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !28)
+!42 = !DILocalVariable(name: "unused", arg: 1, scope: !41, file: !9, line: 21, type: !5)
+!43 = !DILocation(line: 21, column: 21, scope: !41)
+!44 = !DILocation(line: 22, column: 5, scope: !41)
+!45 = !DILocation(line: 22, column: 12, scope: !41)
+!46 = !DILocation(line: 22, column: 14, scope: !41)
+!47 = distinct !{!47, !44, !48, !39}
+!48 = !DILocation(line: 22, column: 22, scope: !41)
+!49 = !DILocation(line: 23, column: 7, scope: !41)
+!50 = !DILocation(line: 24, column: 5, scope: !41)
+!51 = distinct !DISubprogram(name: "main", scope: !9, file: !9, line: 27, type: !52, scopeLine: 28, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !28)
+!52 = !DISubroutineType(types: !53)
+!53 = !{!13}
+!54 = !DILocalVariable(name: "t1", scope: !51, file: !9, line: 29, type: !55)
+!55 = !DIDerivedType(tag: DW_TAG_typedef, name: "pthread_t", file: !56, line: 31, baseType: !57)
+!56 = !DIFile(filename: "/Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk/usr/include/sys/_pthread/_pthread_t.h", directory: "")
+!57 = !DIDerivedType(tag: DW_TAG_typedef, name: "__darwin_pthread_t", file: !58, line: 118, baseType: !59)
+!58 = !DIFile(filename: "/Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk/usr/include/sys/_pthread/_pthread_types.h", directory: "")
+!59 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: !60, size: 64)
+!60 = distinct !DICompositeType(tag: DW_TAG_structure_type, name: "_opaque_pthread_t", file: !58, line: 103, size: 65536, elements: !61)
+!61 = !{!62, !64, !74}
+!62 = !DIDerivedType(tag: DW_TAG_member, name: "__sig", scope: !60, file: !58, line: 104, baseType: !63, size: 64)
+!63 = !DIBasicType(name: "long", size: 64, encoding: DW_ATE_signed)
+!64 = !DIDerivedType(tag: DW_TAG_member, name: "__cleanup_stack", scope: !60, file: !58, line: 105, baseType: !65, size: 64, offset: 64)
+!65 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: !66, size: 64)
+!66 = distinct !DICompositeType(tag: DW_TAG_structure_type, name: "__darwin_pthread_handler_rec", file: !58, line: 57, size: 192, elements: !67)
+!67 = !{!68, !72, !73}
+!68 = !DIDerivedType(tag: DW_TAG_member, name: "__routine", scope: !66, file: !58, line: 58, baseType: !69, size: 64)
+!69 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: !70, size: 64)
+!70 = !DISubroutineType(types: !71)
+!71 = !{null, !5}
+!72 = !DIDerivedType(tag: DW_TAG_member, name: "__arg", scope: !66, file: !58, line: 59, baseType: !5, size: 64, offset: 64)
+!73 = !DIDerivedType(tag: DW_TAG_member, name: "__next", scope: !66, file: !58, line: 60, baseType: !65, size: 64, offset: 128)
+!74 = !DIDerivedType(tag: DW_TAG_member, name: "__opaque", scope: !60, file: !58, line: 106, baseType: !75, size: 65408, offset: 128)
+!75 = !DICompositeType(tag: DW_TAG_array_type, baseType: !76, size: 65408, elements: !77)
+!76 = !DIBasicType(name: "char", size: 8, encoding: DW_ATE_signed_char)
+!77 = !{!78}
+!78 = !DISubrange(count: 8176)
+!79 = !DILocation(line: 29, column: 15, scope: !51)
+!80 = !DILocalVariable(name: "t2", scope: !51, file: !9, line: 29, type: !55)
+!81 = !DILocation(line: 29, column: 19, scope: !51)
+!82 = !DILocation(line: 30, column: 5, scope: !51)
+!83 = !DILocation(line: 31, column: 5, scope: !51)
+!84 = !DILocation(line: 33, column: 5, scope: !51)
diff --git a/dartagnan/src/test/resources/nontermination/nontermination_complex.ll b/dartagnan/src/test/resources/nontermination/nontermination_complex.ll
index a4fd072c4b..5df083b9d4 100644
--- a/dartagnan/src/test/resources/nontermination/nontermination_complex.ll
+++ b/dartagnan/src/test/resources/nontermination/nontermination_complex.ll
@@ -9,129 +9,123 @@ target triple = "arm64-apple-macosx14.0.0"
 
 @x = global i32 0, align 4, !dbg !0
 @y = global i32 0, align 4, !dbg !7
-@z = global i32 0, align 4, !dbg !12
+@z = global i32 0, align 4, !dbg !14
 
 ; Function Attrs: noinline nounwind ssp uwtable
-define i8* @thread(i8* noundef %0) #0 !dbg !25 {
+define i8* @thread(i8* noundef %0) #0 !dbg !27 {
   %2 = alloca i8*, align 8
-  %3 = alloca i8*, align 8
-  store i8* %0, i8** %3, align 8
-  call void @llvm.dbg.declare(metadata i8** %3, metadata !29, metadata !DIExpression()), !dbg !30
-  br label %4, !dbg !31
+  store i8* %0, i8** %2, align 8
+  call void @llvm.dbg.declare(metadata i8** %2, metadata !31, metadata !DIExpression()), !dbg !32
+  br label %3, !dbg !33
 
-4:                                                ; preds = %7, %1
-  %5 = load volatile i32, i32* @y, align 4, !dbg !32
-  %6 = icmp ne i32 %5, 1, !dbg !33
-  br i1 %6, label %7, label %8, !dbg !31
+3:                                                ; preds = %6, %1
+  %4 = load atomic i32, i32* @y seq_cst, align 4, !dbg !34
+  %5 = icmp ne i32 %4, 1, !dbg !35
+  br i1 %5, label %6, label %7, !dbg !33
 
-7:                                                ; preds = %4
-  store volatile i32 1, i32* @x, align 4, !dbg !34
-  store volatile i32 0, i32* @x, align 4, !dbg !36
-  store volatile i32 1, i32* @y, align 4, !dbg !37
-  br label %4, !dbg !31, !llvm.loop !38
+6:                                                ; preds = %3
+  store atomic i32 1, i32* @x seq_cst, align 4, !dbg !36
+  store atomic i32 0, i32* @x seq_cst, align 4, !dbg !38
+  store atomic i32 1, i32* @y seq_cst, align 4, !dbg !39
+  br label %3, !dbg !33, !llvm.loop !40
 
-8:                                                ; preds = %4
-  %9 = load i8*, i8** %2, align 8, !dbg !41
-  ret i8* %9, !dbg !41
+7:                                                ; preds = %3
+  ret i8* null, !dbg !43
 }
 
 ; 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* @thread2(i8* noundef %0) #0 !dbg !42 {
+define i8* @thread2(i8* noundef %0) #0 !dbg !44 {
   %2 = alloca i8*, align 8
-  %3 = alloca i8*, align 8
-  %4 = alloca i32, align 4
-  store i8* %0, i8** %3, align 8
-  call void @llvm.dbg.declare(metadata i8** %3, metadata !43, metadata !DIExpression()), !dbg !44
-  br label %5, !dbg !45
+  %3 = alloca i32, align 4
+  store i8* %0, i8** %2, align 8
+  call void @llvm.dbg.declare(metadata i8** %2, metadata !45, metadata !DIExpression()), !dbg !46
+  br label %4, !dbg !47
 
-5:                                                ; preds = %25, %1
-  %6 = load volatile i32, i32* @x, align 4, !dbg !46
-  %7 = icmp eq i32 %6, 1, !dbg !47
-  br i1 %7, label %8, label %14, !dbg !48
+4:                                                ; preds = %24, %1
+  %5 = load atomic i32, i32* @x seq_cst, align 4, !dbg !48
+  %6 = icmp eq i32 %5, 1, !dbg !49
+  br i1 %6, label %7, label %13, !dbg !50
 
-8:                                                ; preds = %5
-  %9 = load volatile i32, i32* @y, align 4, !dbg !49
-  %10 = icmp ne i32 %9, 0, !dbg !50
-  br i1 %10, label %11, label %14, !dbg !51
+7:                                                ; preds = %4
+  %8 = load atomic i32, i32* @y seq_cst, align 4, !dbg !51
+  %9 = icmp ne i32 %8, 0, !dbg !52
+  br i1 %9, label %10, label %13, !dbg !53
 
-11:                                               ; preds = %8
-  %12 = load volatile i32, i32* @z, align 4, !dbg !52
-  %13 = icmp ne i32 %12, 3, !dbg !53
-  br label %14
+10:                                               ; preds = %7
+  %11 = load atomic i32, i32* @z seq_cst, align 4, !dbg !54
+  %12 = icmp ne i32 %11, 3, !dbg !55
+  br label %13
 
-14:                                               ; preds = %11, %8, %5
-  %15 = phi i1 [ false, %8 ], [ false, %5 ], [ %13, %11 ], !dbg !54
-  br i1 %15, label %16, label %26, !dbg !45
+13:                                               ; preds = %10, %7, %4
+  %14 = phi i1 [ false, %7 ], [ false, %4 ], [ %12, %10 ], !dbg !56
+  br i1 %14, label %15, label %25, !dbg !47
 
-16:                                               ; preds = %14
-  call void @llvm.dbg.declare(metadata i32* %4, metadata !55, metadata !DIExpression()), !dbg !58
-  store i32 0, i32* %4, align 4, !dbg !58
-  br label %17, !dbg !59
+15:                                               ; preds = %13
+  call void @llvm.dbg.declare(metadata i32* %3, metadata !57, metadata !DIExpression()), !dbg !60
+  store i32 0, i32* %3, align 4, !dbg !60
+  br label %16, !dbg !61
 
-17:                                               ; preds = %22, %16
-  %18 = load i32, i32* %4, align 4, !dbg !60
-  %19 = icmp slt i32 %18, 4, !dbg !62
-  br i1 %19, label %20, label %25, !dbg !63
+16:                                               ; preds = %21, %15
+  %17 = load i32, i32* %3, align 4, !dbg !62
+  %18 = icmp slt i32 %17, 4, !dbg !64
+  br i1 %18, label %19, label %24, !dbg !65
 
-20:                                               ; preds = %17
-  %21 = load i32, i32* %4, align 4, !dbg !64
-  store volatile i32 %21, i32* @z, align 4, !dbg !66
-  br label %22, !dbg !67
+19:                                               ; preds = %16
+  %20 = load i32, i32* %3, align 4, !dbg !66
+  store atomic i32 %20, i32* @z seq_cst, align 4, !dbg !68
+  br label %21, !dbg !69
 
-22:                                               ; preds = %20
-  %23 = load i32, i32* %4, align 4, !dbg !68
-  %24 = add nsw i32 %23, 1, !dbg !68
-  store i32 %24, i32* %4, align 4, !dbg !68
-  br label %17, !dbg !69, !llvm.loop !70
+21:                                               ; preds = %19
+  %22 = load i32, i32* %3, align 4, !dbg !70
+  %23 = add nsw i32 %22, 1, !dbg !70
+  store i32 %23, i32* %3, align 4, !dbg !70
+  br label %16, !dbg !71, !llvm.loop !72
 
-25:                                               ; preds = %17
-  br label %5, !dbg !45, !llvm.loop !72
+24:                                               ; preds = %16
+  br label %4, !dbg !47, !llvm.loop !74
 
-26:                                               ; preds = %14
-  %27 = load i8*, i8** %2, align 8, !dbg !74
-  ret i8* %27, !dbg !74
+25:                                               ; preds = %13
+  ret i8* null, !dbg !76
 }
 
 ; Function Attrs: noinline nounwind ssp uwtable
-define i8* @thread3(i8* noundef %0) #0 !dbg !75 {
+define i8* @thread3(i8* noundef %0) #0 !dbg !77 {
   %2 = alloca i8*, align 8
-  %3 = alloca i8*, align 8
-  store i8* %0, i8** %3, align 8
-  call void @llvm.dbg.declare(metadata i8** %3, metadata !76, metadata !DIExpression()), !dbg !77
-  br label %4, !dbg !78
+  store i8* %0, i8** %2, align 8
+  call void @llvm.dbg.declare(metadata i8** %2, metadata !78, metadata !DIExpression()), !dbg !79
+  br label %3, !dbg !80
 
-4:                                                ; preds = %7, %1
-  %5 = load volatile i32, i32* @z, align 4, !dbg !79
-  %6 = icmp eq i32 %5, 1, !dbg !80
-  br i1 %6, label %7, label %8, !dbg !78
+3:                                                ; preds = %6, %1
+  %4 = load atomic i32, i32* @z seq_cst, align 4, !dbg !81
+  %5 = icmp eq i32 %4, 1, !dbg !82
+  br i1 %5, label %6, label %7, !dbg !80
 
-7:                                                ; preds = %4
-  store volatile i32 0, i32* @y, align 4, !dbg !81
-  store volatile i32 0, i32* @z, align 4, !dbg !83
-  br label %4, !dbg !78, !llvm.loop !84
+6:                                                ; preds = %3
+  store atomic i32 0, i32* @y seq_cst, align 4, !dbg !83
+  store atomic i32 0, i32* @z seq_cst, align 4, !dbg !85
+  br label %3, !dbg !80, !llvm.loop !86
 
-8:                                                ; preds = %4
-  %9 = load i8*, i8** %2, align 8, !dbg !86
-  ret i8* %9, !dbg !86
+7:                                                ; preds = %3
+  ret i8* null, !dbg !88
 }
 
 ; Function Attrs: noinline nounwind ssp uwtable
-define i32 @main() #0 !dbg !87 {
+define i32 @main() #0 !dbg !89 {
   %1 = alloca i32, align 4
   %2 = alloca %struct._opaque_pthread_t*, align 8
   %3 = alloca %struct._opaque_pthread_t*, align 8
   %4 = alloca %struct._opaque_pthread_t*, align 8
   store i32 0, i32* %1, align 4
-  call void @llvm.dbg.declare(metadata %struct._opaque_pthread_t** %2, metadata !90, metadata !DIExpression()), !dbg !115
-  call void @llvm.dbg.declare(metadata %struct._opaque_pthread_t** %3, metadata !116, metadata !DIExpression()), !dbg !117
-  call void @llvm.dbg.declare(metadata %struct._opaque_pthread_t** %4, metadata !118, metadata !DIExpression()), !dbg !119
-  %5 = call i32 @pthread_create(%struct._opaque_pthread_t** noundef %2, %struct._opaque_pthread_attr_t* noundef null, i8* (i8*)* noundef @thread, i8* noundef null), !dbg !120
-  %6 = call i32 @pthread_create(%struct._opaque_pthread_t** noundef %3, %struct._opaque_pthread_attr_t* noundef null, i8* (i8*)* noundef @thread2, i8* noundef null), !dbg !121
-  %7 = call i32 @pthread_create(%struct._opaque_pthread_t** noundef %4, %struct._opaque_pthread_attr_t* noundef null, i8* (i8*)* noundef @thread3, i8* noundef null), !dbg !122
-  ret i32 0, !dbg !123
+  call void @llvm.dbg.declare(metadata %struct._opaque_pthread_t** %2, metadata !92, metadata !DIExpression()), !dbg !117
+  call void @llvm.dbg.declare(metadata %struct._opaque_pthread_t** %3, metadata !118, metadata !DIExpression()), !dbg !119
+  call void @llvm.dbg.declare(metadata %struct._opaque_pthread_t** %4, metadata !120, metadata !DIExpression()), !dbg !121
+  %5 = call i32 @pthread_create(%struct._opaque_pthread_t** noundef %2, %struct._opaque_pthread_attr_t* noundef null, i8* (i8*)* noundef @thread, i8* noundef null), !dbg !122
+  %6 = call i32 @pthread_create(%struct._opaque_pthread_t** noundef %3, %struct._opaque_pthread_attr_t* noundef null, i8* (i8*)* noundef @thread2, i8* noundef null), !dbg !123
+  %7 = call i32 @pthread_create(%struct._opaque_pthread_t** noundef %4, %struct._opaque_pthread_attr_t* noundef null, i8* (i8*)* noundef @thread3, i8* noundef null), !dbg !124
+  ret i32 0, !dbg !125
 }
 
 declare i32 @pthread_create(%struct._opaque_pthread_t** noundef, %struct._opaque_pthread_attr_t* noundef, i8* (i8*)* noundef, i8* noundef) #2
@@ -141,130 +135,132 @@ 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 = !{!14, !15, !16, !17, !18, !19, !20, !21, !22, !23}
-!llvm.ident = !{!24}
+!llvm.module.flags = !{!16, !17, !18, !19, !20, !21, !22, !23, !24, !25}
+!llvm.ident = !{!26}
 
 !0 = !DIGlobalVariableExpression(var: !1, expr: !DIExpression())
-!1 = distinct !DIGlobalVariable(name: "x", scope: !2, file: !9, line: 9, type: !10, isLocal: false, isDefinition: true)
+!1 = distinct !DIGlobalVariable(name: "x", scope: !2, file: !9, line: 10, type: !10, 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/nontermination/nontermination_complex.c", directory: "/Users/thomashaas/IdeaProjects/Dat3M")
 !4 = !{!5}
 !5 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: null, size: 64)
-!6 = !{!0, !7, !12}
+!6 = !{!0, !7, !14}
 !7 = !DIGlobalVariableExpression(var: !8, expr: !DIExpression())
-!8 = distinct !DIGlobalVariable(name: "y", scope: !2, file: !9, line: 10, type: !10, isLocal: false, isDefinition: true)
+!8 = distinct !DIGlobalVariable(name: "y", scope: !2, file: !9, line: 11, type: !10, isLocal: false, isDefinition: true)
 !9 = !DIFile(filename: "benchmarks/nontermination/nontermination_complex.c", directory: "/Users/thomashaas/IdeaProjects/Dat3M")
-!10 = !DIDerivedType(tag: DW_TAG_volatile_type, baseType: !11)
-!11 = !DIBasicType(name: "int", size: 32, encoding: DW_ATE_signed)
-!12 = !DIGlobalVariableExpression(var: !13, expr: !DIExpression())
-!13 = distinct !DIGlobalVariable(name: "z", scope: !2, file: !9, line: 11, type: !10, isLocal: false, isDefinition: true)
-!14 = !{i32 7, !"Dwarf Version", i32 4}
-!15 = !{i32 2, !"Debug Info Version", i32 3}
-!16 = !{i32 1, !"wchar_size", i32 4}
-!17 = !{i32 1, !"branch-target-enforcement", i32 0}
-!18 = !{i32 1, !"sign-return-address", i32 0}
-!19 = !{i32 1, !"sign-return-address-all", i32 0}
-!20 = !{i32 1, !"sign-return-address-with-bkey", i32 0}
-!21 = !{i32 7, !"PIC Level", i32 2}
-!22 = !{i32 7, !"uwtable", i32 1}
-!23 = !{i32 7, !"frame-pointer", i32 1}
-!24 = !{!"Homebrew clang version 14.0.6"}
-!25 = distinct !DISubprogram(name: "thread", scope: !9, file: !9, line: 13, type: !26, scopeLine: 14, flags: DIFlagPrototyped, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !28)
-!26 = !DISubroutineType(types: !27)
-!27 = !{!5, !5}
-!28 = !{}
-!29 = !DILocalVariable(name: "unused", arg: 1, scope: !25, file: !9, line: 13, type: !5)
-!30 = !DILocation(line: 13, column: 20, scope: !25)
-!31 = !DILocation(line: 15, column: 5, scope: !25)
-!32 = !DILocation(line: 15, column: 11, scope: !25)
-!33 = !DILocation(line: 15, column: 13, scope: !25)
-!34 = !DILocation(line: 16, column: 11, scope: !35)
-!35 = distinct !DILexicalBlock(scope: !25, file: !9, line: 15, column: 19)
-!36 = !DILocation(line: 17, column: 11, scope: !35)
-!37 = !DILocation(line: 18, column: 11, scope: !35)
-!38 = distinct !{!38, !31, !39, !40}
-!39 = !DILocation(line: 19, column: 5, scope: !25)
-!40 = !{!"llvm.loop.mustprogress"}
-!41 = !DILocation(line: 20, column: 1, scope: !25)
-!42 = distinct !DISubprogram(name: "thread2", scope: !9, file: !9, line: 22, type: !26, scopeLine: 22, flags: DIFlagPrototyped, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !28)
-!43 = !DILocalVariable(name: "unused", arg: 1, scope: !42, file: !9, line: 22, type: !5)
-!44 = !DILocation(line: 22, column: 21, scope: !42)
-!45 = !DILocation(line: 23, column: 5, scope: !42)
-!46 = !DILocation(line: 23, column: 12, scope: !42)
-!47 = !DILocation(line: 23, column: 14, scope: !42)
-!48 = !DILocation(line: 23, column: 19, scope: !42)
-!49 = !DILocation(line: 23, column: 22, scope: !42)
-!50 = !DILocation(line: 23, column: 24, scope: !42)
-!51 = !DILocation(line: 23, column: 29, scope: !42)
-!52 = !DILocation(line: 23, column: 32, scope: !42)
-!53 = !DILocation(line: 23, column: 34, scope: !42)
-!54 = !DILocation(line: 0, scope: !42)
-!55 = !DILocalVariable(name: "i", scope: !56, file: !9, line: 24, type: !11)
-!56 = distinct !DILexicalBlock(scope: !57, file: !9, line: 24, column: 9)
-!57 = distinct !DILexicalBlock(scope: !42, file: !9, line: 23, column: 40)
-!58 = !DILocation(line: 24, column: 18, scope: !56)
-!59 = !DILocation(line: 24, column: 14, scope: !56)
-!60 = !DILocation(line: 24, column: 25, scope: !61)
-!61 = distinct !DILexicalBlock(scope: !56, file: !9, line: 24, column: 9)
-!62 = !DILocation(line: 24, column: 27, scope: !61)
-!63 = !DILocation(line: 24, column: 9, scope: !56)
-!64 = !DILocation(line: 25, column: 17, scope: !65)
-!65 = distinct !DILexicalBlock(scope: !61, file: !9, line: 24, column: 37)
-!66 = !DILocation(line: 25, column: 15, scope: !65)
-!67 = !DILocation(line: 26, column: 9, scope: !65)
-!68 = !DILocation(line: 24, column: 33, scope: !61)
-!69 = !DILocation(line: 24, column: 9, scope: !61)
-!70 = distinct !{!70, !63, !71, !40}
-!71 = !DILocation(line: 26, column: 9, scope: !56)
-!72 = distinct !{!72, !45, !73, !40}
-!73 = !DILocation(line: 27, column: 5, scope: !42)
-!74 = !DILocation(line: 28, column: 1, scope: !42)
-!75 = distinct !DISubprogram(name: "thread3", scope: !9, file: !9, line: 30, type: !26, scopeLine: 30, flags: DIFlagPrototyped, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !28)
-!76 = !DILocalVariable(name: "unused", arg: 1, scope: !75, file: !9, line: 30, type: !5)
-!77 = !DILocation(line: 30, column: 21, scope: !75)
-!78 = !DILocation(line: 31, column: 5, scope: !75)
-!79 = !DILocation(line: 31, column: 12, scope: !75)
-!80 = !DILocation(line: 31, column: 14, scope: !75)
-!81 = !DILocation(line: 32, column: 11, scope: !82)
-!82 = distinct !DILexicalBlock(scope: !75, file: !9, line: 31, column: 20)
-!83 = !DILocation(line: 33, column: 11, scope: !82)
-!84 = distinct !{!84, !78, !85, !40}
-!85 = !DILocation(line: 34, column: 5, scope: !75)
-!86 = !DILocation(line: 36, column: 1, scope: !75)
-!87 = distinct !DISubprogram(name: "main", scope: !9, file: !9, line: 38, type: !88, scopeLine: 39, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !28)
-!88 = !DISubroutineType(types: !89)
-!89 = !{!11}
-!90 = !DILocalVariable(name: "t1", scope: !87, file: !9, line: 40, type: !91)
-!91 = !DIDerivedType(tag: DW_TAG_typedef, name: "pthread_t", file: !92, line: 31, baseType: !93)
-!92 = !DIFile(filename: "/Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk/usr/include/sys/_pthread/_pthread_t.h", directory: "")
-!93 = !DIDerivedType(tag: DW_TAG_typedef, name: "__darwin_pthread_t", file: !94, line: 118, baseType: !95)
-!94 = !DIFile(filename: "/Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk/usr/include/sys/_pthread/_pthread_types.h", directory: "")
-!95 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: !96, size: 64)
-!96 = distinct !DICompositeType(tag: DW_TAG_structure_type, name: "_opaque_pthread_t", file: !94, line: 103, size: 65536, elements: !97)
-!97 = !{!98, !100, !110}
-!98 = !DIDerivedType(tag: DW_TAG_member, name: "__sig", scope: !96, file: !94, line: 104, baseType: !99, size: 64)
-!99 = !DIBasicType(name: "long", size: 64, encoding: DW_ATE_signed)
-!100 = !DIDerivedType(tag: DW_TAG_member, name: "__cleanup_stack", scope: !96, file: !94, line: 105, baseType: !101, size: 64, offset: 64)
-!101 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: !102, size: 64)
-!102 = distinct !DICompositeType(tag: DW_TAG_structure_type, name: "__darwin_pthread_handler_rec", file: !94, line: 57, size: 192, elements: !103)
-!103 = !{!104, !108, !109}
-!104 = !DIDerivedType(tag: DW_TAG_member, name: "__routine", scope: !102, file: !94, line: 58, baseType: !105, size: 64)
-!105 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: !106, size: 64)
-!106 = !DISubroutineType(types: !107)
-!107 = !{null, !5}
-!108 = !DIDerivedType(tag: DW_TAG_member, name: "__arg", scope: !102, file: !94, line: 59, baseType: !5, size: 64, offset: 64)
-!109 = !DIDerivedType(tag: DW_TAG_member, name: "__next", scope: !102, file: !94, line: 60, baseType: !101, size: 64, offset: 128)
-!110 = !DIDerivedType(tag: DW_TAG_member, name: "__opaque", scope: !96, file: !94, line: 106, baseType: !111, size: 65408, offset: 128)
-!111 = !DICompositeType(tag: DW_TAG_array_type, baseType: !112, size: 65408, elements: !113)
-!112 = !DIBasicType(name: "char", size: 8, encoding: DW_ATE_signed_char)
-!113 = !{!114}
-!114 = !DISubrange(count: 8176)
-!115 = !DILocation(line: 40, column: 15, scope: !87)
-!116 = !DILocalVariable(name: "t2", scope: !87, file: !9, line: 40, type: !91)
-!117 = !DILocation(line: 40, column: 19, scope: !87)
-!118 = !DILocalVariable(name: "t3", scope: !87, file: !9, line: 40, type: !91)
-!119 = !DILocation(line: 40, column: 23, scope: !87)
-!120 = !DILocation(line: 41, column: 5, scope: !87)
-!121 = !DILocation(line: 42, column: 5, scope: !87)
-!122 = !DILocation(line: 43, column: 5, scope: !87)
-!123 = !DILocation(line: 45, column: 5, scope: !87)
+!10 = !DIDerivedType(tag: DW_TAG_typedef, name: "atomic_int", file: !11, line: 92, baseType: !12)
+!11 = !DIFile(filename: "/opt/homebrew/Cellar/llvm@14/14.0.6/lib/clang/14.0.6/include/stdatomic.h", directory: "")
+!12 = !DIDerivedType(tag: DW_TAG_atomic_type, baseType: !13)
+!13 = !DIBasicType(name: "int", size: 32, encoding: DW_ATE_signed)
+!14 = !DIGlobalVariableExpression(var: !15, expr: !DIExpression())
+!15 = distinct !DIGlobalVariable(name: "z", scope: !2, file: !9, line: 12, type: !10, isLocal: false, isDefinition: true)
+!16 = !{i32 7, !"Dwarf Version", i32 4}
+!17 = !{i32 2, !"Debug Info Version", i32 3}
+!18 = !{i32 1, !"wchar_size", i32 4}
+!19 = !{i32 1, !"branch-target-enforcement", i32 0}
+!20 = !{i32 1, !"sign-return-address", i32 0}
+!21 = !{i32 1, !"sign-return-address-all", i32 0}
+!22 = !{i32 1, !"sign-return-address-with-bkey", i32 0}
+!23 = !{i32 7, !"PIC Level", i32 2}
+!24 = !{i32 7, !"uwtable", i32 1}
+!25 = !{i32 7, !"frame-pointer", i32 1}
+!26 = !{!"Homebrew clang version 14.0.6"}
+!27 = distinct !DISubprogram(name: "thread", scope: !9, file: !9, line: 14, type: !28, scopeLine: 15, flags: DIFlagPrototyped, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !30)
+!28 = !DISubroutineType(types: !29)
+!29 = !{!5, !5}
+!30 = !{}
+!31 = !DILocalVariable(name: "unused", arg: 1, scope: !27, file: !9, line: 14, type: !5)
+!32 = !DILocation(line: 14, column: 20, scope: !27)
+!33 = !DILocation(line: 16, column: 5, scope: !27)
+!34 = !DILocation(line: 16, column: 11, scope: !27)
+!35 = !DILocation(line: 16, column: 13, scope: !27)
+!36 = !DILocation(line: 17, column: 11, scope: !37)
+!37 = distinct !DILexicalBlock(scope: !27, file: !9, line: 16, column: 19)
+!38 = !DILocation(line: 18, column: 11, scope: !37)
+!39 = !DILocation(line: 19, column: 11, scope: !37)
+!40 = distinct !{!40, !33, !41, !42}
+!41 = !DILocation(line: 20, column: 5, scope: !27)
+!42 = !{!"llvm.loop.mustprogress"}
+!43 = !DILocation(line: 21, column: 5, scope: !27)
+!44 = distinct !DISubprogram(name: "thread2", scope: !9, file: !9, line: 24, type: !28, scopeLine: 24, flags: DIFlagPrototyped, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !30)
+!45 = !DILocalVariable(name: "unused", arg: 1, scope: !44, file: !9, line: 24, type: !5)
+!46 = !DILocation(line: 24, column: 21, scope: !44)
+!47 = !DILocation(line: 25, column: 5, scope: !44)
+!48 = !DILocation(line: 25, column: 12, scope: !44)
+!49 = !DILocation(line: 25, column: 14, scope: !44)
+!50 = !DILocation(line: 25, column: 19, scope: !44)
+!51 = !DILocation(line: 25, column: 22, scope: !44)
+!52 = !DILocation(line: 25, column: 24, scope: !44)
+!53 = !DILocation(line: 25, column: 29, scope: !44)
+!54 = !DILocation(line: 25, column: 32, scope: !44)
+!55 = !DILocation(line: 25, column: 34, scope: !44)
+!56 = !DILocation(line: 0, scope: !44)
+!57 = !DILocalVariable(name: "i", scope: !58, file: !9, line: 26, type: !13)
+!58 = distinct !DILexicalBlock(scope: !59, file: !9, line: 26, column: 9)
+!59 = distinct !DILexicalBlock(scope: !44, file: !9, line: 25, column: 40)
+!60 = !DILocation(line: 26, column: 18, scope: !58)
+!61 = !DILocation(line: 26, column: 14, scope: !58)
+!62 = !DILocation(line: 26, column: 25, scope: !63)
+!63 = distinct !DILexicalBlock(scope: !58, file: !9, line: 26, column: 9)
+!64 = !DILocation(line: 26, column: 27, scope: !63)
+!65 = !DILocation(line: 26, column: 9, scope: !58)
+!66 = !DILocation(line: 27, column: 17, scope: !67)
+!67 = distinct !DILexicalBlock(scope: !63, file: !9, line: 26, column: 37)
+!68 = !DILocation(line: 27, column: 15, scope: !67)
+!69 = !DILocation(line: 28, column: 9, scope: !67)
+!70 = !DILocation(line: 26, column: 33, scope: !63)
+!71 = !DILocation(line: 26, column: 9, scope: !63)
+!72 = distinct !{!72, !65, !73, !42}
+!73 = !DILocation(line: 28, column: 9, scope: !58)
+!74 = distinct !{!74, !47, !75, !42}
+!75 = !DILocation(line: 29, column: 5, scope: !44)
+!76 = !DILocation(line: 30, column: 5, scope: !44)
+!77 = distinct !DISubprogram(name: "thread3", scope: !9, file: !9, line: 33, type: !28, scopeLine: 33, flags: DIFlagPrototyped, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !30)
+!78 = !DILocalVariable(name: "unused", arg: 1, scope: !77, file: !9, line: 33, type: !5)
+!79 = !DILocation(line: 33, column: 21, scope: !77)
+!80 = !DILocation(line: 34, column: 5, scope: !77)
+!81 = !DILocation(line: 34, column: 12, scope: !77)
+!82 = !DILocation(line: 34, column: 14, scope: !77)
+!83 = !DILocation(line: 35, column: 11, scope: !84)
+!84 = distinct !DILexicalBlock(scope: !77, file: !9, line: 34, column: 20)
+!85 = !DILocation(line: 36, column: 11, scope: !84)
+!86 = distinct !{!86, !80, !87, !42}
+!87 = !DILocation(line: 37, column: 5, scope: !77)
+!88 = !DILocation(line: 38, column: 5, scope: !77)
+!89 = distinct !DISubprogram(name: "main", scope: !9, file: !9, line: 41, type: !90, scopeLine: 42, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !30)
+!90 = !DISubroutineType(types: !91)
+!91 = !{!13}
+!92 = !DILocalVariable(name: "t1", scope: !89, file: !9, line: 43, type: !93)
+!93 = !DIDerivedType(tag: DW_TAG_typedef, name: "pthread_t", file: !94, line: 31, baseType: !95)
+!94 = !DIFile(filename: "/Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk/usr/include/sys/_pthread/_pthread_t.h", directory: "")
+!95 = !DIDerivedType(tag: DW_TAG_typedef, name: "__darwin_pthread_t", file: !96, line: 118, baseType: !97)
+!96 = !DIFile(filename: "/Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk/usr/include/sys/_pthread/_pthread_types.h", directory: "")
+!97 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: !98, size: 64)
+!98 = distinct !DICompositeType(tag: DW_TAG_structure_type, name: "_opaque_pthread_t", file: !96, line: 103, size: 65536, elements: !99)
+!99 = !{!100, !102, !112}
+!100 = !DIDerivedType(tag: DW_TAG_member, name: "__sig", scope: !98, file: !96, line: 104, baseType: !101, size: 64)
+!101 = !DIBasicType(name: "long", size: 64, encoding: DW_ATE_signed)
+!102 = !DIDerivedType(tag: DW_TAG_member, name: "__cleanup_stack", scope: !98, file: !96, line: 105, baseType: !103, size: 64, offset: 64)
+!103 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: !104, size: 64)
+!104 = distinct !DICompositeType(tag: DW_TAG_structure_type, name: "__darwin_pthread_handler_rec", file: !96, line: 57, size: 192, elements: !105)
+!105 = !{!106, !110, !111}
+!106 = !DIDerivedType(tag: DW_TAG_member, name: "__routine", scope: !104, file: !96, line: 58, baseType: !107, size: 64)
+!107 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: !108, size: 64)
+!108 = !DISubroutineType(types: !109)
+!109 = !{null, !5}
+!110 = !DIDerivedType(tag: DW_TAG_member, name: "__arg", scope: !104, file: !96, line: 59, baseType: !5, size: 64, offset: 64)
+!111 = !DIDerivedType(tag: DW_TAG_member, name: "__next", scope: !104, file: !96, line: 60, baseType: !103, size: 64, offset: 128)
+!112 = !DIDerivedType(tag: DW_TAG_member, name: "__opaque", scope: !98, file: !96, line: 106, baseType: !113, size: 65408, offset: 128)
+!113 = !DICompositeType(tag: DW_TAG_array_type, baseType: !114, size: 65408, elements: !115)
+!114 = !DIBasicType(name: "char", size: 8, encoding: DW_ATE_signed_char)
+!115 = !{!116}
+!116 = !DISubrange(count: 8176)
+!117 = !DILocation(line: 43, column: 15, scope: !89)
+!118 = !DILocalVariable(name: "t2", scope: !89, file: !9, line: 43, type: !93)
+!119 = !DILocation(line: 43, column: 19, scope: !89)
+!120 = !DILocalVariable(name: "t3", scope: !89, file: !9, line: 43, type: !93)
+!121 = !DILocation(line: 43, column: 23, scope: !89)
+!122 = !DILocation(line: 44, column: 5, scope: !89)
+!123 = !DILocation(line: 45, column: 5, scope: !89)
+!124 = !DILocation(line: 46, column: 5, scope: !89)
+!125 = !DILocation(line: 48, column: 5, scope: !89)
diff --git a/dartagnan/src/test/resources/nontermination/nontermination_weak.ll b/dartagnan/src/test/resources/nontermination/nontermination_weak.ll
index 6256aac53e..7f4b576c21 100644
--- a/dartagnan/src/test/resources/nontermination/nontermination_weak.ll
+++ b/dartagnan/src/test/resources/nontermination/nontermination_weak.ll
@@ -8,80 +8,82 @@ target triple = "arm64-apple-macosx14.0.0"
 %struct._opaque_pthread_attr_t = type { i64, [56 x i8] }
 
 @x = global i32 0, align 4, !dbg !0
-@signal = global i32 0, align 4, !dbg !7
-@success = global i32 0, align 4, !dbg !12
+@signal = global i32 0, align 4, !dbg !18
+@success = global i32 0, align 4, !dbg !24
 
 ; Function Attrs: noinline nounwind ssp uwtable
-define i8* @thread(i8* noundef %0) #0 !dbg !25 {
+define i8* @thread(i8* noundef %0) #0 !dbg !38 {
   %2 = alloca i8*, align 8
-  %3 = alloca i8*, align 8
-  store i8* %0, i8** %3, align 8
-  call void @llvm.dbg.declare(metadata i8** %3, metadata !29, metadata !DIExpression()), !dbg !30
-  br label %4, !dbg !31
+  %3 = alloca i32, align 4
+  store i8* %0, i8** %2, align 8
+  call void @llvm.dbg.declare(metadata i8** %2, metadata !42, metadata !DIExpression()), !dbg !43
+  br label %4, !dbg !44
 
 4:                                                ; preds = %8, %1
-  %5 = load volatile i32, i32* @success, align 4, !dbg !32
-  %6 = icmp ne i32 %5, 0, !dbg !33
-  %7 = xor i1 %6, true, !dbg !33
-  br i1 %7, label %8, label %9, !dbg !31
+  %5 = load atomic i32, i32* @success seq_cst, align 4, !dbg !45
+  %6 = icmp ne i32 %5, 0, !dbg !46
+  %7 = xor i1 %6, true, !dbg !46
+  br i1 %7, label %8, label %10, !dbg !44
 
 8:                                                ; preds = %4
-  store volatile i32 1, i32* @x, align 4, !dbg !34
-  store volatile i32 1, i32* @signal, align 4, !dbg !36
-  br label %4, !dbg !31, !llvm.loop !37
-
-9:                                                ; preds = %4
-  %10 = load i8*, i8** %2, align 8, !dbg !40
-  ret i8* %10, !dbg !40
+  store volatile i32 1, i32* @x, align 4, !dbg !47
+  store i32 1, i32* %3, align 4, !dbg !49
+  %9 = load i32, i32* %3, align 4, !dbg !49
+  store atomic i32 %9, i32* @signal monotonic, align 4, !dbg !49
+  br label %4, !dbg !44, !llvm.loop !50
+
+10:                                               ; preds = %4
+  ret i8* null, !dbg !53
 }
 
 ; 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* @thread2(i8* noundef %0) #0 !dbg !41 {
+define i8* @thread2(i8* noundef %0) #0 !dbg !54 {
   %2 = alloca i8*, align 8
-  %3 = alloca i8*, align 8
-  store i8* %0, i8** %3, align 8
-  call void @llvm.dbg.declare(metadata i8** %3, metadata !42, metadata !DIExpression()), !dbg !43
-  br label %4, !dbg !44
+  %3 = alloca i32, align 4
+  store i8* %0, i8** %2, align 8
+  call void @llvm.dbg.declare(metadata i8** %2, metadata !55, metadata !DIExpression()), !dbg !56
+  br label %4, !dbg !57
+
+4:                                                ; preds = %13, %1
+  %5 = load atomic i32, i32* @signal monotonic, align 4, !dbg !58
+  store i32 %5, i32* %3, align 4, !dbg !58
+  %6 = load i32, i32* %3, align 4, !dbg !58
+  %7 = icmp eq i32 %6, 1, !dbg !59
+  br i1 %7, label %8, label %11, !dbg !60
 
-4:                                                ; preds = %12, %1
-  %5 = load volatile i32, i32* @signal, align 4, !dbg !45
-  %6 = icmp eq i32 %5, 1, !dbg !46
-  br i1 %6, label %7, label %10, !dbg !47
-
-7:                                                ; preds = %4
-  %8 = load volatile i32, i32* @x, align 4, !dbg !48
-  %9 = icmp eq i32 %8, 0, !dbg !49
-  br label %10
-
-10:                                               ; preds = %7, %4
-  %11 = phi i1 [ false, %4 ], [ %9, %7 ], !dbg !50
-  br i1 %11, label %12, label %13, !dbg !44
-
-12:                                               ; preds = %10
-  store volatile i32 0, i32* @x, align 4, !dbg !51
-  store volatile i32 0, i32* @signal, align 4, !dbg !53
-  br label %4, !dbg !44, !llvm.loop !54
-
-13:                                               ; preds = %10
-  store volatile i32 1, i32* @success, align 4, !dbg !56
-  %14 = load i8*, i8** %2, align 8, !dbg !57
-  ret i8* %14, !dbg !57
+8:                                                ; preds = %4
+  %9 = load volatile i32, i32* @x, align 4, !dbg !61
+  %10 = icmp eq i32 %9, 0, !dbg !62
+  br label %11
+
+11:                                               ; preds = %8, %4
+  %12 = phi i1 [ false, %4 ], [ %10, %8 ], !dbg !63
+  br i1 %12, label %13, label %14, !dbg !57
+
+13:                                               ; preds = %11
+  store volatile i32 0, i32* @x, align 4, !dbg !64
+  store atomic i32 0, i32* @signal seq_cst, align 4, !dbg !66
+  br label %4, !dbg !57, !llvm.loop !67
+
+14:                                               ; preds = %11
+  store atomic i32 1, i32* @success seq_cst, align 4, !dbg !69
+  ret i8* null, !dbg !70
 }
 
 ; Function Attrs: noinline nounwind ssp uwtable
-define i32 @main() #0 !dbg !58 {
+define i32 @main() #0 !dbg !71 {
   %1 = alloca i32, align 4
   %2 = alloca %struct._opaque_pthread_t*, align 8
   %3 = alloca %struct._opaque_pthread_t*, align 8
   store i32 0, i32* %1, align 4
-  call void @llvm.dbg.declare(metadata %struct._opaque_pthread_t** %2, metadata !61, metadata !DIExpression()), !dbg !86
-  call void @llvm.dbg.declare(metadata %struct._opaque_pthread_t** %3, metadata !87, metadata !DIExpression()), !dbg !88
-  %4 = call i32 @pthread_create(%struct._opaque_pthread_t** noundef %2, %struct._opaque_pthread_attr_t* noundef null, i8* (i8*)* noundef @thread, i8* noundef null), !dbg !89
-  %5 = call i32 @pthread_create(%struct._opaque_pthread_t** noundef %3, %struct._opaque_pthread_attr_t* noundef null, i8* (i8*)* noundef @thread2, i8* noundef null), !dbg !90
-  ret i32 0, !dbg !91
+  call void @llvm.dbg.declare(metadata %struct._opaque_pthread_t** %2, metadata !74, metadata !DIExpression()), !dbg !99
+  call void @llvm.dbg.declare(metadata %struct._opaque_pthread_t** %3, metadata !100, metadata !DIExpression()), !dbg !101
+  %4 = call i32 @pthread_create(%struct._opaque_pthread_t** noundef %2, %struct._opaque_pthread_attr_t* noundef null, i8* (i8*)* noundef @thread, i8* noundef null), !dbg !102
+  %5 = call i32 @pthread_create(%struct._opaque_pthread_t** noundef %3, %struct._opaque_pthread_attr_t* noundef null, i8* (i8*)* noundef @thread2, i8* noundef null), !dbg !103
+  ret i32 0, !dbg !104
 }
 
 declare i32 @pthread_create(%struct._opaque_pthread_t** noundef, %struct._opaque_pthread_attr_t* noundef, i8* (i8*)* noundef, i8* noundef) #2
@@ -91,98 +93,111 @@ 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 = !{!14, !15, !16, !17, !18, !19, !20, !21, !22, !23}
-!llvm.ident = !{!24}
+!llvm.module.flags = !{!27, !28, !29, !30, !31, !32, !33, !34, !35, !36}
+!llvm.ident = !{!37}
 
 !0 = !DIGlobalVariableExpression(var: !1, expr: !DIExpression())
-!1 = distinct !DIGlobalVariable(name: "x", scope: !2, file: !9, line: 9, type: !10, 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")
+!1 = distinct !DIGlobalVariable(name: "x", scope: !2, file: !20, line: 9, type: !26, 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, enums: !4, retainedTypes: !15, globals: !17, splitDebugInlining: false, nameTableKind: None, sysroot: "/Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk", sdk: "MacOSX13.sdk")
 !3 = !DIFile(filename: "/Users/thomashaas/IdeaProjects/Dat3M/benchmarks/nontermination/nontermination_weak.c", directory: "/Users/thomashaas/IdeaProjects/Dat3M")
 !4 = !{!5}
-!5 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: null, size: 64)
-!6 = !{!0, !7, !12}
-!7 = !DIGlobalVariableExpression(var: !8, expr: !DIExpression())
-!8 = distinct !DIGlobalVariable(name: "signal", scope: !2, file: !9, line: 10, type: !10, isLocal: false, isDefinition: true)
-!9 = !DIFile(filename: "benchmarks/nontermination/nontermination_weak.c", directory: "/Users/thomashaas/IdeaProjects/Dat3M")
-!10 = !DIDerivedType(tag: DW_TAG_volatile_type, baseType: !11)
-!11 = !DIBasicType(name: "int", size: 32, encoding: DW_ATE_signed)
-!12 = !DIGlobalVariableExpression(var: !13, expr: !DIExpression())
-!13 = distinct !DIGlobalVariable(name: "success", scope: !2, file: !9, line: 11, type: !10, isLocal: false, isDefinition: true)
-!14 = !{i32 7, !"Dwarf Version", i32 4}
-!15 = !{i32 2, !"Debug Info Version", i32 3}
-!16 = !{i32 1, !"wchar_size", i32 4}
-!17 = !{i32 1, !"branch-target-enforcement", i32 0}
-!18 = !{i32 1, !"sign-return-address", i32 0}
-!19 = !{i32 1, !"sign-return-address-all", i32 0}
-!20 = !{i32 1, !"sign-return-address-with-bkey", i32 0}
-!21 = !{i32 7, !"PIC Level", i32 2}
-!22 = !{i32 7, !"uwtable", i32 1}
-!23 = !{i32 7, !"frame-pointer", i32 1}
-!24 = !{!"Homebrew clang version 14.0.6"}
-!25 = distinct !DISubprogram(name: "thread", scope: !9, file: !9, line: 13, type: !26, scopeLine: 14, flags: DIFlagPrototyped, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !28)
-!26 = !DISubroutineType(types: !27)
-!27 = !{!5, !5}
-!28 = !{}
-!29 = !DILocalVariable(name: "unused", arg: 1, scope: !25, file: !9, line: 13, type: !5)
-!30 = !DILocation(line: 13, column: 20, scope: !25)
-!31 = !DILocation(line: 15, column: 5, scope: !25)
-!32 = !DILocation(line: 15, column: 12, scope: !25)
-!33 = !DILocation(line: 15, column: 11, scope: !25)
-!34 = !DILocation(line: 16, column: 11, scope: !35)
-!35 = distinct !DILexicalBlock(scope: !25, file: !9, line: 15, column: 21)
-!36 = !DILocation(line: 17, column: 16, scope: !35)
-!37 = distinct !{!37, !31, !38, !39}
-!38 = !DILocation(line: 18, column: 5, scope: !25)
-!39 = !{!"llvm.loop.mustprogress"}
-!40 = !DILocation(line: 19, column: 1, scope: !25)
-!41 = distinct !DISubprogram(name: "thread2", scope: !9, file: !9, line: 21, type: !26, scopeLine: 21, flags: DIFlagPrototyped, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !28)
-!42 = !DILocalVariable(name: "unused", arg: 1, scope: !41, file: !9, line: 21, type: !5)
-!43 = !DILocation(line: 21, column: 21, scope: !41)
-!44 = !DILocation(line: 22, column: 5, scope: !41)
-!45 = !DILocation(line: 22, column: 12, scope: !41)
-!46 = !DILocation(line: 22, column: 19, scope: !41)
-!47 = !DILocation(line: 22, column: 24, scope: !41)
-!48 = !DILocation(line: 22, column: 27, scope: !41)
-!49 = !DILocation(line: 22, column: 29, scope: !41)
-!50 = !DILocation(line: 0, scope: !41)
-!51 = !DILocation(line: 24, column: 11, scope: !52)
-!52 = distinct !DILexicalBlock(scope: !41, file: !9, line: 22, column: 35)
-!53 = !DILocation(line: 25, column: 16, scope: !52)
-!54 = distinct !{!54, !44, !55, !39}
-!55 = !DILocation(line: 26, column: 5, scope: !41)
-!56 = !DILocation(line: 27, column: 13, scope: !41)
-!57 = !DILocation(line: 28, column: 1, scope: !41)
-!58 = distinct !DISubprogram(name: "main", scope: !9, file: !9, line: 30, type: !59, scopeLine: 31, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !28)
-!59 = !DISubroutineType(types: !60)
-!60 = !{!11}
-!61 = !DILocalVariable(name: "t1", scope: !58, file: !9, line: 32, type: !62)
-!62 = !DIDerivedType(tag: DW_TAG_typedef, name: "pthread_t", file: !63, line: 31, baseType: !64)
-!63 = !DIFile(filename: "/Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk/usr/include/sys/_pthread/_pthread_t.h", directory: "")
-!64 = !DIDerivedType(tag: DW_TAG_typedef, name: "__darwin_pthread_t", file: !65, line: 118, baseType: !66)
-!65 = !DIFile(filename: "/Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk/usr/include/sys/_pthread/_pthread_types.h", directory: "")
-!66 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: !67, size: 64)
-!67 = distinct !DICompositeType(tag: DW_TAG_structure_type, name: "_opaque_pthread_t", file: !65, line: 103, size: 65536, elements: !68)
-!68 = !{!69, !71, !81}
-!69 = !DIDerivedType(tag: DW_TAG_member, name: "__sig", scope: !67, file: !65, line: 104, baseType: !70, size: 64)
-!70 = !DIBasicType(name: "long", size: 64, encoding: DW_ATE_signed)
-!71 = !DIDerivedType(tag: DW_TAG_member, name: "__cleanup_stack", scope: !67, file: !65, line: 105, baseType: !72, size: 64, offset: 64)
-!72 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: !73, size: 64)
-!73 = distinct !DICompositeType(tag: DW_TAG_structure_type, name: "__darwin_pthread_handler_rec", file: !65, line: 57, size: 192, elements: !74)
-!74 = !{!75, !79, !80}
-!75 = !DIDerivedType(tag: DW_TAG_member, name: "__routine", scope: !73, file: !65, line: 58, baseType: !76, size: 64)
-!76 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: !77, size: 64)
-!77 = !DISubroutineType(types: !78)
-!78 = !{null, !5}
-!79 = !DIDerivedType(tag: DW_TAG_member, name: "__arg", scope: !73, file: !65, line: 59, baseType: !5, size: 64, offset: 64)
-!80 = !DIDerivedType(tag: DW_TAG_member, name: "__next", scope: !73, file: !65, line: 60, baseType: !72, size: 64, offset: 128)
-!81 = !DIDerivedType(tag: DW_TAG_member, name: "__opaque", scope: !67, file: !65, line: 106, baseType: !82, size: 65408, offset: 128)
-!82 = !DICompositeType(tag: DW_TAG_array_type, baseType: !83, size: 65408, elements: !84)
-!83 = !DIBasicType(name: "char", size: 8, encoding: DW_ATE_signed_char)
-!84 = !{!85}
-!85 = !DISubrange(count: 8176)
-!86 = !DILocation(line: 32, column: 15, scope: !58)
-!87 = !DILocalVariable(name: "t2", scope: !58, file: !9, line: 32, type: !62)
-!88 = !DILocation(line: 32, column: 19, scope: !58)
-!89 = !DILocation(line: 33, column: 5, scope: !58)
-!90 = !DILocation(line: 34, column: 5, scope: !58)
-!91 = !DILocation(line: 36, column: 5, scope: !58)
+!5 = !DICompositeType(tag: DW_TAG_enumeration_type, name: "memory_order", file: !6, line: 56, baseType: !7, size: 32, elements: !8)
+!6 = !DIFile(filename: "/opt/homebrew/Cellar/llvm@14/14.0.6/lib/clang/14.0.6/include/stdatomic.h", directory: "")
+!7 = !DIBasicType(name: "unsigned int", size: 32, encoding: DW_ATE_unsigned)
+!8 = !{!9, !10, !11, !12, !13, !14}
+!9 = !DIEnumerator(name: "memory_order_relaxed", value: 0)
+!10 = !DIEnumerator(name: "memory_order_consume", value: 1)
+!11 = !DIEnumerator(name: "memory_order_acquire", value: 2)
+!12 = !DIEnumerator(name: "memory_order_release", value: 3)
+!13 = !DIEnumerator(name: "memory_order_acq_rel", value: 4)
+!14 = !DIEnumerator(name: "memory_order_seq_cst", value: 5)
+!15 = !{!16}
+!16 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: null, size: 64)
+!17 = !{!0, !18, !24}
+!18 = !DIGlobalVariableExpression(var: !19, expr: !DIExpression())
+!19 = distinct !DIGlobalVariable(name: "signal", scope: !2, file: !20, line: 10, type: !21, isLocal: false, isDefinition: true)
+!20 = !DIFile(filename: "benchmarks/nontermination/nontermination_weak.c", directory: "/Users/thomashaas/IdeaProjects/Dat3M")
+!21 = !DIDerivedType(tag: DW_TAG_typedef, name: "atomic_int", file: !6, line: 92, baseType: !22)
+!22 = !DIDerivedType(tag: DW_TAG_atomic_type, baseType: !23)
+!23 = !DIBasicType(name: "int", size: 32, encoding: DW_ATE_signed)
+!24 = !DIGlobalVariableExpression(var: !25, expr: !DIExpression())
+!25 = distinct !DIGlobalVariable(name: "success", scope: !2, file: !20, line: 11, type: !21, isLocal: false, isDefinition: true)
+!26 = !DIDerivedType(tag: DW_TAG_volatile_type, baseType: !23)
+!27 = !{i32 7, !"Dwarf Version", i32 4}
+!28 = !{i32 2, !"Debug Info Version", i32 3}
+!29 = !{i32 1, !"wchar_size", i32 4}
+!30 = !{i32 1, !"branch-target-enforcement", i32 0}
+!31 = !{i32 1, !"sign-return-address", i32 0}
+!32 = !{i32 1, !"sign-return-address-all", i32 0}
+!33 = !{i32 1, !"sign-return-address-with-bkey", i32 0}
+!34 = !{i32 7, !"PIC Level", i32 2}
+!35 = !{i32 7, !"uwtable", i32 1}
+!36 = !{i32 7, !"frame-pointer", i32 1}
+!37 = !{!"Homebrew clang version 14.0.6"}
+!38 = distinct !DISubprogram(name: "thread", scope: !20, file: !20, line: 13, type: !39, scopeLine: 14, flags: DIFlagPrototyped, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !41)
+!39 = !DISubroutineType(types: !40)
+!40 = !{!16, !16}
+!41 = !{}
+!42 = !DILocalVariable(name: "unused", arg: 1, scope: !38, file: !20, line: 13, type: !16)
+!43 = !DILocation(line: 13, column: 20, scope: !38)
+!44 = !DILocation(line: 15, column: 5, scope: !38)
+!45 = !DILocation(line: 15, column: 12, scope: !38)
+!46 = !DILocation(line: 15, column: 11, scope: !38)
+!47 = !DILocation(line: 16, column: 11, scope: !48)
+!48 = distinct !DILexicalBlock(scope: !38, file: !20, line: 15, column: 21)
+!49 = !DILocation(line: 17, column: 9, scope: !48)
+!50 = distinct !{!50, !44, !51, !52}
+!51 = !DILocation(line: 18, column: 5, scope: !38)
+!52 = !{!"llvm.loop.mustprogress"}
+!53 = !DILocation(line: 19, column: 5, scope: !38)
+!54 = distinct !DISubprogram(name: "thread2", scope: !20, file: !20, line: 22, type: !39, scopeLine: 22, flags: DIFlagPrototyped, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !41)
+!55 = !DILocalVariable(name: "unused", arg: 1, scope: !54, file: !20, line: 22, type: !16)
+!56 = !DILocation(line: 22, column: 21, scope: !54)
+!57 = !DILocation(line: 23, column: 5, scope: !54)
+!58 = !DILocation(line: 23, column: 12, scope: !54)
+!59 = !DILocation(line: 23, column: 64, scope: !54)
+!60 = !DILocation(line: 23, column: 69, scope: !54)
+!61 = !DILocation(line: 23, column: 72, scope: !54)
+!62 = !DILocation(line: 23, column: 74, scope: !54)
+!63 = !DILocation(line: 0, scope: !54)
+!64 = !DILocation(line: 25, column: 11, scope: !65)
+!65 = distinct !DILexicalBlock(scope: !54, file: !20, line: 23, column: 80)
+!66 = !DILocation(line: 26, column: 16, scope: !65)
+!67 = distinct !{!67, !57, !68, !52}
+!68 = !DILocation(line: 27, column: 5, scope: !54)
+!69 = !DILocation(line: 28, column: 13, scope: !54)
+!70 = !DILocation(line: 29, column: 5, scope: !54)
+!71 = distinct !DISubprogram(name: "main", scope: !20, file: !20, line: 32, type: !72, scopeLine: 33, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !41)
+!72 = !DISubroutineType(types: !73)
+!73 = !{!23}
+!74 = !DILocalVariable(name: "t1", scope: !71, file: !20, line: 34, type: !75)
+!75 = !DIDerivedType(tag: DW_TAG_typedef, name: "pthread_t", file: !76, line: 31, baseType: !77)
+!76 = !DIFile(filename: "/Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk/usr/include/sys/_pthread/_pthread_t.h", directory: "")
+!77 = !DIDerivedType(tag: DW_TAG_typedef, name: "__darwin_pthread_t", file: !78, line: 118, baseType: !79)
+!78 = !DIFile(filename: "/Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk/usr/include/sys/_pthread/_pthread_types.h", directory: "")
+!79 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: !80, size: 64)
+!80 = distinct !DICompositeType(tag: DW_TAG_structure_type, name: "_opaque_pthread_t", file: !78, line: 103, size: 65536, elements: !81)
+!81 = !{!82, !84, !94}
+!82 = !DIDerivedType(tag: DW_TAG_member, name: "__sig", scope: !80, file: !78, line: 104, baseType: !83, size: 64)
+!83 = !DIBasicType(name: "long", size: 64, encoding: DW_ATE_signed)
+!84 = !DIDerivedType(tag: DW_TAG_member, name: "__cleanup_stack", scope: !80, file: !78, line: 105, baseType: !85, size: 64, offset: 64)
+!85 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: !86, size: 64)
+!86 = distinct !DICompositeType(tag: DW_TAG_structure_type, name: "__darwin_pthread_handler_rec", file: !78, line: 57, size: 192, elements: !87)
+!87 = !{!88, !92, !93}
+!88 = !DIDerivedType(tag: DW_TAG_member, name: "__routine", scope: !86, file: !78, line: 58, baseType: !89, size: 64)
+!89 = !DIDerivedType(tag: DW_TAG_pointer_type, baseType: !90, size: 64)
+!90 = !DISubroutineType(types: !91)
+!91 = !{null, !16}
+!92 = !DIDerivedType(tag: DW_TAG_member, name: "__arg", scope: !86, file: !78, line: 59, baseType: !16, size: 64, offset: 64)
+!93 = !DIDerivedType(tag: DW_TAG_member, name: "__next", scope: !86, file: !78, line: 60, baseType: !85, size: 64, offset: 128)
+!94 = !DIDerivedType(tag: DW_TAG_member, name: "__opaque", scope: !80, file: !78, line: 106, baseType: !95, size: 65408, offset: 128)
+!95 = !DICompositeType(tag: DW_TAG_array_type, baseType: !96, size: 65408, elements: !97)
+!96 = !DIBasicType(name: "char", size: 8, encoding: DW_ATE_signed_char)
+!97 = !{!98}
+!98 = !DISubrange(count: 8176)
+!99 = !DILocation(line: 34, column: 15, scope: !71)
+!100 = !DILocalVariable(name: "t2", scope: !71, file: !20, line: 34, type: !75)
+!101 = !DILocation(line: 34, column: 19, scope: !71)
+!102 = !DILocation(line: 35, column: 5, scope: !71)
+!103 = !DILocation(line: 36, column: 5, scope: !71)
+!104 = !DILocation(line: 38, column: 5, scope: !71)
diff --git a/dartagnan/src/test/resources/nontermination/nontermination_xchg.ll b/dartagnan/src/test/resources/nontermination/nontermination_xchg.ll
index d9ba7c0d33..dd8c549334 100644
--- a/dartagnan/src/test/resources/nontermination/nontermination_xchg.ll
+++ b/dartagnan/src/test/resources/nontermination/nontermination_xchg.ll
@@ -12,28 +12,26 @@ target triple = "arm64-apple-macosx14.0.0"
 ; Function Attrs: noinline nounwind ssp uwtable
 define i8* @thread(i8* noundef %0) #0 !dbg !23 {
   %2 = alloca i8*, align 8
-  %3 = alloca i8*, align 8
+  %3 = alloca i32, align 4
   %4 = alloca i32, align 4
-  %5 = alloca i32, align 4
-  store i8* %0, i8** %3, align 8
-  call void @llvm.dbg.declare(metadata i8** %3, metadata !27, metadata !DIExpression()), !dbg !28
-  br label %6, !dbg !29
+  store i8* %0, i8** %2, align 8
+  call void @llvm.dbg.declare(metadata i8** %2, metadata !27, metadata !DIExpression()), !dbg !28
+  br label %5, !dbg !29
 
-6:                                                ; preds = %11, %1
-  store i32 1, i32* %4, align 4, !dbg !30
-  %7 = load i32, i32* %4, align 4, !dbg !30
-  %8 = atomicrmw xchg i32* @lock, i32 %7 seq_cst, align 4, !dbg !30
-  store i32 %8, i32* %5, align 4, !dbg !30
-  %9 = load i32, i32* %5, align 4, !dbg !30
-  %10 = icmp eq i32 %9, 1, !dbg !31
-  br i1 %10, label %11, label %12, !dbg !29
+5:                                                ; preds = %10, %1
+  store i32 1, i32* %3, align 4, !dbg !30
+  %6 = load i32, i32* %3, align 4, !dbg !30
+  %7 = atomicrmw xchg i32* @lock, i32 %6 seq_cst, align 4, !dbg !30
+  store i32 %7, i32* %4, align 4, !dbg !30
+  %8 = load i32, i32* %4, align 4, !dbg !30
+  %9 = icmp ne i32 %8, 0, !dbg !31
+  br i1 %9, label %10, label %11, !dbg !29
 
-11:                                               ; preds = %6
-  br label %6, !dbg !29, !llvm.loop !32
+10:                                               ; preds = %5
+  br label %5, !dbg !29, !llvm.loop !32
 
-12:                                               ; preds = %6
-  %13 = load i8*, i8** %2, align 8, !dbg !35
-  ret i8* %13, !dbg !35
+11:                                               ; preds = %5
+  ret i8* null, !dbg !35
 }
 
 ; Function Attrs: nofree nosync nounwind readnone speculatable willreturn
@@ -42,12 +40,16 @@ declare void @llvm.dbg.declare(metadata, metadata, metadata) #1
 ; Function Attrs: noinline nounwind ssp uwtable
 define i8* @thread2(i8* noundef %0) #0 !dbg !36 {
   %2 = alloca i8*, align 8
-  %3 = alloca i8*, align 8
-  store i8* %0, i8** %3, align 8
-  call void @llvm.dbg.declare(metadata i8** %3, metadata !37, metadata !DIExpression()), !dbg !38
-  store atomic i32 1, i32* @lock seq_cst, align 4, !dbg !39
-  %4 = load i8*, i8** %2, align 8, !dbg !40
-  ret i8* %4, !dbg !40
+  %3 = alloca i32, align 4
+  %4 = alloca i32, align 4
+  store i8* %0, i8** %2, align 8
+  call void @llvm.dbg.declare(metadata i8** %2, metadata !37, metadata !DIExpression()), !dbg !38
+  store i32 1, i32* %3, align 4, !dbg !39
+  %5 = load i32, i32* %3, align 4, !dbg !39
+  %6 = atomicrmw xchg i32* @lock, i32 %5 seq_cst, align 4, !dbg !39
+  store i32 %6, i32* %4, align 4, !dbg !39
+  %7 = load i32, i32* %4, align 4, !dbg !39
+  ret i8* null, !dbg !40
 }
 
 ; Function Attrs: noinline nounwind ssp uwtable
@@ -108,16 +110,16 @@ attributes #2 = { "frame-pointer"="non-leaf" "no-trapping-math"="true" "stack-pr
 !32 = distinct !{!32, !29, !33, !34}
 !33 = !DILocation(line: 13, column: 43, scope: !23)
 !34 = !{!"llvm.loop.mustprogress"}
-!35 = !DILocation(line: 14, column: 1, scope: !23)
-!36 = distinct !DISubprogram(name: "thread2", scope: !7, file: !7, line: 16, type: !24, scopeLine: 16, 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: 16, column: 21, scope: !36)
-!39 = !DILocation(line: 17, column: 10, scope: !36)
-!40 = !DILocation(line: 18, column: 1, scope: !36)
-!41 = distinct !DISubprogram(name: "main", scope: !7, file: !7, line: 20, type: !42, scopeLine: 21, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !26)
+!35 = !DILocation(line: 14, column: 5, scope: !23)
+!36 = distinct !DISubprogram(name: "thread2", scope: !7, file: !7, line: 17, type: !24, scopeLine: 17, flags: DIFlagPrototyped, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !26)
+!37 = !DILocalVariable(name: "unused", arg: 1, scope: !36, file: !7, line: 17, type: !5)
+!38 = !DILocation(line: 17, column: 21, scope: !36)
+!39 = !DILocation(line: 18, column: 5, scope: !36)
+!40 = !DILocation(line: 19, column: 5, scope: !36)
+!41 = distinct !DISubprogram(name: "main", scope: !7, file: !7, line: 22, type: !42, scopeLine: 23, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !26)
 !42 = !DISubroutineType(types: !43)
 !43 = !{!11}
-!44 = !DILocalVariable(name: "t1", scope: !41, file: !7, line: 22, type: !45)
+!44 = !DILocalVariable(name: "t1", scope: !41, file: !7, line: 24, 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)
@@ -142,9 +144,9 @@ attributes #2 = { "frame-pointer"="non-leaf" "no-trapping-math"="true" "stack-pr
 !66 = !DIBasicType(name: "char", size: 8, encoding: DW_ATE_signed_char)
 !67 = !{!68}
 !68 = !DISubrange(count: 8176)
-!69 = !DILocation(line: 22, column: 15, scope: !41)
-!70 = !DILocalVariable(name: "t2", scope: !41, file: !7, line: 22, type: !45)
-!71 = !DILocation(line: 22, column: 19, scope: !41)
-!72 = !DILocation(line: 24, column: 5, scope: !41)
-!73 = !DILocation(line: 25, column: 5, scope: !41)
-!74 = !DILocation(line: 27, column: 5, scope: !41)
+!69 = !DILocation(line: 24, column: 15, scope: !41)
+!70 = !DILocalVariable(name: "t2", scope: !41, file: !7, line: 24, type: !45)
+!71 = !DILocation(line: 24, column: 19, scope: !41)
+!72 = !DILocation(line: 26, column: 5, scope: !41)
+!73 = !DILocation(line: 27, column: 5, scope: !41)
+!74 = !DILocation(line: 29, column: 5, scope: !41)
diff --git a/dartagnan/src/test/resources/nontermination/nontermination_zero_effect.ll b/dartagnan/src/test/resources/nontermination/nontermination_zero_effect.ll
index b4fa8fd99f..6caacc1204 100644
--- a/dartagnan/src/test/resources/nontermination/nontermination_zero_effect.ll
+++ b/dartagnan/src/test/resources/nontermination/nontermination_zero_effect.ll
@@ -56,13 +56,11 @@ define void @releaseLock() #0 !dbg !39 {
 ; Function Attrs: noinline nounwind ssp uwtable
 define i8* @thread(i8* noundef %0) #0 !dbg !42 {
   %2 = alloca i8*, align 8
-  %3 = alloca i8*, align 8
-  store i8* %0, i8** %3, align 8
-  call void @llvm.dbg.declare(metadata i8** %3, metadata !45, metadata !DIExpression()), !dbg !46
+  store i8* %0, i8** %2, align 8
+  call void @llvm.dbg.declare(metadata i8** %2, metadata !45, metadata !DIExpression()), !dbg !46
   call void @acquireLock(), !dbg !47
   call void @releaseLock(), !dbg !48
-  %4 = load i8*, i8** %2, align 8, !dbg !49
-  ret i8* %4, !dbg !49
+  ret i8* null, !dbg !49
 }
 
 ; Function Attrs: nofree nosync nounwind readnone speculatable willreturn
@@ -144,11 +142,11 @@ attributes #2 = { "frame-pointer"="non-leaf" "no-trapping-math"="true" "stack-pr
 !46 = !DILocation(line: 24, column: 20, scope: !42)
 !47 = !DILocation(line: 26, column: 5, scope: !42)
 !48 = !DILocation(line: 27, column: 5, scope: !42)
-!49 = !DILocation(line: 28, column: 1, scope: !42)
-!50 = distinct !DISubprogram(name: "main", scope: !7, file: !7, line: 30, type: !51, scopeLine: 31, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !26)
+!49 = !DILocation(line: 28, column: 5, scope: !42)
+!50 = distinct !DISubprogram(name: "main", scope: !7, file: !7, line: 31, type: !51, scopeLine: 32, spFlags: DISPFlagDefinition, unit: !2, retainedNodes: !26)
 !51 = !DISubroutineType(types: !52)
 !52 = !{!11}
-!53 = !DILocalVariable(name: "t1", scope: !50, file: !7, line: 32, type: !54)
+!53 = !DILocalVariable(name: "t1", scope: !50, file: !7, line: 33, type: !54)
 !54 = !DIDerivedType(tag: DW_TAG_typedef, name: "pthread_t", file: !55, line: 31, baseType: !56)
 !55 = !DIFile(filename: "/Library/Developer/CommandLineTools/SDKs/MacOSX13.sdk/usr/include/sys/_pthread/_pthread_t.h", directory: "")
 !56 = !DIDerivedType(tag: DW_TAG_typedef, name: "__darwin_pthread_t", file: !57, line: 118, baseType: !58)
@@ -173,13 +171,13 @@ attributes #2 = { "frame-pointer"="non-leaf" "no-trapping-math"="true" "stack-pr
 !75 = !DIBasicType(name: "char", size: 8, encoding: DW_ATE_signed_char)
 !76 = !{!77}
 !77 = !DISubrange(count: 8176)
-!78 = !DILocation(line: 32, column: 15, scope: !50)
-!79 = !DILocalVariable(name: "t2", scope: !50, file: !7, line: 32, type: !54)
-!80 = !DILocation(line: 32, column: 19, scope: !50)
-!81 = !DILocalVariable(name: "t3", scope: !50, file: !7, line: 32, type: !54)
-!82 = !DILocation(line: 32, column: 23, scope: !50)
-!83 = !DILocation(line: 34, column: 5, scope: !50)
-!84 = !DILocation(line: 36, column: 5, scope: !50)
-!85 = !DILocation(line: 37, column: 5, scope: !50)
-!86 = !DILocation(line: 38, column: 5, scope: !50)
-!87 = !DILocation(line: 39, column: 5, scope: !50)
+!78 = !DILocation(line: 33, column: 15, scope: !50)
+!79 = !DILocalVariable(name: "t2", scope: !50, file: !7, line: 33, type: !54)
+!80 = !DILocation(line: 33, column: 19, scope: !50)
+!81 = !DILocalVariable(name: "t3", scope: !50, file: !7, line: 33, type: !54)
+!82 = !DILocation(line: 33, column: 23, scope: !50)
+!83 = !DILocation(line: 35, column: 5, scope: !50)
+!84 = !DILocation(line: 37, column: 5, scope: !50)
+!85 = !DILocation(line: 38, column: 5, scope: !50)
+!86 = !DILocation(line: 39, column: 5, scope: !50)
+!87 = !DILocation(line: 40, column: 5, scope: !50)