diff --git a/herd/AArch64Sem.ml b/herd/AArch64Sem.ml index 1a54214b6..f064885c2 100644 --- a/herd/AArch64Sem.ml +++ b/herd/AArch64Sem.ml @@ -2323,7 +2323,7 @@ module Make else M.unitT old_val in repeat V.zero 0 >>= fun (new_val) -> - write_reg_predicate p new_val ii + write_reg_predicate p new_val ii >>! new_val let mov_sv r k shift ii = let open AArch64Base in @@ -3265,7 +3265,8 @@ module Make M.unitT ()) | I_PTRUE(p,pattern) -> check_sve inst; - !(ptrue p pattern ii) + ptrue p pattern ii + >>= nextSet p | I_WHILELT(p,var,r1,r2) -> check_sve inst; !!(while_op (M.op Op.Lt) false p var r1 r2 ii)