title: Z3 Prover returns wrong solution
body: <p>I'm trying to solve an equation with Z3 Thoerem Prover in Python.
  But the solution I get is wrong.</p>
  
  <pre><code>from z3 import *    
  solv = Solver()
  x = Int("x")
  y = Int("y")
  z = Int("z")
  s = Solver()
  s.add(x/(y+z)+y/(x+z)+z/(x+y)==10, x&gt;0, y&gt;0, z&gt;0)
  s.add()
  print(s.check())
  print(s.model())
  </code></pre>
  
  <p>I get this solution:</p>
  
  <pre><code>[z = 60, y = 5, x = 1]
  </code></pre>
  
  <p>But when you fill in those values to the given equation the result is: 10.09735182849937. But what I want to find is an exact solution.
  What am I doing wrong?</p>
  
  <p>Thanks for your help :)</p>