I am new to learning Z3 and trying to solve the 'SEND + MORE = MONEY' puzzle with it. I have solved a couple of bugs by copying others' code, but I don't really understand why it works.

Q1:Why is there a difference between the two constraints?

Code:

from z3 import *

digits = Ints('s e n d m o r y')
s,e,n,d,m,o,r,y = digits
sendmore = 1000*s+100*e+10*n+d+1000*m+100*o+10*r+e
money = 10000*m+1000*o+100*n+10*e+y

solver = Solver()

solver.add([s>0, m>0])
for d in digits:
    solver.add([d>=0, d<=9])
solver.add(Distinct(digits))

solver.add( sendmore == money )
print(solver.check())   #sat

solver.add( 1000*s+100*e+10*n+d+1000*m+100*o+10*r+e == 10000*m+1000*o+100*n+10*e+y )
print(solver.check())   #unsat

Initially, I used the second method and found it unsat. Therefore, I googled a solution which is the first method, and it returns sat. So what makes the difference?

Q2:How does changing the position of definitions matters?

Code:

from z3 import *

digits = Ints('s e n d m o r y')
s,e,n,d,m,o,r,y = digits

solver = Solver()

solver.add([s>0, m>0])
for d in digits:
    solver.add([d>=0, d<=9])
solver.add(Distinct(digits))

sendmore = 1000*s+100*e+10*n+d+1000*m+100*o+10*r+e
money = 10000*m+1000*o+100*n+10*e+y
solver.add( sendmore == money )
print(solver.check())   #unsat

So I was messing around with the code and accidentally found that moving the definition of sendmore and money also affects the result. Why?

Edit: I just replaced the for loop with solver.add([And(d>=0, d<=9) for d in digits]), and everything just went perfectly sat, still don't know why.

The flaw is in the for loop to delimit the range of digits:

solver = Solver()
solver.add([s>0, m>0])
for dig in digits:
    solver.add([dig>=0, dig<=9])
solver.add(Distinct(digits))
solver.add( 1000*s+100*e+10*n+d+1000*m+100*o+10*r+e == 10000*m+1000*o+100*n+10*e+y )
res = solver.check()
print(res)  
if res == sat:
    M = solver.model()
    print(M[s],M[e],M[n],M[d],"+",M[m],M[o],M[r],M[e])
    print(M[m],M[o],M[n],M[e],M[y])

The loop variable d clashed with the decision variable d.
Thus, it has to be renamed.