Find MD4 fixed points with with less thab 2^(128/2)/16 decisions & conflicts!

all_128.smt

(set-logic QF_BV) ; remove this line if you haven't patched z3 to incl. ext_rotate_left in QF_BV
(set-info :source |
    NOiSE BRiDGE HASHSMASH KREW
    solve md4(x) == x
    author zv <zv@nxvr.org>
|)
(set-info :smt-lib-version 2.0)
(set-info :status unknown)

;; We are seeking a valid assignment of the 4 32-bit literals (named 'ch_$N')
;; such that each of them corresponds to the same position's 32-bit output register of MD4.

;; E.G In md4(0000c0c504987a5c64949c7870428de4) ch_0 corresponds to '0000c0c5'.
;; The output registers (also 4 32-bit values) are indirectly searched for below
(declare-fun ch_0 () (_ BitVec 32))
(declare-fun ch_1 () (_ BitVec 32))
(declare-fun ch_2 () (_ BitVec 32))
(declare-fun ch_3 () (_ BitVec 32))

;; Each of the asserts below solves the message 32 bits at a time
(assert
 (let ((?x26 (bvadd (bvadd (_ bv1732584193 32) (bvor (bvand (_ bv4023233417 32) (_ bv2562383102 32)) (bvand (bvnot (_ bv4023233417 32)) (_ bv271733878 32)))) ch_0)))
 (let ((?x28 (ext_rotate_left ?x26 (_ bv3 32))))
 (let ((?x34 (bvadd (bvadd (_ bv271733878 32) (bvor (bvand ?x28 (_ bv4023233417 32)) (bvand (bvnot ?x28) (_ bv2562383102 32)))) ch_1)))
 (let ((?x36 (ext_rotate_left ?x34 (_ bv7 32))))
 (let ((?x42 (bvadd (bvadd (_ bv2562383102 32) (bvor (bvand ?x36 ?x28) (bvand (bvnot ?x36) (_ bv4023233417 32)))) ch_2)))
 (let ((?x44 (ext_rotate_left ?x42 (_ bv11 32))))
 (let ((?x50 (bvadd (bvadd (_ bv4023233417 32) (bvor (bvand ?x44 ?x36) (bvand (bvnot ?x44) ?x28))) ch_3)))
 (let ((?x52 (ext_rotate_left ?x50 (_ bv19 32))))
 (let ((?x58 (bvadd (bvadd ?x28 (bvor (bvand ?x52 ?x44) (bvand (bvnot ?x52) ?x36))) (_ bv128 32))))
 (let ((?x59 (ext_rotate_left ?x58 (_ bv3 32))))
 (let ((?x65 (bvadd (bvadd ?x36 (bvor (bvand ?x59 ?x52) (bvand (bvnot ?x59) ?x44))) (_ bv0 32))))
 (let ((?x66 (ext_rotate_left ?x65 (_ bv7 32))))
 (let ((?x72 (bvadd (bvadd ?x44 (bvor (bvand ?x66 ?x59) (bvand (bvnot ?x66) ?x52))) (_ bv0 32))))
 (let ((?x73 (ext_rotate_left ?x72 (_ bv11 32))))
 (let ((?x79 (bvadd (bvadd ?x52 (bvor (bvand ?x73 ?x66) (bvand (bvnot ?x73) ?x59))) (_ bv0 32))))
 (let ((?x80 (ext_rotate_left ?x79 (_ bv19 32))))
 (let ((?x86 (bvadd (bvadd ?x59 (bvor (bvand ?x80 ?x73) (bvand (bvnot ?x80) ?x66))) (_ bv0 32))))
 (let ((?x87 (ext_rotate_left ?x86 (_ bv3 32))))
 (let ((?x93 (bvadd (bvadd ?x66 (bvor (bvand ?x87 ?x80) (bvand (bvnot ?x87) ?x73))) (_ bv0 32))))
 (let ((?x94 (ext_rotate_left ?x93 (_ bv7 32))))
 (let ((?x100 (bvadd (bvadd ?x73 (bvor (bvand ?x94 ?x87) (bvand (bvnot ?x94) ?x80))) (_ bv0 32))))
 (let ((?x101 (ext_rotate_left ?x100 (_ bv11 32))))
 (let ((?x107 (bvadd (bvadd ?x80 (bvor (bvand ?x101 ?x94) (bvand (bvnot ?x101) ?x87))) (_ bv0 32))))
 (let ((?x108 (ext_rotate_left ?x107 (_ bv19 32))))
 (let ((?x114 (bvadd (bvadd ?x87 (bvor (bvand ?x108 ?x101) (bvand (bvnot ?x108) ?x94))) (_ bv0 32))))
 (let ((?x115 (ext_rotate_left ?x114 (_ bv3 32))))
 (let ((?x121 (bvadd (bvadd ?x94 (bvor (bvand ?x115 ?x108) (bvand (bvnot ?x115) ?x101))) (_ bv0 32))))
 (let ((?x122 (ext_rotate_left ?x121 (_ bv7 32))))
 (let ((?x128 (bvadd (bvadd ?x101 (bvor (bvand ?x122 ?x115) (bvand (bvnot ?x122) ?x108))) (_ bv128 32))))
 (let ((?x129 (ext_rotate_left ?x128 (_ bv11 32))))
 (let ((?x135 (bvadd (bvadd ?x108 (bvor (bvand ?x129 ?x122) (bvand (bvnot ?x129) ?x115))) (_ bv0 32))))
 (let ((?x136 (ext_rotate_left ?x135 (_ bv19 32))))
 (let ((?x141 (bvadd ?x115 (bvor (bvor (bvand ?x136 ?x129) (bvand ?x136 ?x122)) (bvand ?x129 ?x122)))))
 (let ((?x145 (ext_rotate_left (bvadd (bvadd ?x141 ch_0) (_ bv1518500249 32)) (_ bv3 32))))
 (let ((?x150 (bvadd ?x122 (bvor (bvor (bvand ?x145 ?x136) (bvand ?x145 ?x129)) (bvand ?x136 ?x129)))))
 (let ((?x154 (ext_rotate_left (bvadd (bvadd ?x150 (_ bv128 32)) (_ bv1518500249 32)) (_ bv5 32))))
 (let ((?x159 (bvadd ?x129 (bvor (bvor (bvand ?x154 ?x145) (bvand ?x154 ?x136)) (bvand ?x145 ?x136)))))
 (let ((?x163 (ext_rotate_left (bvadd (bvadd ?x159 (_ bv0 32)) (_ bv1518500249 32)) (_ bv9 32))))
 (let ((?x168 (bvadd ?x136 (bvor (bvor (bvand ?x163 ?x154) (bvand ?x163 ?x145)) (bvand ?x154 ?x145)))))
 (let ((?x172 (ext_rotate_left (bvadd (bvadd ?x168 (_ bv0 32)) (_ bv1518500249 32)) (_ bv13 32))))
 (let ((?x177 (bvadd ?x145 (bvor (bvor (bvand ?x172 ?x163) (bvand ?x172 ?x154)) (bvand ?x163 ?x154)))))
 (let ((?x180 (ext_rotate_left (bvadd (bvadd ?x177 ch_1) (_ bv1518500249 32)) (_ bv3 32))))
 (let ((?x185 (bvadd ?x154 (bvor (bvor (bvand ?x180 ?x172) (bvand ?x180 ?x163)) (bvand ?x172 ?x163)))))
 (let ((?x188 (ext_rotate_left (bvadd (bvadd ?x185 (_ bv0 32)) (_ bv1518500249 32)) (_ bv5 32))))
 (let ((?x193 (bvadd ?x163 (bvor (bvor (bvand ?x188 ?x180) (bvand ?x188 ?x172)) (bvand ?x180 ?x172)))))
 (let ((?x196 (ext_rotate_left (bvadd (bvadd ?x193 (_ bv0 32)) (_ bv1518500249 32)) (_ bv9 32))))
 (let ((?x201 (bvadd ?x172 (bvor (bvor (bvand ?x196 ?x188) (bvand ?x196 ?x180)) (bvand ?x188 ?x180)))))
 (let ((?x204 (ext_rotate_left (bvadd (bvadd ?x201 (_ bv0 32)) (_ bv1518500249 32)) (_ bv13 32))))
 (let ((?x209 (bvadd ?x180 (bvor (bvor (bvand ?x204 ?x196) (bvand ?x204 ?x188)) (bvand ?x196 ?x188)))))
 (let ((?x212 (ext_rotate_left (bvadd (bvadd ?x209 ch_2) (_ bv1518500249 32)) (_ bv3 32))))
 (let ((?x217 (bvadd ?x188 (bvor (bvor (bvand ?x212 ?x204) (bvand ?x212 ?x196)) (bvand ?x204 ?x196)))))
 (let ((?x220 (ext_rotate_left (bvadd (bvadd ?x217 (_ bv0 32)) (_ bv1518500249 32)) (_ bv5 32))))
 (let ((?x225 (bvadd ?x196 (bvor (bvor (bvand ?x220 ?x212) (bvand ?x220 ?x204)) (bvand ?x212 ?x204)))))
 (let ((?x228 (ext_rotate_left (bvadd (bvadd ?x225 (_ bv0 32)) (_ bv1518500249 32)) (_ bv9 32))))
 (let ((?x233 (bvadd ?x204 (bvor (bvor (bvand ?x228 ?x220) (bvand ?x228 ?x212)) (bvand ?x220 ?x212)))))
 (let ((?x236 (ext_rotate_left (bvadd (bvadd ?x233 (_ bv128 32)) (_ bv1518500249 32)) (_ bv13 32))))
 (let ((?x241 (bvadd ?x212 (bvor (bvor (bvand ?x236 ?x228) (bvand ?x236 ?x220)) (bvand ?x228 ?x220)))))
 (let ((?x244 (ext_rotate_left (bvadd (bvadd ?x241 ch_3) (_ bv1518500249 32)) (_ bv3 32))))
 (let ((?x249 (bvadd ?x220 (bvor (bvor (bvand ?x244 ?x236) (bvand ?x244 ?x228)) (bvand ?x236 ?x228)))))
 (let ((?x252 (ext_rotate_left (bvadd (bvadd ?x249 (_ bv0 32)) (_ bv1518500249 32)) (_ bv5 32))))
 (let ((?x257 (bvadd ?x228 (bvor (bvor (bvand ?x252 ?x244) (bvand ?x252 ?x236)) (bvand ?x244 ?x236)))))
 (let ((?x260 (ext_rotate_left (bvadd (bvadd ?x257 (_ bv0 32)) (_ bv1518500249 32)) (_ bv9 32))))
 (let ((?x265 (bvadd ?x236 (bvor (bvor (bvand ?x260 ?x252) (bvand ?x260 ?x244)) (bvand ?x252 ?x244)))))
 (let ((?x268 (ext_rotate_left (bvadd (bvadd ?x265 (_ bv0 32)) (_ bv1518500249 32)) (_ bv13 32))))
 (let ((?x274 (bvadd (bvadd (bvadd ?x244 (bvxor (bvxor ?x268 ?x260) ?x252)) ch_0) (_ bv1859775393 32))))
 (let ((?x275 (ext_rotate_left ?x274 (_ bv3 32))))
 (let ((?x281 (ext_rotate_left (bvadd (bvadd (bvadd ?x252 (bvxor (bvxor ?x275 ?x268) ?x260)) (_ bv0 32)) (_ bv1859775393 32)) (_ bv9 32))))
 (let ((?x287 (ext_rotate_left (bvadd (bvadd (bvadd ?x260 (bvxor (bvxor ?x281 ?x275) ?x268)) (_ bv128 32)) (_ bv1859775393 32)) (_ bv11 32))))
 (let ((?x294 (ext_rotate_left (bvadd (bvadd (bvadd ?x268 (bvxor (bvxor ?x287 ?x281) ?x275)) (_ bv0 32)) (_ bv1859775393 32)) (_ bv15 32))))
 (let ((?x299 (bvadd (bvadd (bvadd ?x275 (bvxor (bvxor ?x294 ?x287) ?x281)) ch_2) (_ bv1859775393 32))))
 (let ((?x300 (ext_rotate_left ?x299 (_ bv3 32))))
 (let ((?x306 (ext_rotate_left (bvadd (bvadd (bvadd ?x281 (bvxor (bvxor ?x300 ?x294) ?x287)) (_ bv0 32)) (_ bv1859775393 32)) (_ bv9 32))))
 (let ((?x312 (ext_rotate_left (bvadd (bvadd (bvadd ?x287 (bvxor (bvxor ?x306 ?x300) ?x294)) (_ bv0 32)) (_ bv1859775393 32)) (_ bv11 32))))
 (let ((?x318 (ext_rotate_left (bvadd (bvadd (bvadd ?x294 (bvxor (bvxor ?x312 ?x306) ?x300)) (_ bv128 32)) (_ bv1859775393 32)) (_ bv15 32))))
 (let ((?x323 (bvadd (bvadd (bvadd ?x300 (bvxor (bvxor ?x318 ?x312) ?x306)) ch_1) (_ bv1859775393 32))))
 (let ((?x324 (ext_rotate_left ?x323 (_ bv3 32))))
 (let ((?x330 (ext_rotate_left (bvadd (bvadd (bvadd ?x306 (bvxor (bvxor ?x324 ?x318) ?x312)) (_ bv0 32)) (_ bv1859775393 32)) (_ bv9 32))))
 (let ((?x336 (ext_rotate_left (bvadd (bvadd (bvadd ?x312 (bvxor (bvxor ?x330 ?x324) ?x318)) (_ bv0 32)) (_ bv1859775393 32)) (_ bv11 32))))
 (let ((?x342 (ext_rotate_left (bvadd (bvadd (bvadd ?x318 (bvxor (bvxor ?x336 ?x330) ?x324)) (_ bv0 32)) (_ bv1859775393 32)) (_ bv15 32))))
 (let ((?x347 (bvadd (bvadd (bvadd ?x324 (bvxor (bvxor ?x342 ?x336) ?x330)) ch_3) (_ bv1859775393 32))))
 (let ((?x348 (ext_rotate_left ?x347 (_ bv3 32))))
 (= ch_0 (bvadd (_ bv1732584193 32) ?x348))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(assert
 (let ((?x26 (bvadd (bvadd (_ bv1732584193 32) (bvor (bvand (_ bv4023233417 32) (_ bv2562383102 32)) (bvand (bvnot (_ bv4023233417 32)) (_ bv271733878 32)))) ch_0)))
 (let ((?x28 (ext_rotate_left ?x26 (_ bv3 32))))
 (let ((?x34 (bvadd (bvadd (_ bv271733878 32) (bvor (bvand ?x28 (_ bv4023233417 32)) (bvand (bvnot ?x28) (_ bv2562383102 32)))) ch_1)))
 (let ((?x36 (ext_rotate_left ?x34 (_ bv7 32))))
 (let ((?x42 (bvadd (bvadd (_ bv2562383102 32) (bvor (bvand ?x36 ?x28) (bvand (bvnot ?x36) (_ bv4023233417 32)))) ch_2)))
 (let ((?x44 (ext_rotate_left ?x42 (_ bv11 32))))
 (let ((?x50 (bvadd (bvadd (_ bv4023233417 32) (bvor (bvand ?x44 ?x36) (bvand (bvnot ?x44) ?x28))) ch_3)))
 (let ((?x52 (ext_rotate_left ?x50 (_ bv19 32))))
 (let ((?x58 (bvadd (bvadd ?x28 (bvor (bvand ?x52 ?x44) (bvand (bvnot ?x52) ?x36))) (_ bv128 32))))
 (let ((?x59 (ext_rotate_left ?x58 (_ bv3 32))))
 (let ((?x65 (bvadd (bvadd ?x36 (bvor (bvand ?x59 ?x52) (bvand (bvnot ?x59) ?x44))) (_ bv0 32))))
 (let ((?x66 (ext_rotate_left ?x65 (_ bv7 32))))
 (let ((?x72 (bvadd (bvadd ?x44 (bvor (bvand ?x66 ?x59) (bvand (bvnot ?x66) ?x52))) (_ bv0 32))))
 (let ((?x73 (ext_rotate_left ?x72 (_ bv11 32))))
 (let ((?x79 (bvadd (bvadd ?x52 (bvor (bvand ?x73 ?x66) (bvand (bvnot ?x73) ?x59))) (_ bv0 32))))
 (let ((?x80 (ext_rotate_left ?x79 (_ bv19 32))))
 (let ((?x86 (bvadd (bvadd ?x59 (bvor (bvand ?x80 ?x73) (bvand (bvnot ?x80) ?x66))) (_ bv0 32))))
 (let ((?x87 (ext_rotate_left ?x86 (_ bv3 32))))
 (let ((?x93 (bvadd (bvadd ?x66 (bvor (bvand ?x87 ?x80) (bvand (bvnot ?x87) ?x73))) (_ bv0 32))))
 (let ((?x94 (ext_rotate_left ?x93 (_ bv7 32))))
 (let ((?x100 (bvadd (bvadd ?x73 (bvor (bvand ?x94 ?x87) (bvand (bvnot ?x94) ?x80))) (_ bv0 32))))
 (let ((?x101 (ext_rotate_left ?x100 (_ bv11 32))))
 (let ((?x107 (bvadd (bvadd ?x80 (bvor (bvand ?x101 ?x94) (bvand (bvnot ?x101) ?x87))) (_ bv0 32))))
 (let ((?x108 (ext_rotate_left ?x107 (_ bv19 32))))
 (let ((?x114 (bvadd (bvadd ?x87 (bvor (bvand ?x108 ?x101) (bvand (bvnot ?x108) ?x94))) (_ bv0 32))))
 (let ((?x115 (ext_rotate_left ?x114 (_ bv3 32))))
 (let ((?x121 (bvadd (bvadd ?x94 (bvor (bvand ?x115 ?x108) (bvand (bvnot ?x115) ?x101))) (_ bv0 32))))
 (let ((?x122 (ext_rotate_left ?x121 (_ bv7 32))))
 (let ((?x128 (bvadd (bvadd ?x101 (bvor (bvand ?x122 ?x115) (bvand (bvnot ?x122) ?x108))) (_ bv128 32))))
 (let ((?x129 (ext_rotate_left ?x128 (_ bv11 32))))
 (let ((?x135 (bvadd (bvadd ?x108 (bvor (bvand ?x129 ?x122) (bvand (bvnot ?x129) ?x115))) (_ bv0 32))))
 (let ((?x136 (ext_rotate_left ?x135 (_ bv19 32))))
 (let ((?x141 (bvadd ?x115 (bvor (bvor (bvand ?x136 ?x129) (bvand ?x136 ?x122)) (bvand ?x129 ?x122)))))
 (let ((?x145 (ext_rotate_left (bvadd (bvadd ?x141 ch_0) (_ bv1518500249 32)) (_ bv3 32))))
 (let ((?x150 (bvadd ?x122 (bvor (bvor (bvand ?x145 ?x136) (bvand ?x145 ?x129)) (bvand ?x136 ?x129)))))
 (let ((?x154 (ext_rotate_left (bvadd (bvadd ?x150 (_ bv128 32)) (_ bv1518500249 32)) (_ bv5 32))))
 (let ((?x159 (bvadd ?x129 (bvor (bvor (bvand ?x154 ?x145) (bvand ?x154 ?x136)) (bvand ?x145 ?x136)))))
 (let ((?x163 (ext_rotate_left (bvadd (bvadd ?x159 (_ bv0 32)) (_ bv1518500249 32)) (_ bv9 32))))
 (let ((?x168 (bvadd ?x136 (bvor (bvor (bvand ?x163 ?x154) (bvand ?x163 ?x145)) (bvand ?x154 ?x145)))))
 (let ((?x172 (ext_rotate_left (bvadd (bvadd ?x168 (_ bv0 32)) (_ bv1518500249 32)) (_ bv13 32))))
 (let ((?x177 (bvadd ?x145 (bvor (bvor (bvand ?x172 ?x163) (bvand ?x172 ?x154)) (bvand ?x163 ?x154)))))
 (let ((?x180 (ext_rotate_left (bvadd (bvadd ?x177 ch_1) (_ bv1518500249 32)) (_ bv3 32))))
 (let ((?x185 (bvadd ?x154 (bvor (bvor (bvand ?x180 ?x172) (bvand ?x180 ?x163)) (bvand ?x172 ?x163)))))
 (let ((?x188 (ext_rotate_left (bvadd (bvadd ?x185 (_ bv0 32)) (_ bv1518500249 32)) (_ bv5 32))))
 (let ((?x193 (bvadd ?x163 (bvor (bvor (bvand ?x188 ?x180) (bvand ?x188 ?x172)) (bvand ?x180 ?x172)))))
 (let ((?x196 (ext_rotate_left (bvadd (bvadd ?x193 (_ bv0 32)) (_ bv1518500249 32)) (_ bv9 32))))
 (let ((?x201 (bvadd ?x172 (bvor (bvor (bvand ?x196 ?x188) (bvand ?x196 ?x180)) (bvand ?x188 ?x180)))))
 (let ((?x204 (ext_rotate_left (bvadd (bvadd ?x201 (_ bv0 32)) (_ bv1518500249 32)) (_ bv13 32))))
 (let ((?x209 (bvadd ?x180 (bvor (bvor (bvand ?x204 ?x196) (bvand ?x204 ?x188)) (bvand ?x196 ?x188)))))
 (let ((?x212 (ext_rotate_left (bvadd (bvadd ?x209 ch_2) (_ bv1518500249 32)) (_ bv3 32))))
 (let ((?x217 (bvadd ?x188 (bvor (bvor (bvand ?x212 ?x204) (bvand ?x212 ?x196)) (bvand ?x204 ?x196)))))
 (let ((?x220 (ext_rotate_left (bvadd (bvadd ?x217 (_ bv0 32)) (_ bv1518500249 32)) (_ bv5 32))))
 (let ((?x225 (bvadd ?x196 (bvor (bvor (bvand ?x220 ?x212) (bvand ?x220 ?x204)) (bvand ?x212 ?x204)))))
 (let ((?x228 (ext_rotate_left (bvadd (bvadd ?x225 (_ bv0 32)) (_ bv1518500249 32)) (_ bv9 32))))
 (let ((?x233 (bvadd ?x204 (bvor (bvor (bvand ?x228 ?x220) (bvand ?x228 ?x212)) (bvand ?x220 ?x212)))))
 (let ((?x236 (ext_rotate_left (bvadd (bvadd ?x233 (_ bv128 32)) (_ bv1518500249 32)) (_ bv13 32))))
 (let ((?x241 (bvadd ?x212 (bvor (bvor (bvand ?x236 ?x228) (bvand ?x236 ?x220)) (bvand ?x228 ?x220)))))
 (let ((?x244 (ext_rotate_left (bvadd (bvadd ?x241 ch_3) (_ bv1518500249 32)) (_ bv3 32))))
 (let ((?x249 (bvadd ?x220 (bvor (bvor (bvand ?x244 ?x236) (bvand ?x244 ?x228)) (bvand ?x236 ?x228)))))
 (let ((?x252 (ext_rotate_left (bvadd (bvadd ?x249 (_ bv0 32)) (_ bv1518500249 32)) (_ bv5 32))))
 (let ((?x257 (bvadd ?x228 (bvor (bvor (bvand ?x252 ?x244) (bvand ?x252 ?x236)) (bvand ?x244 ?x236)))))
 (let ((?x260 (ext_rotate_left (bvadd (bvadd ?x257 (_ bv0 32)) (_ bv1518500249 32)) (_ bv9 32))))
 (let ((?x265 (bvadd ?x236 (bvor (bvor (bvand ?x260 ?x252) (bvand ?x260 ?x244)) (bvand ?x252 ?x244)))))
 (let ((?x268 (ext_rotate_left (bvadd (bvadd ?x265 (_ bv0 32)) (_ bv1518500249 32)) (_ bv13 32))))
 (let ((?x274 (bvadd (bvadd (bvadd ?x244 (bvxor (bvxor ?x268 ?x260) ?x252)) ch_0) (_ bv1859775393 32))))
 (let ((?x275 (ext_rotate_left ?x274 (_ bv3 32))))
 (let ((?x281 (ext_rotate_left (bvadd (bvadd (bvadd ?x252 (bvxor (bvxor ?x275 ?x268) ?x260)) (_ bv0 32)) (_ bv1859775393 32)) (_ bv9 32))))
 (let ((?x287 (ext_rotate_left (bvadd (bvadd (bvadd ?x260 (bvxor (bvxor ?x281 ?x275) ?x268)) (_ bv128 32)) (_ bv1859775393 32)) (_ bv11 32))))
 (let ((?x294 (ext_rotate_left (bvadd (bvadd (bvadd ?x268 (bvxor (bvxor ?x287 ?x281) ?x275)) (_ bv0 32)) (_ bv1859775393 32)) (_ bv15 32))))
 (let ((?x299 (bvadd (bvadd (bvadd ?x275 (bvxor (bvxor ?x294 ?x287) ?x281)) ch_2) (_ bv1859775393 32))))
 (let ((?x300 (ext_rotate_left ?x299 (_ bv3 32))))
 (let ((?x306 (ext_rotate_left (bvadd (bvadd (bvadd ?x281 (bvxor (bvxor ?x300 ?x294) ?x287)) (_ bv0 32)) (_ bv1859775393 32)) (_ bv9 32))))
 (let ((?x312 (ext_rotate_left (bvadd (bvadd (bvadd ?x287 (bvxor (bvxor ?x306 ?x300) ?x294)) (_ bv0 32)) (_ bv1859775393 32)) (_ bv11 32))))
 (let ((?x318 (ext_rotate_left (bvadd (bvadd (bvadd ?x294 (bvxor (bvxor ?x312 ?x306) ?x300)) (_ bv128 32)) (_ bv1859775393 32)) (_ bv15 32))))
 (let ((?x323 (bvadd (bvadd (bvadd ?x300 (bvxor (bvxor ?x318 ?x312) ?x306)) ch_1) (_ bv1859775393 32))))
 (let ((?x324 (ext_rotate_left ?x323 (_ bv3 32))))
 (let ((?x330 (ext_rotate_left (bvadd (bvadd (bvadd ?x306 (bvxor (bvxor ?x324 ?x318) ?x312)) (_ bv0 32)) (_ bv1859775393 32)) (_ bv9 32))))
 (let ((?x336 (ext_rotate_left (bvadd (bvadd (bvadd ?x312 (bvxor (bvxor ?x330 ?x324) ?x318)) (_ bv0 32)) (_ bv1859775393 32)) (_ bv11 32))))
 (let ((?x342 (ext_rotate_left (bvadd (bvadd (bvadd ?x318 (bvxor (bvxor ?x336 ?x330) ?x324)) (_ bv0 32)) (_ bv1859775393 32)) (_ bv15 32))))
 (let ((?x347 (bvadd (bvadd (bvadd ?x324 (bvxor (bvxor ?x342 ?x336) ?x330)) ch_3) (_ bv1859775393 32))))
 (let ((?x348 (ext_rotate_left ?x347 (_ bv3 32))))
 (let ((?x354 (ext_rotate_left (bvadd (bvadd (bvadd ?x330 (bvxor (bvxor ?x348 ?x342) ?x336)) (_ bv0 32)) (_ bv1859775393 32)) (_ bv9 32))))
 (let ((?x360 (ext_rotate_left (bvadd (bvadd (bvadd ?x336 (bvxor (bvxor ?x354 ?x348) ?x342)) (_ bv0 32)) (_ bv1859775393 32)) (_ bv11 32))))
 (let ((?x366 (ext_rotate_left (bvadd (bvadd (bvadd ?x342 (bvxor (bvxor ?x360 ?x354) ?x348)) (_ bv0 32)) (_ bv1859775393 32)) (_ bv15 32))))
 (= ch_1 (bvadd (_ bv4023233417 32) ?x366)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(assert
 (let ((?x26 (bvadd (bvadd (_ bv1732584193 32) (bvor (bvand (_ bv4023233417 32) (_ bv2562383102 32)) (bvand (bvnot (_ bv4023233417 32)) (_ bv271733878 32)))) ch_0)))
 (let ((?x28 (ext_rotate_left ?x26 (_ bv3 32))))
 (let ((?x34 (bvadd (bvadd (_ bv271733878 32) (bvor (bvand ?x28 (_ bv4023233417 32)) (bvand (bvnot ?x28) (_ bv2562383102 32)))) ch_1)))
 (let ((?x36 (ext_rotate_left ?x34 (_ bv7 32))))
 (let ((?x42 (bvadd (bvadd (_ bv2562383102 32) (bvor (bvand ?x36 ?x28) (bvand (bvnot ?x36) (_ bv4023233417 32)))) ch_2)))
 (let ((?x44 (ext_rotate_left ?x42 (_ bv11 32))))
 (let ((?x50 (bvadd (bvadd (_ bv4023233417 32) (bvor (bvand ?x44 ?x36) (bvand (bvnot ?x44) ?x28))) ch_3)))
 (let ((?x52 (ext_rotate_left ?x50 (_ bv19 32))))
 (let ((?x58 (bvadd (bvadd ?x28 (bvor (bvand ?x52 ?x44) (bvand (bvnot ?x52) ?x36))) (_ bv128 32))))
 (let ((?x59 (ext_rotate_left ?x58 (_ bv3 32))))
 (let ((?x65 (bvadd (bvadd ?x36 (bvor (bvand ?x59 ?x52) (bvand (bvnot ?x59) ?x44))) (_ bv0 32))))
 (let ((?x66 (ext_rotate_left ?x65 (_ bv7 32))))
 (let ((?x72 (bvadd (bvadd ?x44 (bvor (bvand ?x66 ?x59) (bvand (bvnot ?x66) ?x52))) (_ bv0 32))))
 (let ((?x73 (ext_rotate_left ?x72 (_ bv11 32))))
 (let ((?x79 (bvadd (bvadd ?x52 (bvor (bvand ?x73 ?x66) (bvand (bvnot ?x73) ?x59))) (_ bv0 32))))
 (let ((?x80 (ext_rotate_left ?x79 (_ bv19 32))))
 (let ((?x86 (bvadd (bvadd ?x59 (bvor (bvand ?x80 ?x73) (bvand (bvnot ?x80) ?x66))) (_ bv0 32))))
 (let ((?x87 (ext_rotate_left ?x86 (_ bv3 32))))
 (let ((?x93 (bvadd (bvadd ?x66 (bvor (bvand ?x87 ?x80) (bvand (bvnot ?x87) ?x73))) (_ bv0 32))))
 (let ((?x94 (ext_rotate_left ?x93 (_ bv7 32))))
 (let ((?x100 (bvadd (bvadd ?x73 (bvor (bvand ?x94 ?x87) (bvand (bvnot ?x94) ?x80))) (_ bv0 32))))
 (let ((?x101 (ext_rotate_left ?x100 (_ bv11 32))))
 (let ((?x107 (bvadd (bvadd ?x80 (bvor (bvand ?x101 ?x94) (bvand (bvnot ?x101) ?x87))) (_ bv0 32))))
 (let ((?x108 (ext_rotate_left ?x107 (_ bv19 32))))
 (let ((?x114 (bvadd (bvadd ?x87 (bvor (bvand ?x108 ?x101) (bvand (bvnot ?x108) ?x94))) (_ bv0 32))))
 (let ((?x115 (ext_rotate_left ?x114 (_ bv3 32))))
 (let ((?x121 (bvadd (bvadd ?x94 (bvor (bvand ?x115 ?x108) (bvand (bvnot ?x115) ?x101))) (_ bv0 32))))
 (let ((?x122 (ext_rotate_left ?x121 (_ bv7 32))))
 (let ((?x128 (bvadd (bvadd ?x101 (bvor (bvand ?x122 ?x115) (bvand (bvnot ?x122) ?x108))) (_ bv128 32))))
 (let ((?x129 (ext_rotate_left ?x128 (_ bv11 32))))
 (let ((?x135 (bvadd (bvadd ?x108 (bvor (bvand ?x129 ?x122) (bvand (bvnot ?x129) ?x115))) (_ bv0 32))))
 (let ((?x136 (ext_rotate_left ?x135 (_ bv19 32))))
 (let ((?x141 (bvadd ?x115 (bvor (bvor (bvand ?x136 ?x129) (bvand ?x136 ?x122)) (bvand ?x129 ?x122)))))
 (let ((?x145 (ext_rotate_left (bvadd (bvadd ?x141 ch_0) (_ bv1518500249 32)) (_ bv3 32))))
 (let ((?x150 (bvadd ?x122 (bvor (bvor (bvand ?x145 ?x136) (bvand ?x145 ?x129)) (bvand ?x136 ?x129)))))
 (let ((?x154 (ext_rotate_left (bvadd (bvadd ?x150 (_ bv128 32)) (_ bv1518500249 32)) (_ bv5 32))))
 (let ((?x159 (bvadd ?x129 (bvor (bvor (bvand ?x154 ?x145) (bvand ?x154 ?x136)) (bvand ?x145 ?x136)))))
 (let ((?x163 (ext_rotate_left (bvadd (bvadd ?x159 (_ bv0 32)) (_ bv1518500249 32)) (_ bv9 32))))
 (let ((?x168 (bvadd ?x136 (bvor (bvor (bvand ?x163 ?x154) (bvand ?x163 ?x145)) (bvand ?x154 ?x145)))))
 (let ((?x172 (ext_rotate_left (bvadd (bvadd ?x168 (_ bv0 32)) (_ bv1518500249 32)) (_ bv13 32))))
 (let ((?x177 (bvadd ?x145 (bvor (bvor (bvand ?x172 ?x163) (bvand ?x172 ?x154)) (bvand ?x163 ?x154)))))
 (let ((?x180 (ext_rotate_left (bvadd (bvadd ?x177 ch_1) (_ bv1518500249 32)) (_ bv3 32))))
 (let ((?x185 (bvadd ?x154 (bvor (bvor (bvand ?x180 ?x172) (bvand ?x180 ?x163)) (bvand ?x172 ?x163)))))
 (let ((?x188 (ext_rotate_left (bvadd (bvadd ?x185 (_ bv0 32)) (_ bv1518500249 32)) (_ bv5 32))))
 (let ((?x193 (bvadd ?x163 (bvor (bvor (bvand ?x188 ?x180) (bvand ?x188 ?x172)) (bvand ?x180 ?x172)))))
 (let ((?x196 (ext_rotate_left (bvadd (bvadd ?x193 (_ bv0 32)) (_ bv1518500249 32)) (_ bv9 32))))
 (let ((?x201 (bvadd ?x172 (bvor (bvor (bvand ?x196 ?x188) (bvand ?x196 ?x180)) (bvand ?x188 ?x180)))))
 (let ((?x204 (ext_rotate_left (bvadd (bvadd ?x201 (_ bv0 32)) (_ bv1518500249 32)) (_ bv13 32))))
 (let ((?x209 (bvadd ?x180 (bvor (bvor (bvand ?x204 ?x196) (bvand ?x204 ?x188)) (bvand ?x196 ?x188)))))
 (let ((?x212 (ext_rotate_left (bvadd (bvadd ?x209 ch_2) (_ bv1518500249 32)) (_ bv3 32))))
 (let ((?x217 (bvadd ?x188 (bvor (bvor (bvand ?x212 ?x204) (bvand ?x212 ?x196)) (bvand ?x204 ?x196)))))
 (let ((?x220 (ext_rotate_left (bvadd (bvadd ?x217 (_ bv0 32)) (_ bv1518500249 32)) (_ bv5 32))))
 (let ((?x225 (bvadd ?x196 (bvor (bvor (bvand ?x220 ?x212) (bvand ?x220 ?x204)) (bvand ?x212 ?x204)))))
 (let ((?x228 (ext_rotate_left (bvadd (bvadd ?x225 (_ bv0 32)) (_ bv1518500249 32)) (_ bv9 32))))
 (let ((?x233 (bvadd ?x204 (bvor (bvor (bvand ?x228 ?x220) (bvand ?x228 ?x212)) (bvand ?x220 ?x212)))))
 (let ((?x236 (ext_rotate_left (bvadd (bvadd ?x233 (_ bv128 32)) (_ bv1518500249 32)) (_ bv13 32))))
 (let ((?x241 (bvadd ?x212 (bvor (bvor (bvand ?x236 ?x228) (bvand ?x236 ?x220)) (bvand ?x228 ?x220)))))
 (let ((?x244 (ext_rotate_left (bvadd (bvadd ?x241 ch_3) (_ bv1518500249 32)) (_ bv3 32))))
 (let ((?x249 (bvadd ?x220 (bvor (bvor (bvand ?x244 ?x236) (bvand ?x244 ?x228)) (bvand ?x236 ?x228)))))
 (let ((?x252 (ext_rotate_left (bvadd (bvadd ?x249 (_ bv0 32)) (_ bv1518500249 32)) (_ bv5 32))))
 (let ((?x257 (bvadd ?x228 (bvor (bvor (bvand ?x252 ?x244) (bvand ?x252 ?x236)) (bvand ?x244 ?x236)))))
 (let ((?x260 (ext_rotate_left (bvadd (bvadd ?x257 (_ bv0 32)) (_ bv1518500249 32)) (_ bv9 32))))
 (let ((?x265 (bvadd ?x236 (bvor (bvor (bvand ?x260 ?x252) (bvand ?x260 ?x244)) (bvand ?x252 ?x244)))))
 (let ((?x268 (ext_rotate_left (bvadd (bvadd ?x265 (_ bv0 32)) (_ bv1518500249 32)) (_ bv13 32))))
 (let ((?x274 (bvadd (bvadd (bvadd ?x244 (bvxor (bvxor ?x268 ?x260) ?x252)) ch_0) (_ bv1859775393 32))))
 (let ((?x275 (ext_rotate_left ?x274 (_ bv3 32))))
 (let ((?x281 (ext_rotate_left (bvadd (bvadd (bvadd ?x252 (bvxor (bvxor ?x275 ?x268) ?x260)) (_ bv0 32)) (_ bv1859775393 32)) (_ bv9 32))))
 (let ((?x287 (ext_rotate_left (bvadd (bvadd (bvadd ?x260 (bvxor (bvxor ?x281 ?x275) ?x268)) (_ bv128 32)) (_ bv1859775393 32)) (_ bv11 32))))
 (let ((?x294 (ext_rotate_left (bvadd (bvadd (bvadd ?x268 (bvxor (bvxor ?x287 ?x281) ?x275)) (_ bv0 32)) (_ bv1859775393 32)) (_ bv15 32))))
 (let ((?x299 (bvadd (bvadd (bvadd ?x275 (bvxor (bvxor ?x294 ?x287) ?x281)) ch_2) (_ bv1859775393 32))))
 (let ((?x300 (ext_rotate_left ?x299 (_ bv3 32))))
 (let ((?x306 (ext_rotate_left (bvadd (bvadd (bvadd ?x281 (bvxor (bvxor ?x300 ?x294) ?x287)) (_ bv0 32)) (_ bv1859775393 32)) (_ bv9 32))))
 (let ((?x312 (ext_rotate_left (bvadd (bvadd (bvadd ?x287 (bvxor (bvxor ?x306 ?x300) ?x294)) (_ bv0 32)) (_ bv1859775393 32)) (_ bv11 32))))
 (let ((?x318 (ext_rotate_left (bvadd (bvadd (bvadd ?x294 (bvxor (bvxor ?x312 ?x306) ?x300)) (_ bv128 32)) (_ bv1859775393 32)) (_ bv15 32))))
 (let ((?x323 (bvadd (bvadd (bvadd ?x300 (bvxor (bvxor ?x318 ?x312) ?x306)) ch_1) (_ bv1859775393 32))))
 (let ((?x324 (ext_rotate_left ?x323 (_ bv3 32))))
 (let ((?x330 (ext_rotate_left (bvadd (bvadd (bvadd ?x306 (bvxor (bvxor ?x324 ?x318) ?x312)) (_ bv0 32)) (_ bv1859775393 32)) (_ bv9 32))))
 (let ((?x336 (ext_rotate_left (bvadd (bvadd (bvadd ?x312 (bvxor (bvxor ?x330 ?x324) ?x318)) (_ bv0 32)) (_ bv1859775393 32)) (_ bv11 32))))
 (let ((?x342 (ext_rotate_left (bvadd (bvadd (bvadd ?x318 (bvxor (bvxor ?x336 ?x330) ?x324)) (_ bv0 32)) (_ bv1859775393 32)) (_ bv15 32))))
 (let ((?x347 (bvadd (bvadd (bvadd ?x324 (bvxor (bvxor ?x342 ?x336) ?x330)) ch_3) (_ bv1859775393 32))))
 (let ((?x348 (ext_rotate_left ?x347 (_ bv3 32))))
 (let ((?x354 (ext_rotate_left (bvadd (bvadd (bvadd ?x330 (bvxor (bvxor ?x348 ?x342) ?x336)) (_ bv0 32)) (_ bv1859775393 32)) (_ bv9 32))))
 (let ((?x360 (ext_rotate_left (bvadd (bvadd (bvadd ?x336 (bvxor (bvxor ?x354 ?x348) ?x342)) (_ bv0 32)) (_ bv1859775393 32)) (_ bv11 32))))
 (= ch_2 (bvadd (_ bv2562383102 32) ?x360))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(assert
 (let ((?x26 (bvadd (bvadd (_ bv1732584193 32) (bvor (bvand (_ bv4023233417 32) (_ bv2562383102 32)) (bvand (bvnot (_ bv4023233417 32)) (_ bv271733878 32)))) ch_0)))
(let ((?x28 (ext_rotate_left ?x26 (_ bv3 32))))
(let ((?x34 (bvadd (bvadd (_ bv271733878 32) (bvor (bvand ?x28 (_ bv4023233417 32)) (bvand (bvnot ?x28) (_ bv2562383102 32)))) ch_1)))
(let ((?x36 (ext_rotate_left ?x34 (_ bv7 32))))
(let ((?x42 (bvadd (bvadd (_ bv2562383102 32) (bvor (bvand ?x36 ?x28) (bvand (bvnot ?x36) (_ bv4023233417 32)))) ch_2)))
(let ((?x44 (ext_rotate_left ?x42 (_ bv11 32))))
(let ((?x50 (bvadd (bvadd (_ bv4023233417 32) (bvor (bvand ?x44 ?x36) (bvand (bvnot ?x44) ?x28))) ch_3)))
(let ((?x52 (ext_rotate_left ?x50 (_ bv19 32))))
(let ((?x58 (bvadd (bvadd ?x28 (bvor (bvand ?x52 ?x44) (bvand (bvnot ?x52) ?x36))) (_ bv128 32))))
(let ((?x59 (ext_rotate_left ?x58 (_ bv3 32))))
(let ((?x65 (bvadd (bvadd ?x36 (bvor (bvand ?x59 ?x52) (bvand (bvnot ?x59) ?x44))) (_ bv0 32))))
(let ((?x66 (ext_rotate_left ?x65 (_ bv7 32))))
(let ((?x72 (bvadd (bvadd ?x44 (bvor (bvand ?x66 ?x59) (bvand (bvnot ?x66) ?x52))) (_ bv0 32))))
(let ((?x73 (ext_rotate_left ?x72 (_ bv11 32))))
(let ((?x79 (bvadd (bvadd ?x52 (bvor (bvand ?x73 ?x66) (bvand (bvnot ?x73) ?x59))) (_ bv0 32))))
(let ((?x80 (ext_rotate_left ?x79 (_ bv19 32))))
(let ((?x86 (bvadd (bvadd ?x59 (bvor (bvand ?x80 ?x73) (bvand (bvnot ?x80) ?x66))) (_ bv0 32))))
(let ((?x87 (ext_rotate_left ?x86 (_ bv3 32))))
(let ((?x93 (bvadd (bvadd ?x66 (bvor (bvand ?x87 ?x80) (bvand (bvnot ?x87) ?x73))) (_ bv0 32))))
(let ((?x94 (ext_rotate_left ?x93 (_ bv7 32))))
(let ((?x100 (bvadd (bvadd ?x73 (bvor (bvand ?x94 ?x87) (bvand (bvnot ?x94) ?x80))) (_ bv0 32))))
(let ((?x101 (ext_rotate_left ?x100 (_ bv11 32))))
(let ((?x107 (bvadd (bvadd ?x80 (bvor (bvand ?x101 ?x94) (bvand (bvnot ?x101) ?x87))) (_ bv0 32))))
(let ((?x108 (ext_rotate_left ?x107 (_ bv19 32))))
(let ((?x114 (bvadd (bvadd ?x87 (bvor (bvand ?x108 ?x101) (bvand (bvnot ?x108) ?x94))) (_ bv0 32))))
(let ((?x115 (ext_rotate_left ?x114 (_ bv3 32))))
(let ((?x121 (bvadd (bvadd ?x94 (bvor (bvand ?x115 ?x108) (bvand (bvnot ?x115) ?x101))) (_ bv0 32))))
(let ((?x122 (ext_rotate_left ?x121 (_ bv7 32))))
(let ((?x128 (bvadd (bvadd ?x101 (bvor (bvand ?x122 ?x115) (bvand (bvnot ?x122) ?x108))) (_ bv128 32))))
(let ((?x129 (ext_rotate_left ?x128 (_ bv11 32))))
(let ((?x135 (bvadd (bvadd ?x108 (bvor (bvand ?x129 ?x122) (bvand (bvnot ?x129) ?x115))) (_ bv0 32))))
(let ((?x136 (ext_rotate_left ?x135 (_ bv19 32))))
(let ((?x141 (bvadd ?x115 (bvor (bvor (bvand ?x136 ?x129) (bvand ?x136 ?x122)) (bvand ?x129 ?x122)))))
(let ((?x145 (ext_rotate_left (bvadd (bvadd ?x141 ch_0) (_ bv1518500249 32)) (_ bv3 32))))
(let ((?x150 (bvadd ?x122 (bvor (bvor (bvand ?x145 ?x136) (bvand ?x145 ?x129)) (bvand ?x136 ?x129)))))
(let ((?x154 (ext_rotate_left (bvadd (bvadd ?x150 (_ bv128 32)) (_ bv1518500249 32)) (_ bv5 32))))
(let ((?x159 (bvadd ?x129 (bvor (bvor (bvand ?x154 ?x145) (bvand ?x154 ?x136)) (bvand ?x145 ?x136)))))
(let ((?x163 (ext_rotate_left (bvadd (bvadd ?x159 (_ bv0 32)) (_ bv1518500249 32)) (_ bv9 32))))
(let ((?x168 (bvadd ?x136 (bvor (bvor (bvand ?x163 ?x154) (bvand ?x163 ?x145)) (bvand ?x154 ?x145)))))
(let ((?x172 (ext_rotate_left (bvadd (bvadd ?x168 (_ bv0 32)) (_ bv1518500249 32)) (_ bv13 32))))
(let ((?x177 (bvadd ?x145 (bvor (bvor (bvand ?x172 ?x163) (bvand ?x172 ?x154)) (bvand ?x163 ?x154)))))
(let ((?x180 (ext_rotate_left (bvadd (bvadd ?x177 ch_1) (_ bv1518500249 32)) (_ bv3 32))))
(let ((?x185 (bvadd ?x154 (bvor (bvor (bvand ?x180 ?x172) (bvand ?x180 ?x163)) (bvand ?x172 ?x163)))))
(let ((?x188 (ext_rotate_left (bvadd (bvadd ?x185 (_ bv0 32)) (_ bv1518500249 32)) (_ bv5 32))))
(let ((?x193 (bvadd ?x163 (bvor (bvor (bvand ?x188 ?x180) (bvand ?x188 ?x172)) (bvand ?x180 ?x172)))))
(let ((?x196 (ext_rotate_left (bvadd (bvadd ?x193 (_ bv0 32)) (_ bv1518500249 32)) (_ bv9 32))))
(let ((?x201 (bvadd ?x172 (bvor (bvor (bvand ?x196 ?x188) (bvand ?x196 ?x180)) (bvand ?x188 ?x180)))))
(let ((?x204 (ext_rotate_left (bvadd (bvadd ?x201 (_ bv0 32)) (_ bv1518500249 32)) (_ bv13 32))))
(let ((?x209 (bvadd ?x180 (bvor (bvor (bvand ?x204 ?x196) (bvand ?x204 ?x188)) (bvand ?x196 ?x188)))))
(let ((?x212 (ext_rotate_left (bvadd (bvadd ?x209 ch_2) (_ bv1518500249 32)) (_ bv3 32))))
(let ((?x217 (bvadd ?x188 (bvor (bvor (bvand ?x212 ?x204) (bvand ?x212 ?x196)) (bvand ?x204 ?x196)))))
(let ((?x220 (ext_rotate_left (bvadd (bvadd ?x217 (_ bv0 32)) (_ bv1518500249 32)) (_ bv5 32))))
(let ((?x225 (bvadd ?x196 (bvor (bvor (bvand ?x220 ?x212) (bvand ?x220 ?x204)) (bvand ?x212 ?x204)))))
(let ((?x228 (ext_rotate_left (bvadd (bvadd ?x225 (_ bv0 32)) (_ bv1518500249 32)) (_ bv9 32))))
(let ((?x233 (bvadd ?x204 (bvor (bvor (bvand ?x228 ?x220) (bvand ?x228 ?x212)) (bvand ?x220 ?x212)))))
(let ((?x236 (ext_rotate_left (bvadd (bvadd ?x233 (_ bv128 32)) (_ bv1518500249 32)) (_ bv13 32))))
(let ((?x241 (bvadd ?x212 (bvor (bvor (bvand ?x236 ?x228) (bvand ?x236 ?x220)) (bvand ?x228 ?x220)))))
(let ((?x244 (ext_rotate_left (bvadd (bvadd ?x241 ch_3) (_ bv1518500249 32)) (_ bv3 32))))
(let ((?x249 (bvadd ?x220 (bvor (bvor (bvand ?x244 ?x236) (bvand ?x244 ?x228)) (bvand ?x236 ?x228)))))
(let ((?x252 (ext_rotate_left (bvadd (bvadd ?x249 (_ bv0 32)) (_ bv1518500249 32)) (_ bv5 32))))
(let ((?x257 (bvadd ?x228 (bvor (bvor (bvand ?x252 ?x244) (bvand ?x252 ?x236)) (bvand ?x244 ?x236)))))
(let ((?x260 (ext_rotate_left (bvadd (bvadd ?x257 (_ bv0 32)) (_ bv1518500249 32)) (_ bv9 32))))
(let ((?x265 (bvadd ?x236 (bvor (bvor (bvand ?x260 ?x252) (bvand ?x260 ?x244)) (bvand ?x252 ?x244)))))
(let ((?x268 (ext_rotate_left (bvadd (bvadd ?x265 (_ bv0 32)) (_ bv1518500249 32)) (_ bv13 32))))
(let ((?x274 (bvadd (bvadd (bvadd ?x244 (bvxor (bvxor ?x268 ?x260) ?x252)) ch_0) (_ bv1859775393 32))))
(let ((?x275 (ext_rotate_left ?x274 (_ bv3 32))))
(let ((?x281 (ext_rotate_left (bvadd (bvadd (bvadd ?x252 (bvxor (bvxor ?x275 ?x268) ?x260)) (_ bv0 32)) (_ bv1859775393 32)) (_ bv9 32))))
(let ((?x287 (ext_rotate_left (bvadd (bvadd (bvadd ?x260 (bvxor (bvxor ?x281 ?x275) ?x268)) (_ bv128 32)) (_ bv1859775393 32)) (_ bv11 32))))
(let ((?x294 (ext_rotate_left (bvadd (bvadd (bvadd ?x268 (bvxor (bvxor ?x287 ?x281) ?x275)) (_ bv0 32)) (_ bv1859775393 32)) (_ bv15 32))))
(let ((?x299 (bvadd (bvadd (bvadd ?x275 (bvxor (bvxor ?x294 ?x287) ?x281)) ch_2) (_ bv1859775393 32))))
(let ((?x300 (ext_rotate_left ?x299 (_ bv3 32))))
(let ((?x306 (ext_rotate_left (bvadd (bvadd (bvadd ?x281 (bvxor (bvxor ?x300 ?x294) ?x287)) (_ bv0 32)) (_ bv1859775393 32)) (_ bv9 32))))
(let ((?x312 (ext_rotate_left (bvadd (bvadd (bvadd ?x287 (bvxor (bvxor ?x306 ?x300) ?x294)) (_ bv0 32)) (_ bv1859775393 32)) (_ bv11 32))))
(let ((?x318 (ext_rotate_left (bvadd (bvadd (bvadd ?x294 (bvxor (bvxor ?x312 ?x306) ?x300)) (_ bv128 32)) (_ bv1859775393 32)) (_ bv15 32))))
(let ((?x323 (bvadd (bvadd (bvadd ?x300 (bvxor (bvxor ?x318 ?x312) ?x306)) ch_1) (_ bv1859775393 32))))
(let ((?x324 (ext_rotate_left ?x323 (_ bv3 32))))
(let ((?x330 (ext_rotate_left (bvadd (bvadd (bvadd ?x306 (bvxor (bvxor ?x324 ?x318) ?x312)) (_ bv0 32)) (_ bv1859775393 32)) (_ bv9 32))))
(let ((?x336 (ext_rotate_left (bvadd (bvadd (bvadd ?x312 (bvxor (bvxor ?x330 ?x324) ?x318)) (_ bv0 32)) (_ bv1859775393 32)) (_ bv11 32))))
(let ((?x342 (ext_rotate_left (bvadd (bvadd (bvadd ?x318 (bvxor (bvxor ?x336 ?x330) ?x324)) (_ bv0 32)) (_ bv1859775393 32)) (_ bv15 32))))
(let ((?x347 (bvadd (bvadd (bvadd ?x324 (bvxor (bvxor ?x342 ?x336) ?x330)) ch_3) (_ bv1859775393 32))))
(let ((?x348 (ext_rotate_left ?x347 (_ bv3 32))))
(let ((?x354 (ext_rotate_left (bvadd (bvadd (bvadd ?x330 (bvxor (bvxor ?x348 ?x342) ?x336)) (_ bv0 32)) (_ bv1859775393 32)) (_ bv9 32))))
(= ch_3 (bvadd (_ bv271733878 32) ?x354)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

;;; Uncommenting this below will search with two different methods in parallel
(check-sat-using
  (par-or
   (using-params qfbv :random-seed 17283)
   (using-params qfbv-sls :random-seed 19121)))

;;; Otherwise only use one core
;; (check-sat-using
;; (using-params qfbv :random-seed 91919))

(get-model)