What an annoying task. There are multiple valid solutionsThe serial key is taken as `argv[1]` is of the format `dddd_dddd_dddd_dddd`Here's my z3 script
```from z3 import *from hashlib import md5
"""    `get_models` returns atmost M solutions https://stackoverflow.com/questions/11867611/z3py-checking-all-solutions-for-equation"""def get_models(F, M):    s = Solver()    count = 0    s.add(F)    while count < M and s.check() == sat:        m = s.model()        count += 1        yield m        # Create a new constraint the blocks the current model        block = []        for d in m:            # d is a declaration            if d.arity() > 0:                raise Z3Exception("uninterpreted functions are not supported")            # create a constant from declaration            c = d()            if is_array(c) or c.sort().kind() == Z3_UNINTERPRETED_SORT:                raise Z3Exception("arrays and uninterpreted sorts are not supported")            block.append(c != m[d])        s.add(Or(block))
d = [BitVec('i%d' % i, 16) for i in xrange(19)]#s = Solver()s = []
for i in xrange(4):    s.append(And(d[i] > 0, d[i] <= 9))    s.append(And(d[i+5] > 1, d[i+5] < 9))    s.append(And(d[i+10] >= 0, d[i+10] <= 9))    s.append(And(d[i+15] > 2, d[i+15] < 8))
s.append(d[4+5*0] == ord('_')-0x30)s.append(d[4+5*1] == ord('_')-0x30)s.append(d[4+5*2] == ord('_')-0x30)
r11 = sum(d[0:4])r13 = sum(d[5:9])esi = sum(d[10:14])r8 = sum(d[15:])
s.append((r11+r13+esi)/3 == r8)s.append(esi/3 == r11)s.append(r11 != r13)
l = []for i in xrange(4):    l.append(d[i] != d[i+10])
s.append(And(l))
l = []for i in xrange(4):    l.append(d[i+5] != d[i+15])
s.append(And(l))
for A in get_models(s, 10):    ans = []    for i in d:        ans.append(chr(A[i].as_long()+0x30))
    x = "".join(ans)    print x```
Here's the output
```1612_8456_8769_65372262_8738_9999_64772262_8738_9999_65762262_2728_9999_45762262_2728_9999_44772262_2728_9999_66372262_2728_9999_66552262_5728_9999_66472262_3388_9999_66472222_7375_5388_5643```
All of them are valid !
There was a hint that -`The correct md5 starts with one of the two options: 0c79 or 98fc`and that took 20 points !! How annoying
So, now the modified script is 
```...for A in get_models(s, 10000000):    ans = []    for i in d:        ans.append(chr(A[i].as_long()+0x30))    x = "".join(ans)    m = md5(x).hexdigest()    if m.startswith('0c79') or m.startswith('98fc'):        print "[*] Serial: %s" % x        print "[*] MD5: %s" % m```
The output```[*] Serial: 8111_2562_9997_6653[*] MD5: 98fcc746a6ab0b2d776c331875f245b9[*] Serial: 1118_3538_9897_5673[*] MD5: 0c79badeb7544ce59bbb958a812e11e8[*] Serial: 2144_2362_9789_3457[*] MD5: 0c79842c0d7ecd5cab431da828c19134[*] Serial: 1241_6888_9790_5646[*] MD5: 0c79a44c4104531c569399f4811ac4a5...```