title: How do I evaluate this equation in z3 for python
body: <p>I'm trying to evaluate a simple absolute value inequality like this using z3.</p>
  
  <pre><code>
  x = Int("x")
  y = Int("y")
  
  
  def abs(x):
      return If(x &gt;= 0,x,-x)
  
  solve(abs( x / 1000 - y / 1000  ) &lt; .01, y==1000)
  </code></pre>
  
  <p>The output is no solution every time.  I know this is mathematically possible, I just can't figure out how z3 does stuff like this. </p>