title: z3 Solver solution issues
body: <pre><code>p = Int('p')
  q = Int('q')
  
  s = Solver()
  s.add(1&lt;=p&lt;=9, 1&lt;=q&lt;=19, 5&lt;(3*p-4*q)&lt;10)
  s.check() 
  print s.model()
  </code></pre>
  
  <p>returns sat, and gives the solution</p>
  
  <pre><code>[p = 0, q = 0]
  </code></pre>
  
  <p>which does not satisfy the constraints. If I remove the final constraint, it returns 
  a sensible pair that satisfies the first two (trivial) constraints. What's going on?</p>
  
  <p>Permalink to try this online: <a href="http://rise4fun.com/Z3Py/fk4" rel="nofollow">http://rise4fun.com/Z3Py/fk4</a></p>
  
  <hr>
  
  <p>EDIT : I'm new to z3, so there's a chance I'm doing something horribly wrong, do let me know.</p>