diff --git a/cat/ptx-v7.5.cat b/cat/ptx-v7.5.cat
index 58868482f0..b1701d36b9 100644
--- a/cat/ptx-v7.5.cat
+++ b/cat/ptx-v7.5.cat
@@ -77,8 +77,6 @@ let proxy-preserved-cause-base
                 | vloc & (cause-base & (proxy-fence-ops^-1); cause-base; [GEN])
                 | vloc & ([GEN]; cause-base; cause-base & proxy-fence-ops)
                 | vloc & (cause-base & (proxy-fence-ops^-1); cause-base; cause-base & proxy-fence-ops)
-                // The alloy model does not support the constant proxy below
-                | loc & ([M & CON]; cause-base; [F & CON]; cause-base; [M & CON])
                 | loc & ([GEN]; cause-base; [F & ALIAS]; cause-base; [GEN])
                 | loc & (cause-base & (proxy-fence-ops^-1); cause-base; [F & ALIAS]; cause-base; [GEN])
                 | loc & ([GEN]; cause-base; [F & ALIAS]; cause-base; cause-base & proxy-fence-ops)
diff --git a/cat/spirv-nochains.cat b/cat/spirv-nochains.cat
index 89941c8c89..0607eab516 100644
--- a/cat/spirv-nochains.cat
+++ b/cat/spirv-nochains.cat
@@ -129,8 +129,6 @@ let locord = loc &
                 (       ([W];        (hb & avvisinc);  avdv; (hb);       visdv; (hb & avvisinc);  [R]))            // RaW (via device domain)
              )
 
-let w-locord = [W]; locord
-
 (***********************)
 (* Memory Model Axioms *)
 (***********************)
diff --git a/cat/spirv.cat b/cat/spirv.cat
index d46758d168..e94382b535 100644
--- a/cat/spirv.cat
+++ b/cat/spirv.cat
@@ -129,8 +129,6 @@ let locord = loc &
                 (       ([W];        (hb & avvisinc);  avdv; (hb);       visdv; (hb & avvisinc);  [R]))            // RaW (via device domain)
              )
 
-let w-locord = [W]; locord
-
 (***********************)
 (* Memory Model Axioms *)
 (***********************)
diff --git a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPTX.java b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPTX.java
index 2998b6cfdc..40a1c1cf84 100644
--- a/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPTX.java
+++ b/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/VisitorLitmusPTX.java
@@ -142,19 +142,17 @@ public Object visitStoreConstant(LitmusPTXParser.StoreConstantContext ctx) {
         MemoryObject object = programBuilder.getOrNewMemoryObject(ctx.location().getText());
         IConst constant = (IConst) ctx.constant().accept(this);
         String mo = ctx.mo().content;
-        String scope;
+        Store store = EventFactory.newStoreWithMo(object, constant, mo);
         switch (mo) {
             case Tag.PTX.WEAK -> {
                 if (ctx.scope() != null) {
                     throw new ParsingException("Weak store instruction doesn't need scope: " + ctx.scope().content);
                 }
-                scope = Tag.PTX.SYS;
             }
-            case Tag.PTX.REL, Tag.PTX.RLX -> scope = ctx.scope().content;
+            case Tag.PTX.REL, Tag.PTX.RLX -> store.addTags(ctx.scope().content);
             default -> throw new ParsingException("Store instruction doesn't support mo: " + mo);
         }
-        Store store = EventFactory.newStoreWithMo(object, constant, mo);
-        store.addTags(scope, ctx.store().storeProxy, Tag.PTX.CON);
+        store.addTags(ctx.store().storeProxy);
         return programBuilder.addChild(mainThread, store);
     }
 
@@ -163,19 +161,17 @@ public Object visitStoreRegister(LitmusPTXParser.StoreRegisterContext ctx) {
         MemoryObject object = programBuilder.getOrNewMemoryObject(ctx.location().getText());
         Register register = (Register) ctx.register().accept(this);
         String mo = ctx.mo().content;
-        String scope;
+        Store store = EventFactory.newStoreWithMo(object, register, mo);
         switch (mo) {
             case Tag.PTX.WEAK -> {
                 if (ctx.scope() != null) {
                     throw new ParsingException("Weak store instruction doesn't need scope: " + ctx.scope().content);
                 }
-                scope = Tag.PTX.SYS;
             }
-            case Tag.PTX.REL, Tag.PTX.RLX -> scope = ctx.scope().content;
+            case Tag.PTX.REL, Tag.PTX.RLX -> store.addTags(ctx.scope().content);
             default -> throw new ParsingException("Store instruction doesn't support mo: " + mo);
         }
-        Store store = EventFactory.newStoreWithMo(object, register, mo);
-        store.addTags(scope, ctx.store().storeProxy);
+        store.addTags(ctx.store().storeProxy);
         return programBuilder.addChild(mainThread, store);
     }
 
@@ -227,19 +223,17 @@ public Object visitLoadLocation(LitmusPTXParser.LoadLocationContext ctx) {
         Register register = (Register) ctx.register().accept(this);
         MemoryObject location = programBuilder.getOrNewMemoryObject(ctx.location().getText());
         String mo = ctx.mo().content;
-        String scope;
+        Load load = EventFactory.newLoadWithMo(register, location, mo);
         switch (mo) {
             case Tag.PTX.WEAK -> {
                 if (ctx.scope() != null) {
                     throw new ParsingException("Weak load instruction doesn't need scope: " + ctx.scope().content);
                 }
-                scope = Tag.PTX.SYS;
             }
-            case Tag.PTX.ACQ, Tag.PTX.RLX -> scope = ctx.scope().content;
+            case Tag.PTX.ACQ, Tag.PTX.RLX -> load.addTags(ctx.scope().content);
             default -> throw new ParsingException("Load instruction doesn't support mo: " + mo);
         }
-        Load load = EventFactory.newLoadWithMo(register, location, mo);
-        load.addTags(scope, ctx.load().loadProxy);
+        load.addTags(ctx.load().loadProxy);
         return programBuilder.addChild(mainThread, load);
     }
 
diff --git a/litmus/PTX/Nvidia/Proxy-Const-ConstFence.litmus b/litmus/PTX/Nvidia/Proxy-Const-ConstFence.litmus
index f418f110ea..0888d86466 100644
--- a/litmus/PTX/Nvidia/Proxy-Const-ConstFence.litmus
+++ b/litmus/PTX/Nvidia/Proxy-Const-ConstFence.litmus
@@ -2,7 +2,7 @@ PTX Proxy-Const-with-ConstFence
 "A single thread example showing constant proxy fence usage"
 {
 rd1 = 0;
-rd2 @ generic aliases rd1;
+rd2 @ constant aliases rd1;
 P0:r0=0;
 }
  P0@cta 0,gpu 0                   ;
diff --git a/litmus/PTX/Nvidia/Proxy-Const-MP-cause1.litmus b/litmus/PTX/Nvidia/Proxy-Const-MP-cause1.litmus
index 3fdeeac60a..3f67de9638 100644
--- a/litmus/PTX/Nvidia/Proxy-Const-MP-cause1.litmus
+++ b/litmus/PTX/Nvidia/Proxy-Const-MP-cause1.litmus
@@ -3,7 +3,7 @@ PTX Proxy-Const-MP-cause1
 "The constant fence along the base causality path from the weak st to the cold, hence rf is guaranteed"
 {
 rd1 = 0;
-rd2 @ generic aliases rd1;
+rd2 @ constant aliases rd1;
 rd4 = 0;
 P0:r0=0;
 }
diff --git a/litmus/PTX/Nvidia/Proxy-Const-MP-cause2.litmus b/litmus/PTX/Nvidia/Proxy-Const-MP-cause2.litmus
index e086fd0a8c..cefbfb6f6d 100644
--- a/litmus/PTX/Nvidia/Proxy-Const-MP-cause2.litmus
+++ b/litmus/PTX/Nvidia/Proxy-Const-MP-cause2.litmus
@@ -3,7 +3,7 @@ PTX Proxy-Const-MP-cause2
 "The constant fence along the base causality path from the weak st to the cold, hence rf is guaranteed"
 {
 rd1 = 0;
-rd2 @ generic aliases rd1;
+rd2 @ constant aliases rd1;
 rd4 = 0;
 P1:r3=0;
 P1:r5=0;
diff --git a/litmus/PTX/Nvidia/Proxy-SingleThread-rf-surW-surF-conF-conR.litmus b/litmus/PTX/Nvidia/Proxy-SingleThread-rf-surW-surF-conF-conR.litmus
index f1fc67f8ae..80d05480df 100644
--- a/litmus/PTX/Nvidia/Proxy-SingleThread-rf-surW-surF-conF-conR.litmus
+++ b/litmus/PTX/Nvidia/Proxy-SingleThread-rf-surW-surF-conF-conR.litmus
@@ -3,7 +3,7 @@ PTX Proxy-SingleThread-rf-surW-surF-conF-conR
 "The generic memory is synchronize with surface cache by surface fence, then constant fence synchronize the data from generic memory to constant cache. Hence the cold is guaranteed to rf sust"
 {
 rd1 = 0;
-rd2 @ generic aliases rd1;
+rd2 @ constant aliases rd1;
 rd3 @ surface aliases rd1;
 P0:r0=0;
 }