Ban tid_init

weakmemory · Jan 18, 2025 · 5952bd0 · 5952bd0
1 parent 41b43c9
commit 5952bd0
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/src/reordering/Reordering.v b/src/reordering/Reordering.v
@@ -72,6 +72,7 @@ Definition correct_mod_at : Prop :=
     )).
 
 Record correct_traces_t : Prop := {
+  prf_at_tid : tid a_t <> tid_init;
   prf_tid : tid b_t = tid a_t;
   prf_at_bt_neq : a_t <> b_t;
   prf_bt_at_imm : immediate ext_sb b_t a_t;