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?