We invite the reviewers to consider the difference between our submissions to ESOP 2013 and TACAS 2013:
Partial Orders for Efficient BMC of Concurrent Software
This paper presents a new BMC encoding for concurrent systems based on partial orders. It outperforms competing SC model checkers, and in addition supports all weak memory models of our framework. No program instrumentation is used.
Software Verification for Weak Memory via Program Transformation
This paper presents a new instrumentation method for encoding weak memory semantics into SC. It outperforms previous encodings of this kind for TSO, and in addition is the first instrumentation for the complex Power model. The paper features a detailed description of the PostgreSQL bug on Power.