Invariants can be inserted into the contract under test itself (i.e., internal testing) or written in test functions that call into the contract under test from an external contract (i.e., external testing—for more detail see our introduction to common testing approaches). Function Comptroller._become(Unitroller) (*) Expression: require(bool,string)(msg.sender == unitroller.admin(),only admin can upgrade) IRs: TMP_50(address) = HIGH_LEVEL_CALL, dest:unitroller(Unitroller), function:admin, args:[] TMP_51(bool) = msg.sender == TMP_50 TMP_52(None) = SOLIDITY_CALL require(bool,string)(TMP_51,only admin can upgrade) Expression: require(bool,string)(unitroller._acceptImplementation() == 0,not authorized) IRs: TMP_53(uint256) = HIGH_LEVEL_CALL, dest:unitroller(Unitroller),…