You can solve this using Z3 if you encode the integers as reals, which will force Z3 to use the nonlinear real arithmetic solver. See this for more details on the nonlinear integer vs. real arithmetic solvers: How does Z3 handle non-linear integer arithmetic?
Here's your example encoded as reals with the solution (z3py link: http://rise4fun.com/Z3Py/1lxH ):
a,b,c,d,e,f = Reals('a b c d e f')
solve(
a>0, a<200,
b>0, b<200,
c>0, c<200,
d>0, d<200,
e>0, e<200,
f>0, f<200,
(e+f)**2 + d**2 == 119**2,
(e+f)**2 + c**2 == 70**2,
e**2 + 30**2 == a**2,
f**2 + 30**2 == b**2,
a*d == 119*30,
b*c == 70*30,
a*f - 119*e + a*e == 0,
b*e - 70*f + b*f == 0,
d*e == c*f) # yields [a = 34, b = 50, c = 42, d = 105, e = 16, f = 40]
While the result is integer as you noted, and as what Z3 finds, Z3 apparently needs to use the real arithmetic solver to handle it.
Alternatively, you can leave the variables declared as integers and do the following from the suggestion at the referenced post:
t = Then('purify-arith','nlsat')
s = t.solver()
solve_using(s, P)
where P
is the conjunction of the constraints (z3py link: http://rise4fun.com/Z3Py/7nqN ).