title: Z3 should be able to verify this program?
body: <p>I am a beginner user of Z3. Recently, I have been using z3 to verify some problems. Here is one problem I tried: (x &lt; 0 &amp;&amp; y &lt; 0) implies x/y >= 0, below are the programs I wrote:</p>
  
  <pre><code>(declare-const x Int)
  (declare-const y Int)
  (define-fun assumption() Bool
    (and (&lt; x 0) (&lt; y 0))
  )
  
  (define-fun predicate() Bool
    (&lt;= 0 (div x y))
  )
  
  (assert (not (=&gt; assumption predicate)))
  
  (check-sat)
  </code></pre>
  
  <p>When I use 'z3 -smt2 filename' to verify this program, it works and return unsat. However, when I later modify the program to:</p>
  
  <pre><code>(declare-const x Int)
  (declare-const y Int)
  (define-fun assumption() Bool
    (and (&lt; x 0) (&lt; y 0))
  )
  
  (define-fun predicate() Bool
    (&lt;= 0 (div (* -1 x) (* -1 y)))
  )
  
  (assert (not (=&gt; assumption predicate)))
  
  (check-sat)
  </code></pre>
  
  <p>This cause z3 to timeout when I changed 'x/y' to (-1 * x)/(-1 * y) and somehow I need to add -1 there. I am confused why this happened and why multiplied by a constant makes this problem more complex. </p>
  
  <p>Can somebody help figure out why this happened?</p>
  
  <p>Thank you!</p>