diff --git a/README.markdown b/README.markdown
index 90900ee..d731a00 100644
--- a/README.markdown
+++ b/README.markdown
@@ -35,3 +35,7 @@ provided where non-paywalled ones are available.
 - [Empirical] *Concurrency Testing Using Schedule Bounding: an
   Empirical Study*, P. Thompson, A. Donaldson, and A. Betts (2014)
   http://www.doc.ic.ac.uk/~afd/homepages/papers/pdfs/2014/PPoPP.pdf
+
+- [RMMVerification] *On the Verification of Programs on Relaxed Memory
+  Models*, A. Linden (2014)
+  https://orbi.ulg.ac.be/bitstream/2268/158670/1/thesis.pdf
diff --git a/dejafu/Test/DejaFu/SCT/Internal.hs b/dejafu/Test/DejaFu/SCT/Internal.hs
index 9d91b3d..3ac2c46 100755
--- a/dejafu/Test/DejaFu/SCT/Internal.hs
+++ b/dejafu/Test/DejaFu/SCT/Internal.hs
@@ -333,6 +333,13 @@ dependentActions memtype buf a1 a2 = case (a1, a2) of
   (UnsynchronisedWrite r1, UnsynchronisedRead  r2) -> r1 == r2
   (UnsynchronisedWrite r1, UnsynchronisedWrite r2) -> r1 == r2
 
+  -- Unsynchronised writes and synchronisation where the buffer is not
+  -- empty.
+  --
+  -- See [RMMVerification], lemma 5.25.
+  (UnsynchronisedWrite r1, _) | same crefOf && isCommit a2 r1 && isBuffered buf r1 -> False
+  (_, UnsynchronisedWrite r2) | same crefOf && isCommit a1 r2 && isBuffered buf r2 -> False
+
   -- Unsynchronised reads where a memory barrier would flush a
   -- buffered write
   (UnsynchronisedRead r1, _) | isBarrier a2 -> isBuffered buf r1 && memtype /= SequentialConsistency