Reverse CRC64 with z3

decrc64.py

import z3

s = z3.Solver()
s.push()

poly = z3.BitVecVal(0xC96C5795D7870F42, 64)
goal = z3.BitVecVal(0x751092902dfa050e, 64)
ZERO = z3.BitVecVal(0, 64)
ONE  = z3.BitVecVal(1, 64)

unklen = 14
unknown = z3.BitVec("fn", unklen*8)
prefixstr = "system/scripts/"
suffixstr = ".lc"
prefixnum = sum(ord(c) << 8*i for i, c in enumerate(prefixstr))
prefix = z3.BitVecVal(prefixnum, len(prefixstr)*8)
suffixnum = sum(ord(c) << 8*i for i, c in enumerate(suffixstr))
suffix = z3.BitVecVal(suffixnum, len(suffixstr)*8)
full = z3.Concat(suffix, unknown, prefix)

crc = ~ZERO
for i in range(full.size()//8):
    c = z3.Extract(8*(i+1)-1, 8*i, full)

    if len(prefixstr) <= i < len(prefixstr)+unklen:
        s.add(c >= z3.BitVecVal(ord('a'), 8))
        s.add(c <= z3.BitVecVal(ord('z'), 8))

    crc = z3.simplify(crc ^ z3.ZeroExt(56, c))
    for k in range(8):
        crc = z3.If(z3.Extract(0, 0, crc) != 0, # faster now
            z3.LShR(crc, ONE) ^ poly,
            z3.LShR(crc, ONE))

s.add(crc == goal)

while s.check() == z3.sat:
    m = s.model()
    r = m.eval(unknown, True)
    s.add(unknown != r)

    print("".join(chr((r.as_long() >> 8*i) & 0xff) 
        for i in range(unklen)))