For future values, we can enforce the following rule:
If X --hb-> Y --mo-> Z, then X should not read from Z.
This a change from previous behavior, where we used 'sb' instead of
'hb'.
Tested with linuxrwlocks example:
./run.sh test/linuxrwlocks.o -f 4 -m 1
No difference in number of executions (feasible or infeasible); HASH
values were exactly the same.