Avoid write guard in supremum constraint

Instead, if a write event is guarded by an unsatisfiable condition,
then require that the write happens after the read.