diff --git a/herd/AArch64ASLSem.ml b/herd/AArch64ASLSem.ml
index 07d51c2549..195e9b7940 100644
--- a/herd/AArch64ASLSem.ml
+++ b/herd/AArch64ASLSem.ml
@@ -87,6 +87,7 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) :
 
   module Mixed (SZ : ByteSize.S) : sig
     val build_semantics : test -> A.inst_instance_id -> (proc * branch) M.t
+    val can_unset_af_loc : event -> V.v option
     val spurious_setaf : V.v -> unit M.t
   end = struct
     module AArch64Mixed = AArch64S.Mixed (SZ)
@@ -1392,36 +1393,7 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) :
 
       let tr_cnstrnts cs = List.fold_left tr_cnstrnt [] cs
 
-
-      let dirty =
-        match TopConf.dirty with
-        | None -> DirtyBit.soft
-        | Some d -> d
-
-      let check_spurious ii =
-        (*
-         * Explicit loads or stores yield a potential spurious update of
-         * the AF flag. When the hardware feature is active, of course.
-         *)
-        if dirty.DirtyBit.ha ii.A.proc then
-          let dir_ok =
-            let open Dir in
-            if TopConf.C.variant Variant.PhantomOnLoad then
-              (function R -> true | W -> false)
-            else
-              (function W -> true | R -> false) in
-          fun act ->
-            match act with
-            | Act.Access
-                (dir,A.Location_global loc,_,_,
-                 AArch64Explicit.Exp,_,Access.(PHY_PTE|PTE DISide.Data))
-              when dir_ok dir
-              ->
-                Some loc
-            | _ -> None
-        else  fun _ -> None
-
-      let event_to_monad ii check_spurious is_bcc get_port event =
+      let event_to_monad ii is_bcc get_port event =
         let { ASLE.action; ASLE.iiid; _ } = event in
         let () =
           if _dbg then
@@ -1446,8 +1418,7 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) :
               |> M.as_port (get_port event)
               |> M.force_once
             in
-            let check_af = check_spurious action' in
-            Some (event, (check_af,m))
+            Some (event,m)
 
       let rel_to_monad event_to_monad_map comb rel =
         let one_pair (e1, e2) =
@@ -1497,17 +1468,10 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) :
           fun e -> ASLE.EventSet.mem e bcc in
         let () = if _dbg then Printf.eprintf "\t- events: " in
         let event_list = List.of_seq events in
-        let check_spurious = check_spurious ii in
-        let spurious_locs,event_to_monad_map =
+        let event_to_monad_map =
           let seq =
-            Seq.filter_map (event_to_monad ii check_spurious is_bcc get_port) events in
-          let locs =
-            Seq.filter_map (fun (_,(loc,_))  -> loc) seq
-            |> List.of_seq
-          and map =
-            Seq.map (fun (e,(_,m)) -> (e,m)) seq
-            |> EMap.of_seq in
-          locs,map
+            Seq.filter_map (event_to_monad ii is_bcc get_port) events in
+          EMap.of_seq seq
         in
         let events_m =
           let folder _e1 m1 acc = m1 ||| acc in
@@ -1604,18 +1568,8 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) :
           M.restrict (tr_cnstrnts cs)
         in
         let () = if _dbg then Printf.eprintf "\n" in
-        let m_spurious =
-          (*
-           * At most one spurious setaf operation per relevant location
-           * is probably sufficient. Anyway, it is unlikely that a given
-           * value appears more than once in the spurious_locs list.
-           *)
-          List.fold_left
-            (fun m loc ->
-               M.altT (AArch64Mixed.spurious_setaf loc) (M.unitT ()) ||| m)
-            (M.unitT ()) @@ List.sort_uniq A.V.compare spurious_locs in
         let* () =
-          m_spurious ||| events_m ||| iico_data ||| iico_ctrl
+          events_m ||| iico_data ||| iico_ctrl
           ||| iico_order ||| constraints ||| M.restrict eqs_test
         in
         M.addT (A.next_po_index ii.A.program_order_index) (return branch)
@@ -1777,6 +1731,7 @@ module Make (TopConf : AArch64Sig.Config) (V : Value.AArch64ASL) :
           AArch64Mixed.build_semantics test ii
       | _ -> asl_build_semantics test ii
 
+    let can_unset_af_loc e = AArch64Mixed.can_unset_af_loc e
     let spurious_setaf v = AArch64Mixed.spurious_setaf v
   end
 end
diff --git a/herd/AArch64Sem.ml b/herd/AArch64Sem.ml
index c89f7c4710..f1183ed519 100644
--- a/herd/AArch64Sem.ml
+++ b/herd/AArch64Sem.ml
@@ -105,6 +105,7 @@ module Make
     (* Semantics proper *)
     module Mixed(SZ:ByteSize.S) : sig
       val build_semantics : test -> A.inst_instance_id -> (proc * branch) M.t
+      val can_unset_af_loc : event -> V.v option
       val spurious_setaf : V.v -> unit M.t
     end = struct
 
@@ -1120,14 +1121,15 @@ module Make
               check_cond cond)
           end in
         if pte2 then  mvirt
-        else
-          M.op1 Op.IsVirtual a_virt >>= fun cond ->
-          M.choiceT cond mvirt
+        else begin
+          let mdirect =
             (* Non-virtual accesses are disallowed from EL0.
                For instance, user code cannot access the page table. *)
-            (if is_el0 then mk_pte_fault a_virt ma dir an ii domain
-             else mdirect)
-
+            if is_el0 then mk_pte_fault a_virt ma dir an ii domain
+            else mdirect in
+          M.op1 Op.IsVirtual a_virt >>= fun cond ->
+          M.choiceT cond mvirt mdirect
+        end
 (* Read memory, return value read *)
       let do_read_mem_ret sz an anexp ac a ii =
         let m a =
@@ -1444,25 +1446,22 @@ module Make
 
 (* KVM mode *)
 
-      let some_ha = dirty.DirtyBit.some_ha || dirty.DirtyBit.some_hd
+      let can_be_pt v =
+        match V.as_constant v with
+        | None -> true
+        | Some c -> Constant.is_pt c
 
-      let fire_spurious_af dir a m domain =
-        if
-          some_ha &&
-            (let v = C.variant Variant.PhantomOnLoad in
-             match dir with Dir.W -> not v | Dir.R -> v)
-        then
-          (m >>|
-             M.altT (test_and_set_af_succeeds a E.IdSpurious domain) (M.unitT ())) >>=
-            fun (r,_) -> M.unitT r
-        else m
+      let can_af0 v =
+        (match V.as_constant v with
+        | Some (Constant.PteVal p) ->
+           p.AArch64PteVal.valid <> 0 &&  p.AArch64PteVal.af = 0
+        | _ -> true)
 
-      let lift_kvm dir updatedb mop ma an ii mphy branch domain =
+      let lift_kvm _tag dir updatedb mop ma an ii mphy branch domain =
         let mfault ma a ft = emit_fault a ma dir an ft None ii in
         let maccess a ma =
           check_ptw ii.AArch64.proc dir updatedb false a ma an ii
-            ((let m = mop (Access.PTE domain) ma in
-              fire_spurious_af dir a m domain) |> branch)
+            (mop (Access.PTE domain) ma |> branch)
             mphy
             mfault
             domain in
@@ -1515,8 +1514,7 @@ module Make
           (* tag checks only apply to data *)
           let domain = DISide.Data in
           let mdirect =
-            let m = mop (Access.PTE domain) ma in
-            fire_spurious_af dir a m domain >>= M.ignore >>= B.next1T in
+            mop (Access.PTE domain) ma >>= M.ignore >>= B.next1T in
           check_ptw ii.AArch64.proc Dir.R false true a ma an ii
             mdirect
             cond_check_tag
@@ -1617,7 +1615,7 @@ Arguments:
               when translating for instruction fetches.
 - domain:     Whether the translation is for data or instruction access.
 *)
-      let do_lift_memop rA (* Base address register *)
+      let do_lift_memop ?tag rA (* Base address register *)
             dir updatedb checked mop perms ma mv an ii branch domain =
         if morello then
           lift_morello mop perms ma mv dir an ii branch
@@ -1630,15 +1628,15 @@ Arguments:
                 M.op1 Op.IsVirtual a_virt >>= fun c ->
                 M.choiceT c
                   (mop Access.PHY ma)
-                  (fire_spurious_af dir a_virt (mop Access.PHY_PTE ma) domain) |> branch
+                  (mop Access.PHY_PTE ma)
+                |> branch
               else
-                mop Access.PHY ma
-                |> branch in
+                mop Access.PHY ma |> branch in
             let mphy =
               if checked then lift_memtag_phy dir mop ma an ii mphy
               else mphy
             in
-            let m = lift_kvm dir updatedb mop ma an ii mphy branch domain in
+            let m = lift_kvm tag dir updatedb mop ma an ii mphy branch domain in
             (* M.short will add an iico_data only if memtag is enabled *)
             M.short (is_this_reg rA) (E.is_pred_txt (Some "color")) m
           else if pac then
@@ -1648,10 +1646,10 @@ Arguments:
           else
             mop Access.VIR ma |> branch
 
-      let lift_memop rA (* Base address register *)
+      let lift_memop ?(tag = "") rA (* Base address register *)
             dir updatedb checked mop perms ma mv an ii =
         let domain = DISide.Data in
-        do_lift_memop rA dir updatedb checked mop perms ma mv an ii
+        do_lift_memop ~tag rA dir updatedb checked mop perms ma mv an ii
           (fun a -> a >>= M.ignore >>= B.next1T) domain
 
       (* Address translation instruction *)
@@ -1679,8 +1677,7 @@ Arguments:
         let domain = DISide.Data in
         let maccess a ma =
           check_ptw ii.AArch64.proc dir false false a ma Annot.N ii
-            ((let m = mop (Access.PTE domain) ma in
-              fire_spurious_af dir a m domain) >>= M.ignore >>= B.next1T)
+            (mop (Access.PTE domain) ma >>= M.ignore >>= B.next1T)
             mphy
             mfault
             domain in
@@ -1694,7 +1691,7 @@ Arguments:
           if memtag && C.mte_store_only then
             ma >>= fun a -> loc_extract a
           else ma in
-        lift_memop rA Dir.R false checked
+        lift_memop ~tag:"LD" rA Dir.R false checked
           (fun ac ma _mv -> (* value fake here *)
             let open Precision in
             let memtag_sync =
@@ -1709,7 +1706,7 @@ Arguments:
 
 (* Generic store *)
       let do_str rA mop sz an ma mv ii =
-        lift_memop rA Dir.W true memtag
+        lift_memop ~tag:"ST" rA Dir.W true memtag
           (fun ac ma mv ->
             let open Precision in
             let memtag_sync = memtag && C.mte_precision = Synchronous in
@@ -1994,12 +1991,12 @@ Arguments:
 
       let str_simple sz rs rd m_ea ii =
         do_str rd
-          (fun ac a _ ii ->
-               M.data_input_next
-                 (read_reg_data_sz sz rs ii)
-                 (fun v -> do_write_mem sz Annot.N aexp ac a v ii))
+          (fun ac a v ii ->
+            M.data_input_next
+              (M.unitT v)
+              (fun v -> do_write_mem sz Annot.N aexp ac a v ii))
           sz Annot.N
-          m_ea  (M.unitT V.zero) ii
+          m_ea (read_reg_data_sz sz rs ii) ii
 
       let str sz rs rd e ii =
         let open AArch64Base in
@@ -2013,14 +2010,14 @@ Arguments:
                (read_reg_addr rd ii)
                (fun a_virt ma ->
                  do_str rd
-                   (fun ac a _ ii ->
+                   (fun ac a v ii ->
                      M.add a_virt (V.intToV k) >>= fun b -> write_reg rd b ii
                      >>|
                      M.data_input_next
-                       (read_reg_data_sz sz rs ii)
+                       (M.unitT v)
                        (fun v -> do_write_mem sz Annot.N aexp ac a v ii))
                    sz Annot.N
-                   ma (M.unitT V.zero) ii) in
+                   ma (read_reg_data_sz sz rs ii) ii) in
            if kvm then M.upOneRW (is_this_reg rd) m
            else m
         | Imm (k,PreIdx) ->
@@ -2117,9 +2114,9 @@ Arguments:
               (write_reg ResAddr V.zero ii)
               (fun v -> write_reg rr v ii)
               (mw an ac))
-              (to_perms "w" sz)
-              (read_reg_addr rd ii)
-              ms an ii
+          (to_perms "w" sz)
+          (read_reg_addr rd ii)
+          ms an ii
 
       let stxr sz t rr rs rd ii =
         do_stxr
@@ -2193,7 +2190,7 @@ Arguments:
               (* Dir.W would force check for dbm bit:                  *)
               (* - if set then either update or not db bit per R_TXGHB *)
               (* - if unset raise Permission fault                     *)
-              lift_memop rn Dir.W updatedb checked mop (to_perms "rw" sz) ma mv an ii
+              lift_memop ~tag:"FAIL" rn Dir.W updatedb checked mop (to_perms "rw" sz) ma mv an ii
           in
           if do_wb then
             do_action true checked ma
@@ -2234,7 +2231,7 @@ Arguments:
         M.altT (
           (* CAS succeeds and generates an Explicit Write Effect *)
           (* there must be an update to the dirty bit of the TTD *)
-          lift_memop rn Dir.W true memtag mop_success (to_perms "rw" sz) ma mv an ii
+          lift_memop ~tag:"CAS" rn Dir.W true memtag mop_success (to_perms "rw" sz) ma mv an ii
         )( (* CAS fails *)
           M.altT (
             (* CAS generates an Explicit Write Effect              *)
@@ -4881,6 +4878,19 @@ Arguments:
             else do_build_semantics test ii.A.inst ii
           end
 
+      let can_unset_af_loc e =
+        match E.access_of e with
+        | Some Access.(PTE _|PHY_PTE)
+          ->
+            begin
+              match E.location_of e,E.written_of e with
+              | Some (A.Location_global loc),Some v ->
+                  if E.is_explicit e && can_be_pt loc && can_af0 v then Some loc
+                  else None
+              | _ -> None
+            end
+        | _ -> None
+
       let spurious_setaf v =
         test_and_set_af_succeeds v E.IdSpurious DISide.Data
 
diff --git a/herd/ARMSem.ml b/herd/ARMSem.ml
index d3158c7510..a060f50f5c 100644
--- a/herd/ARMSem.ml
+++ b/herd/ARMSem.ml
@@ -514,7 +514,7 @@ module
 
           end
 
-      let spurious_setaf _ = assert false
+      include NoAF
 
     end
 
diff --git a/herd/ASLAction.ml b/herd/ASLAction.ml
index ba42bedad1..93c9d8fa4e 100644
--- a/herd/ASLAction.ml
+++ b/herd/ASLAction.ml
@@ -112,6 +112,10 @@ module Make (C: Config) (A : S) = struct
   (**************************************)
   (* Access to sub_components of events *)
   (**************************************)
+  let access_of = function
+    | Access (_,_,_,_,(_,_,a)) -> Some a
+    | Fault _|Barrier _|Branching _|CutOff _|NoAction
+      -> None
 
   let value_of =
     function
diff --git a/herd/ASLSem.ml b/herd/ASLSem.ml
index ebdd821424..c929664089 100644
--- a/herd/ASLSem.ml
+++ b/herd/ASLSem.ml
@@ -152,6 +152,7 @@ module Make (Conf : Config) = struct
   let atomic_pair_allowed _ _ = true
   module Mixed (SZ : ByteSize.S) : sig
     val build_semantics : test -> A.inst_instance_id -> (proc * branch) M.t
+    val can_unset_af_loc : event -> A.V.v option
     val spurious_setaf : A.V.v -> unit M.t
   end = struct
     module Mixed = M.Mixed (SZ)
@@ -931,6 +932,7 @@ module Make (Conf : Config) = struct
       assert (V.equal i V.zero);
       M.addT !(snd ii_env) B.nextT
 
-    let spurious_setaf _ = assert false
+    include NoAF
+
   end
 end
diff --git a/herd/BPFSem.ml b/herd/BPFSem.ml
index 43ba06148b..b5105246a6 100644
--- a/herd/BPFSem.ml
+++ b/herd/BPFSem.ml
@@ -246,6 +246,7 @@ struct
            >>= fun v -> commit ii >>= fun () -> B.bccT v lbl)
     ;;
 
-    let spurious_setaf _ = assert false
+    include NoAF
+
   end
 end
diff --git a/herd/BellAction.ml b/herd/BellAction.ml
index 5d7afd26c6..64a3524ac0 100644
--- a/herd/BellAction.ml
+++ b/herd/BellAction.ml
@@ -81,6 +81,9 @@ end = struct
   | CutOff msg -> "CutOff:" ^ msg
 
 (* Utility functions to pick out components *)
+
+  let access_of _ = None
+
   let value_of a = match a with
   | Access (_,_ ,v,_,_,_) -> Some v
   | _ -> None
diff --git a/herd/BellSem.ml b/herd/BellSem.ml
index 390f79c262..d2f0b32b5b 100644
--- a/herd/BellSem.ml
+++ b/herd/BellSem.ml
@@ -186,6 +186,7 @@ module
 
         in
         M.addT (A.next_po_index ii.A.program_order_index) (build_semantics_inner ii)
-      let spurious_setaf _ = assert false
+      include NoAF
+
     end
   end
diff --git a/herd/CAction.ml b/herd/CAction.ml
index 1de67bc5d5..d5a06249d9 100644
--- a/herd/CAction.ml
+++ b/herd/CAction.ml
@@ -119,6 +119,8 @@ end = struct
 
 (* Utility functions to pick out components *)
 
+  let access_of _ = None
+
   let value_of a = match a with
   | Access (_,_ ,v,_,_,_)
   | SRCU (_,_,Some v)   -> Some v
diff --git a/herd/CSem.ml b/herd/CSem.ml
index e9d7df7091..34d714a6e4 100644
--- a/herd/CSem.ml
+++ b/herd/CSem.ml
@@ -510,7 +510,7 @@ module
           build_semantics test ii >>> fun (prog_order, _branch) ->
             build_semantics_list test insts {ii with  A.program_order_index = prog_order;}
 
-      let spurious_setaf _ = assert false
+      include NoAF
 
     end
   end
diff --git a/herd/JavaAction.ml b/herd/JavaAction.ml
index cb38716331..9455dfe9db 100644
--- a/herd/JavaAction.ml
+++ b/herd/JavaAction.ml
@@ -133,6 +133,8 @@ end = struct
     -> true
   | _ -> false
 
+  let access_of _ = None
+
   let value_of a = match a with
   | Access (_,_,v,_,_) -> Some v
   | _ -> None
diff --git a/herd/JavaSem.ml b/herd/JavaSem.ml
index 2fe49263b6..5d86378390 100644
--- a/herd/JavaSem.ml
+++ b/herd/JavaSem.ml
@@ -163,7 +163,7 @@ module
             (build_semantics test ii) >>> fun (prog_order, _branch) ->
                 build_semantics_list test tl {ii with A.program_order_index = prog_order;}
 
-    let spurious_setaf _ = assert false
+    include NoAF
 
-    end
+  end
 end
diff --git a/herd/MIPSSem.ml b/herd/MIPSSem.ml
index a4487b5d79..d4fa89ad0c 100644
--- a/herd/MIPSSem.ml
+++ b/herd/MIPSSem.ml
@@ -265,7 +265,7 @@ module
               create_barrier MIPS.Sync ii >>= B.next1T
           end
 
-      let spurious_setaf _ = assert false
+      include NoAF
 
     end
   end
diff --git a/herd/PPCSem.ml b/herd/PPCSem.ml
index a930d69cd7..5493b8d2a5 100644
--- a/herd/PPCSem.ml
+++ b/herd/PPCSem.ml
@@ -481,7 +481,7 @@ module
                 (PPC.dump_instruction ii.A.inst)
           end
 
-      let spurious_setaf _ = assert false
+      include NoAF
 
     end
   end
diff --git a/herd/RISCVSem.ml b/herd/RISCVSem.ml
index 9ede236524..403843cc72 100644
--- a/herd/RISCVSem.ml
+++ b/herd/RISCVSem.ml
@@ -384,7 +384,7 @@ module
           | ins -> Warn.fatal "RISCV, instruction '%s' not handled" (RISCV.dump_instruction ins)
           end
 
-      let spurious_setaf _ = assert false
+      include NoAF
 
     end
 
diff --git a/herd/X86Sem.ml b/herd/X86Sem.ml
index e4ed140a74..cc341c190e 100644
--- a/herd/X86Sem.ml
+++ b/herd/X86Sem.ml
@@ -310,7 +310,7 @@ module
           (A.next_po_index ii.A.program_order_index)
           (build_semantics_inner false ii)
 
-      let spurious_setaf _ = assert false
+      include NoAF
 
     end
   end
diff --git a/herd/X86_64Arch_herd.ml b/herd/X86_64Arch_herd.ml
index 8f24dc2213..4a26002257 100644
--- a/herd/X86_64Arch_herd.ml
+++ b/herd/X86_64Arch_herd.ml
@@ -142,6 +142,7 @@ module Make (C:Arch_herd.Config)(V:Value.S) =
 
       let get_lannot _ = Plain
       let get_explicit _ = exp_annot
+      let access_of _ = None
       let value_of _ = None
       let read_of _ = None
       let written_of _ = None
diff --git a/herd/X86_64Sem.ml b/herd/X86_64Sem.ml
index 39bbf15dbb..7a7ab41b7a 100644
--- a/herd/X86_64Sem.ml
+++ b/herd/X86_64Sem.ml
@@ -431,7 +431,7 @@ module
           (A.next_po_index ii.A.program_order_index)
           (build_semantics_inner plain ii)
 
-    let spurious_setaf _ = assert false
+    include NoAF
 
     end
 
diff --git a/herd/action.mli b/herd/action.mli
index bdf7fbb0a2..9b68763d5d 100644
--- a/herd/action.mli
+++ b/herd/action.mli
@@ -39,7 +39,7 @@ module type S = sig
 (**************************************)
 (* Access to sub_components of events *)
 (**************************************)
-
+  val access_of : action -> Access.t option
   val value_of : action -> A.V.v option
   val read_of : action -> A.V.v option
   val written_of : action -> A.V.v option
diff --git a/herd/archAction.ml b/herd/archAction.ml
index 2d4e1ef1d5..76117b10bf 100644
--- a/herd/archAction.ml
+++ b/herd/archAction.ml
@@ -29,6 +29,7 @@ module type S = sig
 
   val get_lannot : t -> arch_lannot
   val get_explicit : t ->  arch_explicit
+  val access_of : t -> Access.t option
   val value_of : t -> v option
   val read_of : t -> v option
   val written_of : t -> v option
@@ -64,9 +65,10 @@ module No(C:NoConf) = struct
 
   let get_lannot _ = assert false
   let get_explicit _ = assert false
+  let access_of _ = assert false
+  let value_of _ = assert false
   let read_of _ = assert false
   let written_of _ = assert false
-  let value_of _ = assert false
   let location_of _ = assert false
   let is_store _ = assert false
   let is_load _ = assert false
diff --git a/herd/event.ml b/herd/event.ml
index 2dc79b8e78..37e549a236 100644
--- a/herd/event.ml
+++ b/herd/event.ml
@@ -279,6 +279,7 @@ val same_instance : event -> event -> bool
 (*************************************)
 (* Access to sub_components of events *)
 (*************************************)
+  val access_of : event -> Access.t option
   val value_of : event -> A.V.v option (* Warning: fails on RMW actions *)
   val read_of : event -> A.V.v option
   val written_of : event -> A.V.v option
@@ -314,6 +315,10 @@ val same_instance : event -> event -> bool
   val inst_code_comp_spec :
      event_structure -> event_structure -> event_structure -> event_structure
 
+(******************)
+(* Standard union *)
+(******************)
+  val union_comp : event_structure -> event_structure -> event_structure
 
 (************************)
 (* Parallel composition *)
@@ -578,6 +583,7 @@ module Make  (C:Config) (AI:Arch_herd.S) (Act:Action.S with module A = AI) :
         "(eeid=%s action=%s)" (pp_eiid e) (pp_action e)
 
 (* Utility functions to pick out components *)
+    let access_of e = Act.access_of e.action
     let value_of e = Act.value_of e.action
     let read_of e = Act.read_of e.action
     let written_of e = Act.written_of e.action
@@ -1320,6 +1326,7 @@ module Make  (C:Config) (AI:Arch_herd.S) (Act:Action.S with module A = AI) :
         fun es _ -> es.speculated
 
 (* Standard union of two structures, specific fields to be completed *)
+
     let union es1 es2 =
       { procs = [];
         events = EventSet.union es1.events es2.events ;
@@ -1351,6 +1358,8 @@ module Make  (C:Config) (AI:Arch_herd.S) (Act:Action.S with module A = AI) :
        aligned = es1.aligned @ es2.aligned ;
       }
 
+    let union_comp es1 es2 = union es1 es2
+
 (* Parallel composition *)
 
     let do_para_comp es1 es2 =
diff --git a/herd/eventsMonad.ml b/herd/eventsMonad.ml
index 63d8237f5a..2657b00623 100644
--- a/herd/eventsMonad.ml
+++ b/herd/eventsMonad.ml
@@ -193,13 +193,10 @@ Monad type:
                     eprintf "Delay %s output is %a\n" tag E.debug_output es
                   end ;
                let delayed : 'a t =
-                  fun eiid -> eiid,(Evt.singleton (v,[],es),None) in
+                  fun eiid -> eiid,(Evt.singleton (v,cls,es),None) in
                 let eiid,(acts2,specs) = kont v delayed eiid in
                 assert (specs=None) ;
-                let acts =
-                  Evt.fold
-                    (fun (v,cls2,es) acts -> Evt.add (v,cls@cls2,es) acts)
-                    acts2 acts in
+                let acts = Evt.union acts acts2 in
                 eiid,acts)
               acts (eiid,Evt.empty) in
           eiid,(acts,None)
@@ -1730,11 +1727,25 @@ Monad type:
     type evt_struct = E.event_structure
     type output = VC.cnstrnts * evt_struct
 
-    let get_output et k =
-      let (_,(es,_)) = et (0,0) in
+    let get_output_check check et k =
+      let ((_,eiid),(es,_)) = et (0,0) in
       List.fold_left
-        (fun k (_,vcl,evts) -> (vcl,evts)::k)
-        k (Evt.elements es)
+        (fun (eiid,k) (_,vcl,evts) ->
+           let m = check (vcl,evts) in
+           let eiid,(acts,_) = m eiid in
+           let k =
+             Evt.fold
+               (fun (_,cls0,es0) k ->
+                  let evts = E.union_comp es0 evts
+                  and vcl = cls0@vcl in
+                  (vcl,evts)::k)
+               acts k in
+           eiid,k)
+        ({ id=eiid; sub=0; },k)
+        (Evt.elements es)
+      |> snd
+
+    let get_output et k = get_output_check (fun _ -> unitT ()) et k
 
     let force_once (m : 'a t) : 'a t =
       let res = ref None in
diff --git a/herd/machAction.ml b/herd/machAction.ml
index 35ddac65c4..66465e2b42 100644
--- a/herd/machAction.ml
+++ b/herd/machAction.ml
@@ -185,6 +185,13 @@ end = struct
   | Arch a -> A.ArchAction.pp a
 
 (* Utility functions to pick out components *)
+  let access_of = function
+    | Access (_,_,_,_,_,_,ac) -> Some ac
+    | Barrier _|Commit _|Amo _|Fault _
+    | CutOff _|Inv _|CMO _|NoAction
+      -> None
+    | Arch a -> A.ArchAction.access_of a
+
   let value_of a = match a with
   | Access (_,_ , v,_,_,_,_)
     -> Some v
diff --git a/herd/mem.ml b/herd/mem.ml
index 4bfbba91c5..61772d728d 100644
--- a/herd/mem.ml
+++ b/herd/mem.ml
@@ -778,32 +778,78 @@ module Make(C:Config) (S:Sem.Semantics) : S with module S = S	=
         let r,e = es.E.po in
         (r,E.EventRel.transitive_closure e) in
 
-      let af0 = (* locations with initial spurious update *)
+      let add_setaf =
         if
           match C.dirty with
           | None -> false
           | Some t -> t.DirtyBit.some_ha || t.DirtyBit.some_hd
-        then begin (* One spurious update per observed pte (final load) *)
-            if C.variant Variant.PhantomOnLoad then
-              let look_pt rloc k = match rloc with
-                | ConstrGen.Loc (A.Location_global (V.Val c as vloc))
-                when Constant.is_pt c -> vloc::k
-                | _ -> k in
-              A.RLocSet.fold look_pt test.Test_herd.observed []
-            else (* One spurious update per variable not accessed initially *)
-              let add_setaf0 k (loc,v) =
-                match loc with
-                | A.Location_global (V.Val c as vloc) ->
-                   if Constant.is_pt c then
-                     match v with
-                     | V.Val (Constant.PteVal p)
-                           when not (V.Cst.PteVal.is_af p) ->
-                        vloc::k
-                     | _ -> k
-                   else k
-                | _ -> k in
-              List.fold_left add_setaf0 [] env0
-        end else [] in
+        then
+          fun (_,es) ->
+            let evts = E.EventSet.filter E.is_mem es.E.events in
+            let inv_iico_data_atomics =
+              lazy begin
+                  let atms =
+                    E.EventSet.filter E.is_atomic evts in
+                  E.EventRel.restrict_domains_to_sets
+                    atms atms es.E.intra_causality_data
+                  |> E.EventRel.inverse
+              end in
+            let locs =
+              E.EventSet.fold
+                (fun e k ->
+                   match SM.can_unset_af_loc e with
+                   | None -> k
+                   | Some loc ->
+                       let v = Misc.as_some @@ E.written_of e in
+                       if dbg then
+                         Printf.eprintf
+                           "loc=%s,v=%s\n%!" (V.pp_v loc) (V.pp_v v) ;
+                       let write_loaded =
+                         (* Special case where the value stored
+                          * has just been read. In such a case,
+                          * no supplementary HW update is necessary.
+                          *)
+                         E.is_atomic e &&
+                           begin
+                             try
+                               E.EventRel.succs
+                                 (Lazy.force inv_iico_data_atomics) e
+                               |>
+                               E.EventSet.exists
+                                 (fun er ->
+                                   assert (E.is_load er);
+                                   match
+                                     E.global_loc_of er,
+                                     E.read_of er
+                                   with
+                                   | Some loc_r,Some v_r
+                                     ->
+                                      V.equal loc loc_r && V.equal v v_r
+                                   | _,_ -> false)
+                             with Not_found -> false
+                           end in
+                       if write_loaded then k else loc::k)
+                evts []
+              |> Misc.group V.compare in
+            let om =
+              Misc.fold_suffix_cross_gen
+                (fun xs m ->
+                   List.fold_left
+                     (fun m x -> EM.(|||) (SM.spurious_setaf x) m)
+                     m xs)
+                (EM.unitT ())
+                locs
+                (fun m1 o2 ->
+                   (* Without this trick, the execution with
+                      no spurious update will present twice. *)
+                   match o2 with
+                   | None -> Some m1
+                   | Some m2 -> Some (EM.altT m1 m2))
+                None in
+            match om with
+            | None -> EM.unitT ()
+            | Some m -> m
+        else fun _ -> EM.unitT () in
 
       let rec index xs i = match xs with
       | [] ->
@@ -817,11 +863,9 @@ module Make(C:Config) (S:Sem.Semantics) : S with module S = S	=
             { es with E.procs = procs; E.po = if do_deps then transitive_po es else es.E.po } in
           (i,vcl,es)::index xs (i+1) in
       let r =
-        Misc.fold_subsets_gen
-          (fun vloc -> EM.(|||) (SM.spurious_setaf vloc))
-          (EM.unitT ()) af0
-          (fun maf0 ->
-            EM.get_output (set_of_all_instr_events (EM.(|||) maf0)))
+        EM.get_output_check
+          add_setaf
+          (set_of_all_instr_events (EM.(|||) (EM.unitT ())))
           [] in
       let r = match C.maxphantom with
         | None -> r
@@ -896,7 +940,7 @@ struct
       else ambiguous_po e1 e2
   end)
 
-  let find_last_before e set =
+  let find_last_before set e =
     find_last_opt (fun e' -> is_before_strict e' e) set
 
   let find_first_after e set =
@@ -927,7 +971,7 @@ let match_reg_events add_eq es csn =
       List.fold_left
         (fun k load ->
           let rf =
-            match StoreSet.find_last_before load stores with
+            match StoreSet.find_last_before stores load with
             | Some store -> S.Store store
             | None -> S.Init
           in
@@ -1988,7 +2032,7 @@ let get_rf_value test read =
             eprintf "Observed locs: {%s}\n" (pp_locations observed_locs)
           end ;
           U.LocEnv.filter
-            (fun loc _ ->  keep_observed_loc loc observed_locs)
+            (fun loc _ -> keep_observed_loc loc observed_locs)
             loc_stores
         else loc_stores in
 
diff --git a/herd/monad.mli b/herd/monad.mli
index 6621d75e8f..01003feeb3 100644
--- a/herd/monad.mli
+++ b/herd/monad.mli
@@ -52,7 +52,7 @@ module type S =
     val unitcodeT        : 'a -> 'a code
     val failcodeT        : exn -> 'a -> 'a code
     val warncodeT        : string -> 'a -> 'a code
-    val delay_kont : string -> 'a t -> ('a ->  'a t -> 'b t) -> 'b t
+    val delay_kont : string -> 'a t -> ('a -> 'a t -> 'b t) -> 'b t
     val delay : 'a t -> ('a * 'a t) t
 
     val set_standard_input_output : 'a t -> 'a t
@@ -372,8 +372,14 @@ module type S =
     type evt_struct
     type output = VC.cnstrnts * evt_struct
 
-    val get_output  : 'a code -> output list -> output list
+    (* Generic, i.e. apply transformation to output *)
+    val get_output_check :
+      (output -> unit t)
+      -> 'a code -> output list -> output list
 
+    val get_output :
+      'a code -> output list -> output list
     (* Force executed only once. *)
+
     val force_once : 'a t -> 'a t
   end
diff --git a/herd/noAF.ml b/herd/noAF.ml
new file mode 100644
index 0000000000..c29676fa9d
--- /dev/null
+++ b/herd/noAF.ml
@@ -0,0 +1,2 @@
+let can_unset_af_loc _ = None
+let spurious_setaf _ = assert false
diff --git a/herd/sem.mli b/herd/sem.mli
index 74e7b58c37..f2b6a1f001 100644
--- a/herd/sem.mli
+++ b/herd/sem.mli
@@ -31,6 +31,7 @@ module type Semantics =
     module Mixed(SZ:ByteSize.S) : sig
       val build_semantics :
         test -> A.inst_instance_id -> (A.program_order_index * branch) M.t
+      val can_unset_af_loc : event -> A.V.v option
       val spurious_setaf : A.V.v -> unit M.t
     end
   end
diff --git a/herd/tests/instructions/AArch64.kvm/A031.litmus.expected b/herd/tests/instructions/AArch64.kvm/A031.litmus.expected
index 4ee55fea03..a7087de97b 100644
--- a/herd/tests/instructions/AArch64.kvm/A031.litmus.expected
+++ b/herd/tests/instructions/AArch64.kvm/A031.litmus.expected
@@ -5,9 +5,9 @@ States 3
 1:X5=2; [PTE(z)]=(oa:PA(x));
 Ok
 Witnesses
-Positive: 14 Negative: 0
+Positive: 10 Negative: 0
 Flag requires-BBM
 Condition ~exists ([PTE(z)]=(oa:PA(x), af:0) /\ 1:X5=2)
-Observation A031 Never 0 14
+Observation A031 Never 0 10
 Hash=b49f887241d4043b0d917f97925e00ab
 
diff --git a/herd/tests/instructions/AArch64.kvm/A032.litmus b/herd/tests/instructions/AArch64.kvm/A032.litmus
new file mode 100644
index 0000000000..0dc5fc7071
--- /dev/null
+++ b/herd/tests/instructions/AArch64.kvm/A032.litmus
@@ -0,0 +1,14 @@
+AArch64 A032
+Variant=vmsa
+TTHM=HA
+(* Allowed, by two spurious HW updates *)
+{
+int x=1;
+int y=2;
+[PTE(x)]=(oa:PA(x),af:0);
+0:X0=PTE(x); 0:X1=(oa:PA(y),af:0);
+}
+  P0         ;
+ LDR X3,[X0] ;
+ STR X1,[X0] ;
+exists 0:X3=(oa:PA(x)) /\ [PTE(x)]=(oa:PA(y))
diff --git a/herd/tests/instructions/AArch64.kvm/A032.litmus.expected b/herd/tests/instructions/AArch64.kvm/A032.litmus.expected
new file mode 100644
index 0000000000..039bc5a97d
--- /dev/null
+++ b/herd/tests/instructions/AArch64.kvm/A032.litmus.expected
@@ -0,0 +1,13 @@
+Test A032 Allowed
+States 4
+0:X3=(oa:PA(x), af:0); [PTE(x)]=(oa:PA(y), af:0);
+0:X3=(oa:PA(x), af:0); [PTE(x)]=(oa:PA(y));
+0:X3=(oa:PA(x)); [PTE(x)]=(oa:PA(y), af:0);
+0:X3=(oa:PA(x)); [PTE(x)]=(oa:PA(y));
+Ok
+Witnesses
+Positive: 2 Negative: 6
+Condition exists (0:X3=(oa:PA(x)) /\ [PTE(x)]=(oa:PA(y)))
+Observation A032 Sometimes 2 6
+Hash=4d4ebbbbd741d64b8bb4bcece91ef26d
+
diff --git a/herd/tests/instructions/AArch64.kvm/A033.litmus b/herd/tests/instructions/AArch64.kvm/A033.litmus
new file mode 100644
index 0000000000..bfa3b61089
--- /dev/null
+++ b/herd/tests/instructions/AArch64.kvm/A033.litmus
@@ -0,0 +1,14 @@
+AArch64 A033
+Variant=vmsa
+TTHM=HA
+(* Only 4 exections, tests the "write_loaded" optimisation in herd/mem.ml *)
+{
+  [x]=1;
+  [PTE(x)]=(oa:PA(x),af:0);
+  0:X4=(oa:PA(x),af:0); 0:X5=PTE(x);
+  0:X6=(oa:PA(y));
+}
+ P0              ;
+ CAS X4,X6,[X5]  ;
+locations [PTE(x)]
+exists [PTE(x)]=(oa:PA(x));
diff --git a/herd/tests/instructions/AArch64.kvm/A033.litmus.expected b/herd/tests/instructions/AArch64.kvm/A033.litmus.expected
new file mode 100644
index 0000000000..1f8c1289c4
--- /dev/null
+++ b/herd/tests/instructions/AArch64.kvm/A033.litmus.expected
@@ -0,0 +1,11 @@
+Test A033 Allowed
+States 2
+[PTE(x)]=(oa:PA(x));
+[PTE(x)]=(oa:PA(y));
+Ok
+Witnesses
+Positive: 2 Negative: 2
+Condition exists ([PTE(x)]=(oa:PA(x)))
+Observation A033 Sometimes 2 2
+Hash=3ed88fecb82a1a11276fc0a9dff5afa6
+
diff --git a/herd/tests/instructions/AArch64.kvm/A034.litmus b/herd/tests/instructions/AArch64.kvm/A034.litmus
new file mode 100644
index 0000000000..3b6dc1f695
--- /dev/null
+++ b/herd/tests/instructions/AArch64.kvm/A034.litmus
@@ -0,0 +1,22 @@
+AArch64 A034
+Variant=vmsa
+TTHM=HA
+(*
+ * Test enhanced bounds on spurious HW updates,
+ * Should terminate in decent time.
+ *)
+{
+  [x]=1; [y]=2;
+  [PTE(x)]=(oa:PA(x));
+  0:X1=x; 1:X1=x;
+  1:X4=(oa:PA(x),af:0); 1:X5=PTE(x);
+  1:X6=(oa:PA(y));
+}
+  P0           | P1              ;
+  L1:          | STR X4,[X5]     ;
+   LDR W0,[X1] | DSB ISH         ;
+  L2:          | LSR X9,X1,#12   ;
+   LDR W2,[X1] | TLBI VAAE1IS,X9 ;
+               | DSB ISH         ;
+               | CAS X4,X6,[X5]  ;
+exists (0:X0=2 /\ 0:X2=1)
diff --git a/herd/tests/instructions/AArch64.kvm/A034.litmus.expected b/herd/tests/instructions/AArch64.kvm/A034.litmus.expected
new file mode 100644
index 0000000000..be31bad04a
--- /dev/null
+++ b/herd/tests/instructions/AArch64.kvm/A034.litmus.expected
@@ -0,0 +1,12 @@
+Test A034 Allowed
+States 3
+0:X0=1; 0:X2=1;
+0:X0=1; 0:X2=2;
+0:X0=2; 0:X2=2;
+No
+Witnesses
+Positive: 0 Negative: 70
+Condition exists (0:X0=2 /\ 0:X2=1)
+Observation A034 Never 0 70
+Hash=0a5d5dfceba07390c6252921dbe58a4f
+
diff --git a/herd/tests/instructions/AArch64.kvm/asl-vmsa.cfg b/herd/tests/instructions/AArch64.kvm/asl-vmsa.cfg
index 3dac0fead1..d628d668e7 100644
--- a/herd/tests/instructions/AArch64.kvm/asl-vmsa.cfg
+++ b/herd/tests/instructions/AArch64.kvm/asl-vmsa.cfg
@@ -17,3 +17,5 @@ nonames A006,F006,F007
 nonames A024,A025
 # Too long to run (copied to the catalogue)
 nonames A031
+# Too long to run
+nonames A034
diff --git a/herd/variant.ml b/herd/variant.ml
index 2287a00262..65d9a82bc7 100644
--- a/herd/variant.ml
+++ b/herd/variant.ml
@@ -70,8 +70,6 @@ type t =
   | NoPteBranch
 (* Pte-Squared: all accesses through page table, including PT accesses *)
   | PTE2
-(* Count maximal number of phantom updates by looking at loads *)
-  | PhantomOnLoad
 (* Optimise Rf enumeration leading to rmw *)
   | OptRfRMW
 (* Allow some constrained unpredictable, behaviours.
@@ -162,7 +160,6 @@ let (mode_variants, arch_variants) : t list * t list =
   | EOS -> EOS
   | NoPteBranch -> NoPteBranch
   | PTE2 -> PTE2
-  | PhantomOnLoad -> PhantomOnLoad
   | OptRfRMW -> OptRfRMW
   | ConstrainedUnpredictable -> ConstrainedUnpredictable
   | Exp -> Exp
@@ -200,7 +197,7 @@ let (mode_variants, arch_variants) : t list * t list =
         NotWeakPredicated;
         LKMMVersion `lkmmv1; LKMMVersion `lkmmv2;
         CutOff; Morello; Deps; Instances;
-        PhantomOnLoad; OptRfRMW; ConstrainedUnpredictable;
+        OptRfRMW; ConstrainedUnpredictable;
         Exp; CosOpt; Test; T 0;
         ASL; ASL_AArch64; ASLVersion `ASLv0; ASLVersion `ASLv1;
         S128; Strict; Warn;
@@ -265,7 +262,6 @@ let parse s = match Misc.lowercase s with
 | "eos" -> Some EOS
 | "noptebranch"|"nobranch" -> Some NoPteBranch
 | "pte2" | "pte-squared" -> Some PTE2
-| "phantomonload" -> Some PhantomOnLoad
 | "optrfrmw" -> Some OptRfRMW
 | "constrainedunpredictable"|"cu" -> Some ConstrainedUnpredictable
 | "exp" -> Some Exp
@@ -370,7 +366,6 @@ let pp = function
   | EOS -> "eos"
   | NoPteBranch -> "NoPteBranch"
   | PTE2 -> "pte-squared"
-  | PhantomOnLoad -> "PhantomOnLoad"
   | OptRfRMW -> "OptRfRMW"
   | ConstrainedUnpredictable -> "ConstrainedUnpredictable"
   | Exp -> "exp"
@@ -449,7 +444,6 @@ let pp = function
   | EOS -> "If FEAT_ExS is enabled, configure the effect of an Exception return, see SCTLR_ELx.EOS (AArch64 only)"
   | NoPteBranch -> "Disable branching events between PTE reads and accesses"
   | PTE2 -> "Perform a table walk for each memory access, including page tables"
-  | PhantomOnLoad -> ""
   | OptRfRMW -> ""
   | ConstrainedUnpredictable -> ""
   | Exp -> ""
diff --git a/herd/variant.mli b/herd/variant.mli
index 38e2714533..309a7e9ebc 100644
--- a/herd/variant.mli
+++ b/herd/variant.mli
@@ -68,8 +68,6 @@ type t =
   | NoPteBranch
 (* Pte-Squared: all accesses through page table, including PT accesses *)
   | PTE2
-(* Generate extra spurious updates based upon load on pte. *)
-  | PhantomOnLoad
 (* Optimise Rf enumeration leading to rmw *)
   | OptRfRMW
 (* Allow some constrained unpredictable, behaviours.
diff --git a/lib/misc.ml b/lib/misc.ml
index 7a3dda2f3d..309b234fee 100644
--- a/lib/misc.ml
+++ b/lib/misc.ml
@@ -325,11 +325,24 @@ let nsplit n xs =
   let yss = do_rec xs (replicate n []) in
   List.map List.rev yss
 
-let rec group same xs = match xs with
-| [] -> []
-| x::xs ->
-    let xx,xs = List.partition (same x) xs in
-    (x::xx)::group same xs
+let group_sorted eq =
+  let rec do_rec x0 xs = match xs with
+    | [] -> [x0],[]
+    | x::xs ->
+        if eq x0 x then
+          let xs,xss = do_rec x xs in
+          x0::xs,xss
+        else
+          let xs,xss = do_rec x xs in
+          [x0],xs::xss in
+  function
+  | [] -> []
+  | x::xs ->
+      let xs,xss = do_rec x xs in
+      xs::xss
+
+let group cmp xs =
+  List.sort cmp xs |> group_sorted (fun x y -> cmp x y = 0)
 
 let group_iter same do_it xs =
   let xss = group same xs in
@@ -618,6 +631,16 @@ and go dir line (chans,ns as st) =
     | None -> next_iter st
   else Some (fconcat dir line,st)
 
+(*******************)
+(* Suffix genrator *)
+(*******************)
+
+let fold_suffix xs kont r =
+  let rec fold_rec r = function
+    | [] -> kont [] r
+    | _::ys as xs -> fold_rec (kont xs r) ys in
+  fold_rec r xs
+
 (********************)
 (* Subset generator *)
 (********************)
@@ -642,18 +665,27 @@ let fold_subsets xs kont r =
 (* cross product iteration *)
 (***************************)
 
-let fold_cross_gen add start xss kont r =
+(* Uttra generic, internal use *)
+let fold_cross_gen2 fold add start xss kont r =
  let rec fold_rec r ys xss = match xss with
   | [] -> kont ys r
   | xs::xss ->
-      List.fold_left
+      fold
         (fun r x -> fold_rec r (add x ys) xss)
         r xs in
  fold_rec r start (List.rev xss)
 
+let fold_cross_gen add start xss kont r =
+  fold_cross_gen2 List.fold_left  add start xss kont r
 
 let fold_cross xss = fold_cross_gen cons [] xss
 
+let fold_suffix_cross_gen madd start xss kont r =
+  let fold f r xs = fold_suffix xs (fun xs r -> f r xs) r in
+  fold_cross_gen2 fold madd start xss kont r
+
+let fold_suffix_cross xss = fold_suffix_cross_gen cons [] xss
+
 (*******************)
 (* Simple bindings *)
 (*******************)
diff --git a/lib/misc.mli b/lib/misc.mli
index ab3538b686..342395bdca 100644
--- a/lib/misc.mli
+++ b/lib/misc.mli
@@ -161,10 +161,10 @@ val nsplit : int -> 'a list -> 'a list list
    WARNING, correct only when duplicates are in sequence *)
 val rem_dups : ('a -> 'a -> bool) -> 'a list -> 'a list
 
-(* group elements, quadratic *)
-val group : ('a -> 'a -> bool) -> 'a list -> 'a list list
-val group_iter : ('a -> 'a -> bool) -> ('a -> 'a list -> unit) -> 'a list -> unit
-val group_iteri : ('a -> 'a -> bool) -> (int -> 'a -> 'a list -> unit) -> 'a list -> unit
+(* group elements, efficient*)
+val group : ('a -> 'a -> int) -> 'a list -> 'a list list
+val group_iter : ('a -> 'a -> int) -> ('a -> 'a list -> unit) -> 'a list -> unit
+val group_iteri : ('a -> 'a -> int) -> (int -> 'a -> 'a list -> unit) -> 'a list -> unit
 
 (* Check that f yields the same result on all list elements *)
 val check_same : ('a -> 'a -> bool) -> ('b -> 'a) -> 'b list -> 'a option
@@ -285,6 +285,13 @@ val fold_cross :  'a list list ->  ('a list -> 'b -> 'b) -> 'b -> 'b
 val fold_cross_gen :
     ('a -> 'b -> 'b) -> 'b -> 'a list list -> ('b -> 'c -> 'c) -> 'c -> 'c
 
+(* Similar, except that suffixes are selected *)
+
+val fold_suffix_cross : 'a list list -> ('a list list -> 'b -> 'b) -> 'b -> 'b
+
+val fold_suffix_cross_gen :
+  ('a list -> 'c -> 'c) -> 'c -> 'a list list -> ('c -> 'b -> 'b) -> 'b -> 'b
+
 (*******************)
 (* Simple bindings *)
 (*******************)
diff --git a/litmus/skelUtil.ml b/litmus/skelUtil.ml
index 6c23eb015e..0c9e8e37c3 100644
--- a/litmus/skelUtil.ml
+++ b/litmus/skelUtil.ml
@@ -1128,7 +1128,7 @@ end
             is ;
             let lbl2instrs =
               Misc.group
-                (fun ((p1,_),_) ((p2,_),_) -> Proc.equal p1 p2)
+                (fun ((p1,_),_) ((p2,_),_) -> Proc.compare p1 p2)
                 lbl2instr in
             let open OutUtils in
             List.iter