send more money puzzle in z3

gistfile1.txt

from z3 import *

# find the (distinct) integers in 0..9 that make this equation work:                                              
#                                                                                                                 
#   SEND                                                                                                          
# + MORE                                                                                                          
# ------                                                                                                          
#  MONEY                                                                                                          

S = Int('S')
E = Int('E')
N = Int('N')
D = Int('D')
M = Int('M')
O = Int('O')
R = Int('R')
Y = Int('Y')

s = Solver()

s.add (S >= 0, S < 10,
       E >= 0, E < 10,
       N >= 0, N < 10,
       D >= 0, D < 10,
       M >= 0, M < 10,
       O >= 0, O < 10,
       R >= 0, R < 10,
       Y >= 0, Y < 10)

s.add(Distinct(S, E, N, D, M, O, R, Y))

s.add ((D + 10 * N + 100 * E + 1000 * S + E + 10 * R + 100 * O + 1000 * M) ==
       (Y + 10 * E + 100 * N + 1000 * O + 10000 * M))

print s.check()
m = s.model()
for d in m.decls():
    print "%s = %s" % (d.name(), m[d])