(model
(define-fun OK_0_0_0_0_9_0_138_0 () Bool false)
(define-fun certoraTmpBool$12 () Bool true)
(define-fun tacS!ce4604a0000000000000000000000001!5!0$0 () Int 0)
(define-fun certoraTmpBool$11 () Bool true)
(define-fun certoraTmpBool$10 () Bool false)
(define-fun certoraTmp2$4 () Bool true)
(define-fun certoraTmpBool$9 () Bool true)
(define-fun tacS!ce4604a0000000000000000000000000!57!0$0 () Int 0)
(define-fun certoraTmpBool$8 () Bool true)
(define-fun certoraTmpBool$7 () Bool false)
(define-fun certoraTmp2$3 () Bool true)
(define-fun certoraTmpBool$6 () Bool true)
(define-fun tacS!ce4604a0000000000000000000000000!1!0$0 () Int 0)
(define-fun certoraTmpBool$5 () Bool true)
(define-fun certoraTmpBool$4 () Bool false)
(define-fun certoraTmp2$2 () Bool true)
(define-fun certoraTmpBool$3 () Bool true)
(define-fun a$0 () Int 1461501637330902918203684832716283019655932542975)
(define-fun certoraTmpBool$2 () Bool true)
(define-fun certoraTmpBool$1 () Bool true)
(define-fun certoraTmp2$1 () Bool false)
(define-fun B3542@9$1 () Bool true)
(define-fun OK_12453_1017_0_0_9_0_142_0 () Bool true)
(define-fun OK_12445_1017_0_0_9_0_146_0 () Bool false)
(define-fun R2755@9$1 () Int 0)
(define-fun tacS!ce4604a0000000000000000000000000$0 () (Array Int Int) (store (store ((as const (Array Int Int)) 1) 113013079095620606733405281368479398064791505033665190502510601991723214528577536 2000000000000000000000000001) 98191691673244133719188195287390729885770241443154457262783491767024828855353328 0))
(define-fun R390@9$1 () Int 1461501637330902918203684832716283019655932542975)
(define-fun hash2linear ((BOUND_VARIABLE_12334 Int) (BOUND_VARIABLE_12335 Int)) Int (ite (= BOUND_VARIABLE_12334 0) (ite (= BOUND_VARIABLE_12335 60) 113013079095620606733405281368479398064791505033665190502510601991723214528577536 98191691673244133719188195287390729885770241443154457262783491767024828855353328) 98191691673244133719188195287390729885770241443154457262783491767024828855353328))
(define-fun R1723@9$1 () Int 2000000000000000000000000001)
(define-fun tacTimestamp@9$0 () Int 0)
(define-fun B1172@9$1 () Bool false)
(define-fun R1171@9$1 () Int 2000000000000000000000000001)
(define-fun tacCalldatabuf!4@9$0 () Int 1461501637330902918203684832716283019655932542975)
(define-fun uninterp_bwand ((BOUND_VARIABLE_12334 Int) (BOUND_VARIABLE_12335 Int)) Int (ite (= BOUND_VARIABLE_12334 1461501637330902918203684832716283019655932542975) (ite (= BOUND_VARIABLE_12335 1461501637330902918203684832716283019655932542975) 1461501637330902918203684832716283019655932542975 0) 0))
(define-fun B133@9$1 () Bool false)
(define-fun R131@9$1 () Int 32)
(define-fun tacCalldatasize@9$0 () Int 36)
(define-fun B67@9$1 () Bool true)
(define-fun tacCallvalue@9$0 () Int 0)
(define-fun B38@9$1 () Bool true)
(define-fun R10@9$1 () Int 1889567281)
(define-fun B26@9$1 () Bool true)
(define-fun B20@9$1 () Bool true)
(define-fun B12@9$1 () Bool false)
(define-fun tacCalldatabuf!0@9$0 () Int 0)
(define-fun uninterp_bwlshr ((BOUND_VARIABLE_12334 Int) (BOUND_VARIABLE_12335 Int)) Int (ite (= BOUND_VARIABLE_12334 2) (ite (= BOUND_VARIABLE_12335 224) 1889567281 359541238) (ite (= BOUND_VARIABLE_12334 0) (ite (= BOUND_VARIABLE_12335 224) 1889567281 359541238) 359541238)))
(define-fun B5@9$1 () Bool false)
(define-fun B3@9$1 () Bool true)
(define-fun R2@9$1 () Int 1)
(define-fun tacExtcodesize$0 () (Array Int Int) (store ((as const (Array Int Int)) (- 1)) 274184521717934524641157099916833587200 1))
(define-fun tacAddress@9$0 () Int 274184521717934524641157099916833587200)
(define-fun B1@9$1 () Bool true)
(define-fun certoraTmpBool$26 () Bool true)
(define-fun e.block.timestamp$0 () Int 0)
(define-fun certoraTmpBool$25 () Bool true)
(define-fun tacNumber@9$0 () Int 0)
(define-fun e.block.number$0 () Int 0)
(define-fun certoraTmpBool$24 () Bool true)
(define-fun tacOrigin@9$0 () Int 0)
(define-fun certoraTmpBool$23 () Bool true)
(define-fun certoraTmpBool$22 () Bool false)
(define-fun certoraTmp2$7 () Bool true)
(define-fun certoraTmpBool$21 () Bool true)
(define-fun certoraTmpBool$20 () Bool true)
(define-fun certoraTmpBool$19 () Bool true)
(define-fun certoraTmp2$6 () Bool false)
(define-fun certoraTmpBool$18 () Bool true)
(define-fun e.msg.address$0 () Int 274184521717934524641157099916833587200)
(define-fun certoraTmpBool$17 () Bool true)
(define-fun e.msg.value$0 () Int 0)
(define-fun certoraTmpBool$16 () Bool true)
(define-fun tacCaller@9$0 () Int 0)
(define-fun certoraTmpBool$15 () Bool true)
(define-fun certoraTmpBool$14 () Bool false)
(define-fun certoraTmp2$5 () Bool true)
(define-fun certoraTmpBool$13 () Bool true)
(define-fun e.msg.sender$0 () Int 0)
(define-fun certoraEqParam$2 () Bool true)
(define-fun certoraEqParam$1 () Bool true)
(define-fun tacTmp$1 () Int 1461501637330902918203684832716283019655932542975)
(define-fun tacCalldatabuf@9$0 () (Array Int Int) (store (store ((as const (Array Int Int)) 0) 0 2) 4 1461501637330902918203684832716283019655932542975))
(define-fun datasizeCheck$2 () Bool false)
(define-fun tmpLastMsgSig$2 () Bool true)
(define-fun certoraInput$4 () Int 1889567281)
(define-fun datasizeCheck$1 () Bool false)
(define-fun tmpLastMsgSig$1 () Bool true)
(define-fun certoraInput$2 () Int 1889567281)
(define-fun certoraInput$1 () Int 2)
(define-fun tacTmpBool$1 () Bool true)
(define-fun tacM0x40@9$4 () Int 128)
(define-fun R3784@9$3 () Int 0)
(define-fun R5992@9$1 () Int 0)
(define-fun OK_12993_1017_0_0_9_0_147_0 () Bool false)
(define-fun R4630@9$1 () Int 0)
(define-fun uninterp_div ((BOUND_VARIABLE_12334 Int) (BOUND_VARIABLE_12335 Int)) Int 0)
(define-fun B4891@9$1 () Bool false)
(define-fun tacM@9$4 () (Array Int Int) ((as const (Array Int Int)) 0))
(define-fun tacM@9$3 () (Array Int Int) ((as const (Array Int Int)) 0))
(define-fun tacM@9$2 () (Array Int Int) ((as const (Array Int Int)) 0))
(define-fun B4890@9$1 () Bool false)
(define-fun R3777@9$1 () Int 1)
(define-fun B3969@9$1 () Bool false)
(define-fun tacM@9$1 () (Array Int Int) ((as const (Array Int Int)) 0))
(define-fun tacM@9$0 () (Array Int Int) ((as const (Array Int Int)) 2))
(define-fun R3968@9$1 () Int 0)
(define-fun uninterp_mul ((BOUND_VARIABLE_12334 Int) (BOUND_VARIABLE_12335 Int)) Int 0)
(define-fun OK_11_0_0_0_0_0_0_0 () Bool false)
(define-fun certora_returnSizeMatch9$2 () Bool true)
(define-fun R4651@9$1 () Int 32)
(define-fun tacRetval0@9$1 () Int 0)
(define-fun tacM@9$6 () (Array Int Int) (store ((as const (Array Int Int)) 2) 128 0))
(define-fun R4643@9$1 () Int 160)
(define-fun R4646@9$1 () Int 128)
(define-fun tacM@9$5 () (Array Int Int) ((as const (Array Int Int)) 2))
(define-fun ReachabilityCertora12445_1017_0_0_9_0_146_0$0 () Bool true)
(define-fun OK_0_0_0_0_10_0_148_0 () Bool false)
(define-fun OK_19_0_0_0_0_0_0_0 () Bool false)
(define-fun tacS!ce4604a0000000000000000000000000$1 () (Array Int Int) (store (store ((as const (Array Int Int)) 1) 113013079095620606733405281368479398064791505033665190502510601991723214528577536 2000000000000000000000000001) 98191691673244133719188195287390729885770241443154457262783491767024828855353328 0))
(define-fun R234@10$1 () Int 1461501637330902918203684832716283019655932542975)
(define-fun R7900@10$1 () Int 0)
(define-fun B7905@10$1 () Bool false)
(define-fun R7744@10$1 () Int 0)
(define-fun R5188@10$1 () Int 0)
(define-fun B7398@10$1 () Bool false)
(define-fun R7393@10$1 () Int 0)
(define-fun tacS!ce4604a0000000000000000000000000!54$0 () Int 0)
(define-fun tmp!alias!assume@10$1 () Bool true)
(define-fun B6162@10$1 () Bool false)
(define-fun R4408@10$1 () Int 2000000000000000000000000000)
(define-fun tacCalldatabuf!68@10$0 () Int 2000000000000000000000000001)
(define-fun B4414@10$1 () Bool true)
(define-fun B4413@10$1 () Bool false)
(define-fun R3922@10$1 () Int 1000000000000000000000000000)
(define-fun R3926@10$1 () Int 1000000000000000000000000000)
(define-fun B4139@10$1 () Bool true)
(define-fun R4138@10$1 () Int 1)
(define-fun tacCalldatabuf!36@10$0 () Int 1)
(define-fun B3396@10$1 () Bool true)
(define-fun B3395@10$1 () Bool false)
(define-fun B2619@10$1 () Bool false)
(define-fun R2071@10$1 () Int 2000000000000000000000000001)
(define-fun tacTimestamp@10$0 () Int 0)
(define-fun B1476@10$1 () Bool false)
(define-fun R1475@10$1 () Int 2000000000000000000000000001)
(define-fun B555@10$1 () Bool true)
(define-fun R554@10$1 () Int 0)
(define-fun R552@10$1 () Int 0)
(define-fun tacCaller@10$0 () Int 0)
(define-fun tacImmut_POOL$0 () Int 2923003274661805836407369665432566039311865085952)
(define-fun tacCalldatabuf!4@10$0 () Int 1461501637330902918203684832716283019655932542975)
(define-fun B97@10$1 () Bool false)
(define-fun R95@10$1 () Int 96)
(define-fun tacCalldatasize@10$0 () Int 100)
(define-fun B52@10$1 () Bool true)
(define-fun tacCallvalue@10$0 () Int 0)
(define-fun B32@10$1 () Bool true)
(define-fun R10@10$1 () Int 359541238)
(define-fun B22@10$1 () Bool false)
(define-fun B18@10$1 () Bool true)
(define-fun B12@10$1 () Bool true)
(define-fun tacCalldatabuf!0@10$0 () Int 1)
(define-fun B5@10$1 () Bool false)
(define-fun B3@10$1 () Bool true)
(define-fun R2@10$1 () Int 1)
(define-fun tacAddress@10$0 () Int 274184521717934524641157099916833587200)
(define-fun B1@10$1 () Bool true)
(define-fun certoraTmpBool$40 () Bool true)
(define-fun certoraTmpBool$39 () Bool true)
(define-fun tacNumber@10$0 () Int 0)
(define-fun certoraTmpBool$38 () Bool true)
(define-fun tacOrigin@10$0 () Int 0)
(define-fun certoraTmpBool$37 () Bool true)
(define-fun certoraTmpBool$36 () Bool false)
(define-fun certoraTmp2$10 () Bool true)
(define-fun certoraTmpBool$35 () Bool true)
(define-fun certoraTmpBool$34 () Bool true)
(define-fun certoraTmpBool$33 () Bool true)
(define-fun certoraTmp2$9 () Bool false)
(define-fun certoraTmpBool$32 () Bool true)
(define-fun certoraTmpBool$31 () Bool true)
(define-fun certoraTmpBool$30 () Bool true)
(define-fun certoraTmpBool$29 () Bool true)
(define-fun certoraTmpBool$28 () Bool false)
(define-fun certoraTmp2$8 () Bool true)
(define-fun certoraTmpBool$27 () Bool true)
(define-fun certoraEqParam$8 () Bool true)
(define-fun index$0 () Int 2000000000000000000000000001)
(define-fun certoraEqParam$7 () Bool true)
(define-fun tacTmp$4 () Int 2000000000000000000000000001)
(define-fun tacCalldatabuf@10$0 () (Array Int Int) (store (store (store (store ((as const (Array Int Int)) (- 2)) 0 1) 4 1461501637330902918203684832716283019655932542975) 36 1) 68 2000000000000000000000000001))
(define-fun certoraEqParam$6 () Bool true)
(define-fun x$0 () Int 1)
(define-fun certoraEqParam$5 () Bool true)
(define-fun tacTmp$3 () Int 1)
(define-fun certoraEqParam$4 () Bool true)
(define-fun certoraEqParam$3 () Bool true)
(define-fun tacTmp$2 () Int 1461501637330902918203684832716283019655932542975)
(define-fun datasizeCheck$4 () Bool false)
(define-fun tmpLastMsgSig$4 () Bool true)
(define-fun certoraInput$8 () Int 359541238)
(define-fun datasizeCheck$3 () Bool false)
(define-fun tmpLastMsgSig$3 () Bool true)
(define-fun certoraInput$6 () Int 359541238)
(define-fun certoraInput$5 () Int 1)
(define-fun tacTmpBool$2 () Bool true)
(define-fun OK_0_0_0_0_11_0_161_0 () Bool false)
(define-fun B3542@11$1 () Bool true)
(define-fun OK_12453_1017_0_0_11_0_165_0 () Bool true)
(define-fun OK_12445_1017_0_0_11_0_169_0 () Bool false)
(define-fun R2755@11$1 () Int 0)
(define-fun R390@11$1 () Int 1461501637330902918203684832716283019655932542975)
(define-fun R1723@11$1 () Int 2000000000000000000000000001)
(define-fun tacTimestamp@11$0 () Int 0)
(define-fun B1172@11$1 () Bool false)
(define-fun R1171@11$1 () Int 2000000000000000000000000001)
(define-fun tacCalldatabuf!4@11$0 () Int 1461501637330902918203684832716283019655932542975)
(define-fun B133@11$1 () Bool false)
(define-fun R131@11$1 () Int 32)
(define-fun tacCalldatasize@11$0 () Int 36)
(define-fun B67@11$1 () Bool true)
(define-fun tacCallvalue@11$0 () Int 0)
(define-fun B38@11$1 () Bool true)
(define-fun R10@11$1 () Int 1889567281)
(define-fun B26@11$1 () Bool true)
(define-fun B20@11$1 () Bool true)
(define-fun B12@11$1 () Bool false)
(define-fun tacCalldatabuf!0@11$0 () Int 2)
(define-fun B5@11$1 () Bool false)
(define-fun B3@11$1 () Bool true)
(define-fun R2@11$1 () Int 1)
(define-fun tacAddress@11$0 () Int 274184521717934524641157099916833587200)
(define-fun B1@11$1 () Bool true)
(define-fun certoraTmpBool$54 () Bool true)
(define-fun certoraTmpBool$53 () Bool true)
(define-fun tacNumber@11$0 () Int 0)
(define-fun certoraTmpBool$52 () Bool true)
(define-fun tacOrigin@11$0 () Int 0)
(define-fun certoraTmpBool$51 () Bool true)
(define-fun certoraTmpBool$50 () Bool false)
(define-fun certoraTmp2$13 () Bool true)
(define-fun certoraTmpBool$49 () Bool true)
(define-fun certoraTmpBool$48 () Bool true)
(define-fun certoraTmpBool$47 () Bool true)
(define-fun certoraTmp2$12 () Bool false)
(define-fun certoraTmpBool$46 () Bool true)
(define-fun certoraTmpBool$45 () Bool true)
(define-fun certoraTmpBool$44 () Bool true)
(define-fun tacCaller@11$0 () Int 0)
(define-fun certoraTmpBool$43 () Bool true)
(define-fun certoraTmpBool$42 () Bool false)
(define-fun certoraTmp2$11 () Bool true)
(define-fun certoraTmpBool$41 () Bool true)
(define-fun certoraEqParam$10 () Bool true)
(define-fun certoraEqParam$9 () Bool true)
(define-fun tacTmp$5 () Int 1461501637330902918203684832716283019655932542975)
(define-fun tacCalldatabuf@11$0 () (Array Int Int) (store (store ((as const (Array Int Int)) 3) 0 2) 4 1461501637330902918203684832716283019655932542975))
(define-fun datasizeCheck$6 () Bool false)
(define-fun tmpLastMsgSig$6 () Bool true)
(define-fun certoraInput$12 () Int 1889567281)
(define-fun datasizeCheck$5 () Bool false)
(define-fun tmpLastMsgSig$5 () Bool true)
(define-fun certoraInput$10 () Int 1889567281)
(define-fun certoraInput$9 () Int 2)
(define-fun tacTmpBool$3 () Bool true)
(define-fun tacM0x40@11$4 () Int 128)
(define-fun R3784@11$3 () Int 0)
(define-fun R5992@11$1 () Int 0)
(define-fun OK_12993_1017_0_0_11_0_170_0 () Bool false)
(define-fun R4630@11$1 () Int 0)
(define-fun B4891@11$1 () Bool false)
(define-fun tacM@11$4 () (Array Int Int) ((as const (Array Int Int)) 0))
(define-fun tacM@11$3 () (Array Int Int) ((as const (Array Int Int)) 0))
(define-fun tacM@11$2 () (Array Int Int) ((as const (Array Int Int)) 0))
(define-fun B4890@11$1 () Bool false)
(define-fun R3777@11$1 () Int 1)
(define-fun B3969@11$1 () Bool false)
(define-fun tacM@11$1 () (Array Int Int) ((as const (Array Int Int)) 0))
(define-fun tacM@11$0 () (Array Int Int) ((as const (Array Int Int)) (- 3)))
(define-fun R3968@11$1 () Int 0)
(define-fun OK_25_0_0_0_0_0_0_0 () Bool false)
(define-fun certora_returnSizeMatch11$2 () Bool true)
(define-fun R4651@11$1 () Int 32)
(define-fun tacRetval0@11$1 () Int 0)
(define-fun tacM@11$6 () (Array Int Int) (store ((as const (Array Int Int)) (- 3)) 128 0))
(define-fun R4643@11$1 () Int 160)
(define-fun R4646@11$1 () Int 128)
(define-fun tacM@11$5 () (Array Int Int) ((as const (Array Int Int)) (- 3)))
(define-fun ReachabilityCertora12445_1017_0_0_11_0_169_0$0 () Bool true)
(define-fun certoraAssert_1$1 () Bool false)
(define-fun ReachabilityCertora0_0_0_0_0_0_0_0$0 () Bool true)
(define-fun ReachabilityCertora0_0_0_0_9_0_138_0$0 () Bool true)
(define-fun ReachabilityCertora12453_1017_0_0_9_0_142_0$0 () Bool false)
(define-fun ReachabilityCertora12993_1017_0_0_9_0_147_0$0 () Bool true)
(define-fun ReachabilityCertora11_0_0_0_0_0_0_0$0 () Bool true)
(define-fun ReachabilityCertora0_0_0_0_10_0_148_0$0 () Bool true)
(define-fun ReachabilityCertora19_0_0_0_0_0_0_0$0 () Bool true)
(define-fun ReachabilityCertora0_0_0_0_11_0_161_0$0 () Bool true)
(define-fun ReachabilityCertora12453_1017_0_0_11_0_165_0$0 () Bool false)
(define-fun ReachabilityCertora12993_1017_0_0_11_0_170_0$0 () Bool true)
(define-fun ReachabilityCertora25_0_0_0_0_0_0_0$0 () Bool true)
(define-fun OK_0_0_0_0_0_0_0_0 () Bool false)
(define-fun certoraAndSmallPart11 () Int 0)
(define-fun certoraAndSmallPart22 () Int 0)
(define-fun certoraAndSmallPart33 () Int 2)
(define-fun certoraAndSmallPart44 () Int 0)
(define-fun certoraAndSmallPart55 () Int 0)
)