Python z3 session

# pip install z3-solver

from z3 import *
s = Solver()
w = Int('w')
m = Int('m')

s.add(0 <= m, m <= 12)
s.add(0 <= w, w <= 12 - m)
s.add(m / Q(2,1) + w / Q(4,1) + 2 * (12 - m - w) == 12)   # Q(a,b) is the rational a/b

while True:
    if s.check() != sat:
        break
    mod = s.model()
    print(mod)
    s.push()
    # Add a constraint meaning "find a solution that doesn't include this one"
    s.add(w != mod[w], m != mod[m])

# output:
[w = 6, m = 1]
[w = 0, m = 8]