Open
Description
Having identified that one access cannot race (by analysing its "check" program), can we eliminate all of its logs in the other "check" programs?
Related, we could do a run with all access checks disabled to see which generated invariants are even removed in that context. Then, for any subsequent run with some (or all) access checks enabled, we could then omit speculating those removed invariants.
Activity