Last active
October 6, 2017 23:26
-
-
Save zv/750c90c82832f42b24b83430077b08e5 to your computer and use it in GitHub Desktop.
Find MD4 fixed points with with less thab 2^(128/2)/16 decisions & conflicts!
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
(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) |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment