((OK_0_0_0_0_1_0_1_0 false)
 (tacTmpextcodesizeCheck$1 true)
 (tacExtcodesize$0 ((as const (Array Int Int)) 1))
 (OK_7_0_0_0_0_0_0_0 false)
 (B37@1$1 false)
 (R35@1$1 32)
 (tacCalldatasize@1$0 36)
 (B31@1$1 true)
 (R25@1$1 1696260665)
 (B28@1$1 false)
 (tacCalldatabuf!0@1$0 45731097061985477913277334465072951594518140566879712466277509855235947888678)
 (B9@1$1 false)
 (B7@1$1 true)
 (tacCallvalue@1$0 0)
 (B3@1$1 true)
 (R2@1$1 1)
 (tacAddress@1$0 0)
 (B1@1$1 true)
 (certoraTmpBool$1 true)
 (datasizeCheck$2 false)
 (tmpLastMsgSig$2 true)
 (certoraInput$4 1696260665)
 (datasizeCheck$1 false)
 (tmpLastMsgSig$1 true)
 (certoraInput$2 1696260665)
 (certoraInput$1 45731097061985477913277334465072951594518140566879712466277509855235947888640)
 (tacCalldatabuf@1$0 ((as const (Array Int Int))
  45731097061985477913277334465072951594518140566879712466277509855235947888640))
 (tacTmpBool$1 true)
 (ReachabilityCertora0_0_0_0_0_0_0_0$0 true)
 (ReachabilityCertora0_0_0_0_1_0_1_0$0 true)
 (ReachabilityCertora7_0_0_0_0_0_0_0$0 true)
 (OK_0_0_0_0_0_0_0_0 false)
 (certoraAndSmallPart11 1696260665)
 (certoraAndSmallPart22 1696260665)
 (true true)
 ((= #b00000 (_ bv0 5)) true)
)
