diff --git a/src/correct_store_buffer.v b/src/correct_store_buffer.v
index 993249cd06b27009458572a83563de0a4985a496..587d63b3579a6b92bc256b0da50e75c0a8859ab2 100644
--- a/src/correct_store_buffer.v
+++ b/src/correct_store_buffer.v
@@ -5,10 +5,10 @@ Import ListNotations.
 (* free and cycle functions. *)
 Definition ready isSuUsed sbState (elt : instr_kind) :=
   match elt with
-  | (Load, (Lsu, 0)) => busFree isSuUsed sbState
-  | (_, (Su, 0)) => negb (sbStateT_beq sbState Full)
-  | (_, (_, 0)) => true
-  | _ => false
+  | (Load, (Lsu, _)) => busFree isSuUsed sbState
+  | (_, (Su, _)) => negb (sbStateT_beq sbState Full)
+  | (_, (Lu, S _)) => false
+  | _ => true
   end.
 
 Definition luFree isSuUsed sbState trace :=
@@ -28,7 +28,11 @@ Definition suFree isSuUsed sbState trace :=
 Definition lsuFree isSuUsed sbState trace :=
   let instr := get_instr_in_stage trace Lsu in
   match instr with
-  | Some elt => ready isSuUsed sbState elt
+  | Some (opcode, (stg, lat)) => ready isSuUsed sbState (opcode, (stg, lat)) &&
+                                  if stage_beq (nstg stg opcode) Lu then
+                                    luFree isSuUsed sbState trace
+                                  else
+                                    suFree isSuUsed sbState trace
   | None => true
   end.