diff --git a/src/correct_store_buffer.v b/src/correct_store_buffer.v
index 587d63b3579a6b92bc256b0da50e75c0a8859ab2..d337d3d24a008558a2eb3a83bb154552f1ebe447 100644
--- a/src/correct_store_buffer.v
+++ b/src/correct_store_buffer.v
@@ -14,14 +14,14 @@ Definition ready isSuUsed sbState (elt : instr_kind) :=
 Definition luFree isSuUsed sbState trace :=
   let instr := get_instr_in_stage trace Lu in
   match instr with
-  | Some elt => ready isSuUsed sbState elt
+  | Some elt => ready isSuUsed sbState elt (* Sn is always free *)
   | None => true
   end.
 
 Definition suFree isSuUsed sbState trace :=
   let instr := get_instr_in_stage trace Su in
   match instr with
-  | Some elt => ready isSuUsed sbState elt
+  | Some elt => ready isSuUsed sbState elt (* Sn is always free *)
   | None => true
   end.