There is an unsaved comment in progress. You will lose your changes if you continue. Are you sure you want to reopen the work item?
Inlining function with "return" statement causes QED runtime exception
TSO modelling code attached includes return statements in its read and readTID functions.
While inlining read and readTID functions which include return statement , QED runtime throws index out of range exception in call to CodeTransformation.ComputeStraightAtomicStmts.