# PicoCTF 2k13 - Harder serial

# cat harder_serial.py
#!/usr/bin/env python
# Looks like the serial number verification for space ships is similar to that
# of your robot. Try to find a serial that verifies for this space ship

import sys
print ("Please enter a valid serial number from your RoboCorpIntergalactic purchase")
if len(sys.argv) < 2:
 print ("Usage: %s [serial number]"%sys.argv[0])
 exit()

print ("#>" + sys.argv[1] + "<#")

def check_serial(serial):
 if (not set(serial).issubset(set(map(str,range(10))))):
  print ("only numbers allowed")
  return False
 if len(serial) != 20:
  return False
 if int(serial[15]) + int(serial[4]) != 10:
  return False
 if int(serial[1]) * int(serial[18]) != 2:
  return False
 if int(serial[15]) / int(serial[9]) != 1:
  return False
 if int(serial[17]) - int(serial[0]) != 4:
  return False
 if int(serial[5]) - int(serial[17]) != -1:
  return False
 if int(serial[15]) - int(serial[1]) != 5:
  return False
 if int(serial[1]) * int(serial[10]) != 18:
  return False
 if int(serial[8]) + int(serial[13]) != 14:
  return False
 if int(serial[18]) * int(serial[8]) != 5:
  return False
 if int(serial[4]) * int(serial[11]) != 0:
  return False
 if int(serial[8]) + int(serial[9]) != 12:
  return False
 if int(serial[12]) - int(serial[19]) != 1:
  return False
 if int(serial[9]) % int(serial[17]) != 7:
  return False
 if int(serial[14]) * int(serial[16]) != 40:
  return False
 if int(serial[7]) - int(serial[4]) != 1:
  return False
 if int(serial[6]) + int(serial[0]) != 6:
  return False
 if int(serial[2]) - int(serial[16]) != 0:
  return False
 if int(serial[4]) - int(serial[6]) != 1:
  return False
 if int(serial[0]) % int(serial[5]) != 4:
  return False
 if int(serial[5]) * int(serial[11]) != 0:
  return False
 if int(serial[10]) % int(serial[15]) != 2:
  return False
 if int(serial[11]) / int(serial[3]) != 0:
  return False
 if int(serial[14]) - int(serial[13]) != -4:
  return False
 if int(serial[18]) + int(serial[19]) != 3:
  return False
 return True

if check_serial(sys.argv[1]):
 print ("Thank you! Your product has been verified!")
else:
 print ("I'm sorry that is incorrect. Please use a valid RoboCorpIntergalactic serial number")

# cat sol.py 
from z3 import *

serial = IntVector('serial', 20)

s = Solver()
 
s.add(0 <= serial[0]); s.add(0 <= serial[1])
s.add(0 <= serial[2]); s.add(1 <= serial[3])
s.add(0 <= serial[4]); s.add(0 <= serial[5])
s.add(0 <= serial[6]); s.add(0 <= serial[7])
s.add(0 <= serial[8]); s.add(1 <= serial[9])
s.add(0 <= serial[10]); s.add(0 <= serial[11])
s.add(0 <= serial[12]); s.add(0 <= serial[13])
s.add(0 <= serial[14]); s.add(0 <= serial[15])
s.add(0 <= serial[16]); s.add(0 <= serial[17])
s.add(0 <= serial[18]); s.add(0 <= serial[19])

s.add(serial[0] < 10); s.add(serial[1] < 10)
s.add(serial[2] < 10); s.add(serial[3] < 10)
s.add(serial[4] < 10); s.add(serial[5] < 10)
s.add(serial[6] < 10); s.add(serial[7] < 10)
s.add(serial[8] < 10); s.add(serial[9] < 10)
s.add(serial[10] < 10); s.add(serial[11] < 10)
s.add(serial[12] < 10); s.add(serial[13] < 10)
s.add(serial[14] < 10); s.add(serial[15] < 10)
s.add(serial[16] < 10); s.add(serial[17] < 10)
s.add(serial[18] < 10); s.add(serial[19] < 10)

s.add(serial[15] + serial[4] == 10);
s.add(serial[1] * serial[18] == 2)
s.add(serial[15] / serial[9] == 1);
s.add(serial[17] - serial[0] == 4)
s.add(serial[5] - serial[17] == -1);
s.add(serial[15] - serial[1] == 5)
s.add(serial[1] * serial[10] == 18);
s.add(serial[8] + serial[13] == 14)
s.add(serial[18] * serial[8] == 5);
s.add(serial[4] * serial[11] == 0)
s.add(serial[8] + serial[9] == 12);
s.add(serial[12] - serial[19] == 1)
s.add(serial[9] % serial[17] == 7);
s.add(serial[14] * serial[16] == 40)
s.add(serial[7] - serial[4] == 1);
s.add(serial[6] + serial[0] == 6)
s.add(serial[2] - serial[16] == 0);
s.add(serial[4] - serial[6] == 1)
s.add(serial[0] % serial[5] == 4);
s.add(serial[5] * serial[11] == 0)
s.add(serial[10] % serial[15] == 2);
s.add(serial[11] / serial[3] == 0)
s.add(serial[14] - serial[13] == -4);
s.add(serial[18] + serial[19] == 3)

if s.check() == sat:
 print s.model()

$ python sol.py
[serial__17 = 8,
 serial__19 = 2,
 serial__14 = 5,
 serial__9 = 7,
 serial__7 = 4,
 serial__18 = 1,
 serial__11 = 0,
 serial__3 = 1,
 serial__16 = 8,
 serial__1 = 2,
 serial__4 = 3,
 serial__6 = 2,
 serial__15 = 7,
 serial__8 = 5,
 serial__10 = 9,
 serial__13 = 9,
 serial__5 = 7,
 serial__2 = 8,
 serial__0 = 4,
 serial__12 = 3]