Trace_Based_Rely_Guarantee.RG_Soundness_Binary