(set-logic QF_BV)
; benchmark generated from python API
(set-info :status unknown)
(declare-fun q0 () (_ BitVec 8))
(declare-fun r0 () (_ BitVec 8))
(declare-fun q1 () (_ BitVec 8))
(declare-fun r1 () (_ BitVec 8))
(declare-fun q2 () (_ BitVec 8))
(declare-fun r2 () (_ BitVec 8))
(declare-fun q3 () (_ BitVec 8))
(declare-fun r3 () (_ BitVec 8))
(declare-fun q4 () (_ BitVec 8))
(declare-fun r4 () (_ BitVec 8))
(declare-fun q5 () (_ BitVec 8))
(declare-fun r5 () (_ BitVec 8))
(declare-fun q6 () (_ BitVec 8))
(declare-fun r6 () (_ BitVec 8))
(declare-fun q7 () (_ BitVec 8))
(declare-fun r7 () (_ BitVec 8))
(declare-fun q8 () (_ BitVec 8))
(declare-fun r8 () (_ BitVec 8))
(declare-fun q9 () (_ BitVec 8))
(declare-fun r9 () (_ BitVec 8))
(declare-fun q10 () (_ BitVec 8))
(declare-fun r10 () (_ BitVec 8))
(declare-fun q11 () (_ BitVec 8))
(declare-fun r11 () (_ BitVec 8))
(declare-fun q12 () (_ BitVec 8))
(declare-fun r12 () (_ BitVec 8))
(declare-fun q13 () (_ BitVec 8))
(declare-fun r13 () (_ BitVec 8))
(declare-fun q14 () (_ BitVec 8))
(declare-fun r14 () (_ BitVec 8))
(declare-fun q15 () (_ BitVec 8))
(declare-fun r15 () (_ BitVec 8))
(declare-fun q16 () (_ BitVec 8))
(declare-fun r16 () (_ BitVec 8))
(declare-fun q17 () (_ BitVec 8))
(declare-fun r17 () (_ BitVec 8))
(declare-fun q18 () (_ BitVec 8))
(declare-fun r18 () (_ BitVec 8))
(declare-fun q19 () (_ BitVec 8))
(declare-fun r19 () (_ BitVec 8))
(declare-fun q20 () (_ BitVec 8))
(declare-fun r20 () (_ BitVec 8))
(declare-fun q21 () (_ BitVec 8))
(declare-fun r21 () (_ BitVec 8))
(declare-fun q22 () (_ BitVec 8))
(declare-fun r22 () (_ BitVec 8))
(declare-fun q23 () (_ BitVec 8))
(declare-fun r23 () (_ BitVec 8))
(declare-fun q24 () (_ BitVec 8))
(declare-fun r24 () (_ BitVec 8))
(declare-fun q25 () (_ BitVec 8))
(declare-fun r25 () (_ BitVec 8))
(declare-fun q26 () (_ BitVec 8))
(declare-fun r26 () (_ BitVec 8))
(declare-fun q27 () (_ BitVec 8))
(declare-fun r27 () (_ BitVec 8))
(declare-fun q28 () (_ BitVec 8))
(declare-fun r28 () (_ BitVec 8))
(declare-fun q29 () (_ BitVec 8))
(declare-fun r29 () (_ BitVec 8))
(declare-fun q30 () (_ BitVec 8))
(declare-fun r30 () (_ BitVec 8))
(declare-fun q31 () (_ BitVec 8))
(declare-fun r31 () (_ BitVec 8))
(declare-fun q32 () (_ BitVec 8))
(declare-fun r32 () (_ BitVec 8))
(assert
 (bvule q0 (_ bv225 8)))
(assert
 (bvule r0 (_ bv225 8)))
(assert
 (bvule q1 (_ bv225 8)))
(assert
 (bvule r1 (_ bv225 8)))
(assert
 (bvule q2 (_ bv225 8)))
(assert
 (bvule r2 (_ bv225 8)))
(assert
 (bvule q3 (_ bv225 8)))
(assert
 (bvule r3 (_ bv225 8)))
(assert
 (bvule q4 (_ bv225 8)))
(assert
 (bvule r4 (_ bv225 8)))
(assert
 (bvule q5 (_ bv225 8)))
(assert
 (bvule r5 (_ bv225 8)))
(assert
 (bvule q6 (_ bv225 8)))
(assert
 (bvule r6 (_ bv225 8)))
(assert
 (bvule q7 (_ bv225 8)))
(assert
 (bvule r7 (_ bv225 8)))
(assert
 (bvule q8 (_ bv225 8)))
(assert
 (bvule r8 (_ bv225 8)))
(assert
 (bvule q9 (_ bv225 8)))
(assert
 (bvule r9 (_ bv225 8)))
(assert
 (bvule q10 (_ bv225 8)))
(assert
 (bvule r10 (_ bv225 8)))
(assert
 (bvule q11 (_ bv225 8)))
(assert
 (bvule r11 (_ bv225 8)))
(assert
 (bvule q12 (_ bv225 8)))
(assert
 (bvule r12 (_ bv225 8)))
(assert
 (bvule q13 (_ bv225 8)))
(assert
 (bvule r13 (_ bv225 8)))
(assert
 (bvule q14 (_ bv225 8)))
(assert
 (bvule r14 (_ bv225 8)))
(assert
 (bvule q15 (_ bv225 8)))
(assert
 (bvule r15 (_ bv225 8)))
(assert
 (bvule q16 (_ bv225 8)))
(assert
 (bvule r16 (_ bv225 8)))
(assert
 (bvule q17 (_ bv225 8)))
(assert
 (bvule r17 (_ bv225 8)))
(assert
 (bvule q18 (_ bv225 8)))
(assert
 (bvule r18 (_ bv225 8)))
(assert
 (bvule q19 (_ bv225 8)))
(assert
 (bvule r19 (_ bv225 8)))
(assert
 (bvule q20 (_ bv225 8)))
(assert
 (bvule r20 (_ bv225 8)))
(assert
 (bvule q21 (_ bv225 8)))
(assert
 (bvule r21 (_ bv225 8)))
(assert
 (bvule q22 (_ bv225 8)))
(assert
 (bvule r22 (_ bv225 8)))
(assert
 (bvule q23 (_ bv225 8)))
(assert
 (bvule r23 (_ bv225 8)))
(assert
 (bvule q24 (_ bv225 8)))
(assert
 (bvule r24 (_ bv225 8)))
(assert
 (bvule q25 (_ bv225 8)))
(assert
 (bvule r25 (_ bv225 8)))
(assert
 (bvule q26 (_ bv225 8)))
(assert
 (bvule r26 (_ bv225 8)))
(assert
 (bvule q27 (_ bv225 8)))
(assert
 (bvule r27 (_ bv225 8)))
(assert
 (bvule q28 (_ bv225 8)))
(assert
 (bvule r28 (_ bv225 8)))
(assert
 (bvule q29 (_ bv225 8)))
(assert
 (bvule r29 (_ bv225 8)))
(assert
 (bvule q30 (_ bv225 8)))
(assert
 (bvule r30 (_ bv225 8)))
(assert
 (bvule q31 (_ bv225 8)))
(assert
 (bvule r31 (_ bv225 8)))
(assert
 (bvule q32 (_ bv225 8)))
(assert
 (bvule r32 (_ bv225 8)))
(assert
 (let ((?x123 ((_ zero_extend 24) r32)))
 (let ((?x1321 ((_ zero_extend 24) q32)))
 (let ((?x203 ((_ zero_extend 24) r31)))
 (let ((?x4834 ((_ zero_extend 24) q31)))
 (let ((?x1339 ((_ zero_extend 24) r30)))
 (let ((?x3719 ((_ zero_extend 24) q30)))
 (let ((?x2137 ((_ zero_extend 24) r29)))
 (let ((?x1987 ((_ zero_extend 24) q29)))
 (let ((?x1594 ((_ zero_extend 24) r28)))
 (let ((?x3752 ((_ zero_extend 24) q28)))
 (let ((?x1345 ((_ zero_extend 24) r27)))
 (let ((?x3934 ((_ zero_extend 24) q27)))
 (let ((?x1754 ((_ zero_extend 24) r26)))
 (let ((?x4671 ((_ zero_extend 24) q26)))
 (let ((?x2247 ((_ zero_extend 24) r25)))
 (let ((?x3494 ((_ zero_extend 24) q25)))
 (let ((?x1793 ((_ zero_extend 24) r24)))
 (let ((?x1323 ((_ zero_extend 24) q24)))
 (let ((?x2536 ((_ zero_extend 24) r23)))
 (let ((?x247 ((_ zero_extend 24) q23)))
 (let ((?x1465 ((_ zero_extend 24) r22)))
 (let ((?x89 ((_ zero_extend 24) q22)))
 (let ((?x3502 ((_ zero_extend 24) r21)))
 (let ((?x3017 ((_ zero_extend 24) q21)))
 (let ((?x441 ((_ zero_extend 24) r20)))
 (let ((?x3225 ((_ zero_extend 24) q20)))
 (let ((?x3504 ((_ zero_extend 24) r19)))
 (let ((?x1678 ((_ zero_extend 24) q19)))
 (let ((?x4253 ((_ zero_extend 24) r18)))
 (let ((?x4412 ((_ zero_extend 24) q18)))
 (let ((?x1823 ((_ zero_extend 24) r17)))
 (let ((?x3453 ((_ zero_extend 24) q17)))
 (let ((?x2061 ((_ zero_extend 24) r16)))
 (let ((?x5561 ((_ zero_extend 24) q16)))
 (let ((?x2561 ((_ zero_extend 24) r15)))
 (let ((?x3443 ((_ zero_extend 24) q15)))
 (let ((?x295 ((_ zero_extend 24) r14)))
 (let ((?x3647 ((_ zero_extend 24) q14)))
 (let ((?x77 ((_ zero_extend 24) r13)))
 (let ((?x3884 ((_ zero_extend 24) q13)))
 (let ((?x741 ((_ zero_extend 24) r12)))
 (let ((?x399 ((_ zero_extend 24) q12)))
 (let ((?x4477 ((_ zero_extend 24) r11)))
 (let ((?x4167 ((_ zero_extend 24) q11)))
 (let ((?x3173 ((_ zero_extend 24) r10)))
 (let ((?x1750 ((_ zero_extend 24) q10)))
 (let ((?x2529 ((_ zero_extend 24) r9)))
 (let ((?x2345 ((_ zero_extend 24) q9)))
 (let ((?x4247 ((_ zero_extend 24) r8)))
 (let ((?x1172 ((_ zero_extend 24) q8)))
 (let ((?x1703 ((_ zero_extend 24) r7)))
 (let ((?x3843 ((_ zero_extend 24) q7)))
 (let ((?x1873 ((_ zero_extend 24) r6)))
 (let ((?x2011 ((_ zero_extend 24) q6)))
 (let ((?x2622 ((_ zero_extend 24) r5)))
 (let ((?x4488 ((_ zero_extend 24) q5)))
 (let ((?x3293 ((_ zero_extend 24) r4)))
 (let ((?x106 ((_ zero_extend 24) q4)))
 (let ((?x1507 ((_ zero_extend 24) r3)))
 (let ((?x2478 ((_ zero_extend 24) q3)))
 (let ((?x817 ((_ zero_extend 24) r2)))
 (let ((?x1260 ((_ zero_extend 24) q2)))
 (let ((?x3898 ((_ zero_extend 24) r1)))
 (let ((?x493 ((_ zero_extend 24) q1)))
 (let ((?x313 (bvadd (bvadd (bvadd (bvadd (_ bv0 32) ((_ zero_extend 24) q0)) ((_ zero_extend 24) r0)) ?x493) ?x3898)))
 (let ((?x2361 (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd ?x313 ?x1260) ?x817) ?x2478) ?x1507) ?x106) ?x3293)))
 (let ((?x3726 (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd ?x2361 ?x4488) ?x2622) ?x2011) ?x1873) ?x3843) ?x1703)))
 (let ((?x1414 (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd ?x3726 ?x1172) ?x4247) ?x2345) ?x2529) ?x1750) ?x3173)))
 (let ((?x198 (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd ?x1414 ?x4167) ?x4477) ?x399) ?x741) ?x3884) ?x77)))
 (let ((?x725 (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd ?x198 ?x3647) ?x295) ?x3443) ?x2561) ?x5561) ?x2061)))
 (let ((?x4432 (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd ?x725 ?x3453) ?x1823) ?x4412) ?x4253) ?x1678) ?x3504)))
 (let ((?x2170 (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd ?x4432 ?x3225) ?x441) ?x3017) ?x3502) ?x89) ?x1465)))
 (let ((?x220 (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd ?x2170 ?x247) ?x2536) ?x1323) ?x1793) ?x3494) ?x2247)))
 (let ((?x3500 (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd ?x220 ?x4671) ?x1754) ?x3934) ?x1345) ?x3752) ?x1594)))
 (let ((?x1732 (bvadd (bvadd (bvadd (bvadd (bvadd (bvadd ?x3500 ?x1987) ?x2137) ?x3719) ?x1339) ?x4834) ?x203)))
 (let ((?x4140 (bvadd (bvadd ?x1732 ?x1321) ?x123)))
 (let ((?x4499 (bvadd (bvlshr (concat r29 r28) (_ bv8 16)) (bvand (concat r29 r28) (_ bv255 16)))))
 (let ((?x2140 (bvadd (bvlshr (concat r13 r12) (_ bv8 16)) (bvand (concat r13 r12) (_ bv255 16)))))
 (let ((?x1544 (bvadd (bvlshr (concat r31 r30) (_ bv8 16)) (bvand (concat r31 r30) (_ bv255 16)))))
 (let ((?x3750 (bvadd (bvlshr (concat r15 r14) (_ bv8 16)) (bvand (concat r15 r14) (_ bv255 16)))))
 (let ((?x3936 (concat (bvadd (bvadd (_ bv0 16) ?x3750) ?x1544) (bvadd (bvadd (_ bv0 16) ?x2140) ?x4499))))
 (let ((?x158 (bvadd (bvlshr (concat q29 q28) (_ bv8 16)) (bvand (concat q29 q28) (_ bv255 16)))))
 (let ((?x2315 (bvadd (bvlshr (concat q13 q12) (_ bv8 16)) (bvand (concat q13 q12) (_ bv255 16)))))
 (let ((?x267 (bvadd (bvlshr (concat q31 q30) (_ bv8 16)) (bvand (concat q31 q30) (_ bv255 16)))))
 (let ((?x3914 (bvadd (bvlshr (concat q15 q14) (_ bv8 16)) (bvand (concat q15 q14) (_ bv255 16)))))
 (let ((?x4280 (concat (bvadd (bvadd (_ bv0 16) ?x3914) ?x267) (bvadd (bvadd (_ bv0 16) ?x2315) ?x158))))
 (let ((?x3779 (bvadd (bvadd (bvand ?x4280 (_ bv65535 32)) (bvlshr ?x4280 (_ bv16 32))) (bvand ?x3936 (_ bv65535 32)))))
 (let ((?x4130 (bvadd (bvlshr (concat r25 r24) (_ bv8 16)) (bvand (concat r25 r24) (_ bv255 16)))))
 (let ((?x3267 (bvadd (bvlshr (concat r9 r8) (_ bv8 16)) (bvand (concat r9 r8) (_ bv255 16)))))
 (let ((?x574 (bvadd (bvlshr (concat r27 r26) (_ bv8 16)) (bvand (concat r27 r26) (_ bv255 16)))))
 (let ((?x1741 (bvadd (bvlshr (concat r11 r10) (_ bv8 16)) (bvand (concat r11 r10) (_ bv255 16)))))
 (let ((?x3292 (concat (bvadd (bvadd (_ bv0 16) ?x1741) ?x574) (bvadd (bvadd (_ bv0 16) ?x3267) ?x4130))))
 (let ((?x1804 (bvadd (bvlshr (concat q25 q24) (_ bv8 16)) (bvand (concat q25 q24) (_ bv255 16)))))
 (let ((?x824 (bvadd (bvlshr (concat q9 q8) (_ bv8 16)) (bvand (concat q9 q8) (_ bv255 16)))))
 (let ((?x3965 (bvadd (bvlshr (concat q27 q26) (_ bv8 16)) (bvand (concat q27 q26) (_ bv255 16)))))
 (let ((?x2918 (bvadd (bvlshr (concat q11 q10) (_ bv8 16)) (bvand (concat q11 q10) (_ bv255 16)))))
 (let ((?x2388 (concat (bvadd (bvadd (_ bv0 16) ?x2918) ?x3965) (bvadd (bvadd (_ bv0 16) ?x824) ?x1804))))
 (let ((?x4291 (bvadd (bvadd (bvand ?x2388 (_ bv65535 32)) (bvlshr ?x2388 (_ bv16 32))) (bvand ?x3292 (_ bv65535 32)))))
 (let ((?x4367 (bvadd (bvlshr (concat r21 r20) (_ bv8 16)) (bvand (concat r21 r20) (_ bv255 16)))))
 (let ((?x3251 (bvadd (bvlshr (concat r5 r4) (_ bv8 16)) (bvand (concat r5 r4) (_ bv255 16)))))
 (let ((?x4289 (bvadd (bvlshr (concat r23 r22) (_ bv8 16)) (bvand (concat r23 r22) (_ bv255 16)))))
 (let ((?x3218 (bvadd (bvlshr (concat r7 r6) (_ bv8 16)) (bvand (concat r7 r6) (_ bv255 16)))))
 (let ((?x2153 (concat (bvadd (bvadd (_ bv0 16) ?x3218) ?x4289) (bvadd (bvadd (_ bv0 16) ?x3251) ?x4367))))
 (let ((?x307 (bvadd (bvlshr (concat q21 q20) (_ bv8 16)) (bvand (concat q21 q20) (_ bv255 16)))))
 (let ((?x1816 (bvadd (bvlshr (concat q5 q4) (_ bv8 16)) (bvand (concat q5 q4) (_ bv255 16)))))
 (let ((?x1246 (bvadd (bvlshr (concat q23 q22) (_ bv8 16)) (bvand (concat q23 q22) (_ bv255 16)))))
 (let ((?x327 (bvadd (bvlshr (concat q7 q6) (_ bv8 16)) (bvand (concat q7 q6) (_ bv255 16)))))
 (let ((?x2322 (concat (bvadd (bvadd (_ bv0 16) ?x327) ?x1246) (bvadd (bvadd (_ bv0 16) ?x1816) ?x307))))
 (let ((?x502 (bvadd (bvadd (bvand ?x2322 (_ bv65535 32)) (bvlshr ?x2322 (_ bv16 32))) (bvand ?x2153 (_ bv65535 32)))))
 (let ((?x2210 (bvadd (bvlshr (concat r17 r16) (_ bv8 16)) (bvand (concat r17 r16) (_ bv255 16)))))
 (let ((?x2297 (bvadd (bvlshr (concat r1 r0) (_ bv8 16)) (bvand (concat r1 r0) (_ bv255 16)))))
 (let ((?x1859 (bvadd (bvlshr (concat r19 r18) (_ bv8 16)) (bvand (concat r19 r18) (_ bv255 16)))))
 (let ((?x304 (bvadd (bvlshr (concat r3 r2) (_ bv8 16)) (bvand (concat r3 r2) (_ bv255 16)))))
 (let ((?x1325 (concat (bvadd (bvadd (_ bv0 16) ?x304) ?x1859) (bvadd (bvadd (_ bv0 16) ?x2297) ?x2210))))
 (let ((?x1426 (bvadd (bvlshr (concat q17 q16) (_ bv8 16)) (bvand (concat q17 q16) (_ bv255 16)))))
 (let ((?x4230 (bvadd (bvlshr (concat q1 q0) (_ bv8 16)) (bvand (concat q1 q0) (_ bv255 16)))))
 (let ((?x3874 (bvadd (bvlshr (concat q19 q18) (_ bv8 16)) (bvand (concat q19 q18) (_ bv255 16)))))
 (let ((?x1052 (bvadd (bvlshr (concat q3 q2) (_ bv8 16)) (bvand (concat q3 q2) (_ bv255 16)))))
 (let ((?x4239 (concat (bvadd (bvadd (_ bv0 16) ?x1052) ?x3874) (bvadd (bvadd (_ bv0 16) ?x4230) ?x1426))))
 (let ((?x1388 (bvadd (bvadd (bvand ?x4239 (_ bv65535 32)) (bvlshr ?x4239 (_ bv16 32))) (bvand ?x1325 (_ bv65535 32)))))
 (let ((?x4305 (bvadd (bvadd ?x1388 (bvlshr ?x1325 (_ bv16 32))) (bvadd ?x502 (bvlshr ?x2153 (_ bv16 32))))))
 (let ((?x3654 (bvadd (bvadd ?x4305 (bvadd ?x4291 (bvlshr ?x3292 (_ bv16 32)))) (bvadd ?x3779 (bvlshr ?x3936 (_ bv16 32))))))
 (let ((?x277 (bvadd (bvadd (bvadd (_ bv0 32) (bvadd (_ bv0 32) ?x3654)) ?x1321) ?x123)))
 (and (distinct (bvadd ?x277 (_ bv1 32)) (bvadd (bvadd ?x4140 (_ bv1 32)) (_ bv1 32))) true)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)