https://twitter.com/aty_carbuncle/status/1224323674372657156

anaume.py

from z3 import *

x, y, a = Ints(['x', 'y', 'a'])

solver = Solver()
def r(x, n):
    solver.add(x >= n)
    solver.add(x < n * 10)
solver.add(y * 10 == x * a)
solver.add(((x % 10) * (a % 10)) % 10 == 0)
solver.add(((x % 10) * (a / 100)) % 10 == 6)
r(x, 10)
r(y, 1000)
r(a, 100)
r(x * (a / 100), 100)
r(x * (a / 10 % 10), 10)
r(x * (a % 10), 10)
r(y / 10 - x * (a / 100), 10)

r = solver.check()
if r == sat:
    m = solver.model()
    print(m[x], m[y], m[a])
else:
    print('unsat')