Project Euler 142 and Google OR-tools

Should I post such issues? Are they relevant?

Project Euler 142: Find the smallest $x + y + z$ with integers $x \gt y \gt z \gt 0$ such that $x + y$, $x - y$, $x + z$, $x - z$, $y + z$, $y - z$ are all perfect squares. https://projecteuler.net/problem=142

Z3 code:

#!/usr/bin/python3

from z3 import *

x,y,z = Ints('x y z')
a1,a2,a3,a4,a5,a6 = Ints('a1 a2 a3 a4 a5 a6')
s=Solver()
s.add(x>y, y>z, z>0)
max_limit=1000000
s.add(x<max_limit)
s.add(y<max_limit)
s.add(z<max_limit)
max_limit_sqr=(max_limit*2)**2
s.add(a1<max_limit_sqr)
s.add(a2<max_limit_sqr)
s.add(a3<max_limit_sqr)
s.add(a4<max_limit_sqr)
s.add(a5<max_limit_sqr)
s.add(a6<max_limit_sqr)
s.add(x + y == a1**2)
s.add(x - y == a2**2)
s.add(x + z == a3**2)
s.add(x - z == a4**2)
s.add(y + z == a5**2)
s.add(y - z == a6**2)

print (s.check())
print (s.model())

... Never finishes. The same code for Google OR-tools works: https://yurichev.com/n/PE_142/PE_142_OR.py

Z3Prover / z3

Project Euler 142 and Google OR-tools #7275