diff --git a/alloy/spirv.als b/alloy/spirv.als
index daf88a6..de5e3ff 100644
--- a/alloy/spirv.als
+++ b/alloy/spirv.als
@@ -355,14 +355,14 @@ sig Exec {
   // is not supported by ANDing with the identity relation.
   avsg = stor[AVSG]
   avwg = (chains & (rc[avsg . (hb & ssg & avvisinc)])) . (stor[AVWG])
-  avqf = (chains & (rc[avsg . (hb & ssg & avvisinc)]) . (rc[avwg . (hb & swg & avvisinc)])) . (stor[AVQF])
-  avsh = (chains & (rc[avsg . (hb & ssg & avvisinc)]) . (rc[avwg . (hb & swg & avvisinc)]) . (rc[avqf . (hb & sqf & avvisinc)])) . (stor[AVSHADER])
+  avqf = (chains & ((rc[avsg . (hb & ssg & avvisinc)]) + (rc[avwg . (hb & swg & avvisinc)]))) . (stor[AVQF])
+  avsh = (chains & ((rc[avsg . (hb & ssg & avvisinc)]) + (rc[avwg . (hb & swg & avvisinc)]) + (rc[avqf . (hb & sqf & avvisinc)]))) . (stor[AVSHADER])
   avdv = stor[AVDEVICE]
 
   vissg = stor[VISSG]
   viswg = (stor[VISWG])     . (chains & (rc[(hb & ssg & avvisinc) . vissg]))
-  visqf = (stor[VISQF])     . (chains & (rc[(hb & swg & avvisinc) . viswg]) . (rc[(hb & ssg & avvisinc) . vissg]))
-  vissh = (stor[VISSHADER]) . (chains & (rc[(hb & sqf & avvisinc) . visqf]) . (rc[(hb & swg & avvisinc) . viswg]) . (rc[(hb & ssg & avvisinc) . vissg]))
+  visqf = (stor[VISQF])     . (chains & ((rc[(hb & swg & avvisinc) . viswg]) + (rc[(hb & ssg & avvisinc) . vissg])))
+  vissh = (stor[VISSHADER]) . (chains & ((rc[(hb & sqf & avvisinc) . visqf]) + (rc[(hb & swg & avvisinc) . viswg]) + (rc[(hb & ssg & avvisinc) . vissg])))
   visdv = stor[VISDEVICE]
 
   locord = sloc & // relates memory accesses to the same location
diff --git a/alloy/tests/chains1.test b/alloy/tests/chains1.test
new file mode 100644
index 0000000..6443174
--- /dev/null
+++ b/alloy/tests/chains1.test
@@ -0,0 +1,26 @@
+// Copyright (c) 2025 Khronos Group. This work is licensed under a
+// Creative Commons Attribution 4.0 International License; see
+// http://creativecommons.org/licenses/by/4.0/
+
+NEWWG
+NEWSG
+NEWTHREAD
+st.atom.rel.scopesg.sc0.semsc0 a = 1
+NEWTHREAD
+ld.atom.acq.scopesg.sc0.semsc0 a = 1
+st.atom.rel.scopesg.sc1.semsc0.semsc1.semav b = 1
+NEWTHREAD
+ld.atom.acq.scopesg.sc1.semsc1 b = 1
+ld.atom.acq.scopesg.sc0.semsc0.semsc1.semvis a = 0
+st.atom.rel.scopewg.sc0.semsc0.semsc1.semav c = 1
+NEWSG
+NEWTHREAD
+ld.atom.acq.scopewg.sc0.semsc0 c = 1
+st.atom.rel.scopeqf.sc1.semsc0.semsc1.semav d = 1
+NEWWG
+NEWSG
+NEWTHREAD
+ld.atom.acq.scopeqf.sc1.semsc0.semsc1 d = 1
+
+SATISFIABLE consistent[X] && #dr=0
+NOSOLUTION consistent[X] && #dr>0
\ No newline at end of file
diff --git a/alloy/tests/chains2.test b/alloy/tests/chains2.test
new file mode 100644
index 0000000..4bca7d3
--- /dev/null
+++ b/alloy/tests/chains2.test
@@ -0,0 +1,26 @@
+// Copyright (c) 2025 Khronos Group. This work is licensed under a
+// Creative Commons Attribution 4.0 International License; see
+// http://creativecommons.org/licenses/by/4.0/
+
+NEWWG
+NEWSG
+NEWTHREAD
+st.atom.rel.scopesg.sc0.semsc0 a = 1
+NEWTHREAD
+ld.atom.acq.scopesg.sc0.semsc0 a = 1
+st.atom.rel.scopesg.sc1.semsc0.semsc1.semav b = 1
+NEWTHREAD
+ld.atom.acq.scopesg.sc1.semsc1 b = 1
+st.atom.rel.scopewg.sc0.semsc0.semsc1.semav c = 1
+NEWSG
+NEWTHREAD
+ld.atom.acq.scopewg.sc0.semsc0 c = 1
+ld.atom.acq.scopewg.sc0.semsc0.semsc1.semvis a = 0
+st.atom.rel.scopeqf.sc1.semsc0.semsc1.semav d = 1
+NEWWG
+NEWSG
+NEWTHREAD
+ld.atom.acq.scopeqf.sc1.semsc0.semsc1 d = 1
+
+SATISFIABLE consistent[X] && #dr>0
+NOSOLUTION consistent[X] && #dr=0
\ No newline at end of file
diff --git a/alloy/tests/chains3.test b/alloy/tests/chains3.test
new file mode 100644
index 0000000..a51c558
--- /dev/null
+++ b/alloy/tests/chains3.test
@@ -0,0 +1,26 @@
+// Copyright (c) 2025 Khronos Group. This work is licensed under a
+// Creative Commons Attribution 4.0 International License; see
+// http://creativecommons.org/licenses/by/4.0/
+
+NEWWG
+NEWSG
+NEWTHREAD
+st.atom.rel.scopesg.sc0.semsc0 a = 1
+NEWTHREAD
+ld.atom.acq.scopesg.sc0.semsc0 a = 1
+st.atom.rel.scopesg.sc1.semsc0.semsc1.semav b = 1
+NEWTHREAD
+ld.atom.acq.scopesg.sc1.semsc1 b = 1
+st.atom.rel.scopewg.sc0.semsc0.semsc1.semav c = 1
+NEWSG
+NEWTHREAD
+ld.atom.acq.scopewg.sc0.semsc0 c = 1
+st.atom.rel.scopeqf.sc1.semsc0.semsc1.semav d = 1
+NEWWG
+NEWSG
+NEWTHREAD
+ld.atom.acq.scopeqf.sc1.semsc0.semsc1 d = 1
+ld.atom.acq.scopeqf.sc0.semsc0.semsc1.semvis a = 0
+
+SATISFIABLE consistent[X] && #dr>0
+NOSOLUTION consistent[X] && #dr=0
\ No newline at end of file
diff --git a/alloy/tests/chains4.test b/alloy/tests/chains4.test
new file mode 100644
index 0000000..21b25a7
--- /dev/null
+++ b/alloy/tests/chains4.test
@@ -0,0 +1,24 @@
+// Copyright (c) 2025 Khronos Group. This work is licensed under a
+// Creative Commons Attribution 4.0 International License; see
+// http://creativecommons.org/licenses/by/4.0/
+
+NEWQF
+NEWWG
+NEWSG
+NEWTHREAD
+st.atom.rel.scopesg.sc0.semsc0 a = 1
+NEWTHREAD
+ld.atom.acq.scopesg.sc0.semsc0 a = 1
+st.atom.rel.scopewg.sc1.semsc0.semsc1.semav b = 1
+NEWSG
+NEWTHREAD
+ld.atom.acq.scopewg.sc1.semsc1 b = 1
+st.atom.rel.scopedev.sc0.semsc0.semsc1.semav c = 1
+NEWQF
+NEWWG
+NEWSG
+NEWTHREAD
+ld.atom.acq.scopedev.sc0.semsc0 c = 1
+ld.atom.scopedev.sc0 a = 0
+
+NOSOLUTION consistent[X]
\ No newline at end of file
diff --git a/alloy/tests/chains5.test b/alloy/tests/chains5.test
new file mode 100644
index 0000000..36145ca
--- /dev/null
+++ b/alloy/tests/chains5.test
@@ -0,0 +1,33 @@
+// Copyright (c) 2025 Khronos Group. This work is licensed under a
+// Creative Commons Attribution 4.0 International License; see
+// http://creativecommons.org/licenses/by/4.0/
+
+NEWWG
+NEWSG
+NEWTHREAD
+st.atom.rel.scopewg.sc0.semsc0 a = 1
+NEWSG
+NEWTHREAD
+ld.atom.acq.scopewg.sc0.semsc0 a = 1
+st.atom.rel.scopesg.sc1.semsc0.semsc1.semav b = 1
+NEWTHREAD
+ld.atom.acq.scopesg.sc1.semsc1 b = 1
+st.atom.rel.scopewg.sc0.semsc0.semsc1.semav c = 1
+NEWSG
+NEWTHREAD
+ld.atom.acq.scopewg.sc0.semsc0 c = 1
+st.atom.rel.scopeqf.sc1.semsc0.semsc1.semav d = 1
+NEWWG
+NEWSG
+NEWTHREAD
+ld.atom.acq.scopeqf.sc1.semsc1 d = 1
+st.atom.rel.scopedev.sc0.semsc0.semsc1.semav e = 1
+NEWQF
+NEWWG
+NEWSG
+NEWTHREAD
+ld.atom.acq.scopedev.sc0.semsc0 e = 1
+ld.atom.acq.scopedev.sc0.semsc0.semsc1.semvis a = 0
+
+SATISFIABLE consistent[X] && #dr>0
+NOSOLUTION consistent[X] && #dr=0
\ No newline at end of file