title: Why operators '/' and 'div' in Z3 give different results?
body: <p>I was trying to represent a real number with two integer numbers as using them as the numerator and the denominator of the real number. I wrote the following program:</p>
  
  <pre><code>(declare-const a Int)
  (declare-const b Int)
  (declare-const f Real)
  
  (assert (= f (/ a b)))
  (assert (= f 0.5))
  (assert (&gt; b 2))
  (assert (&gt; b a))
  
  (check-sat)
  (get-model)
  </code></pre>
  
  <p>The program returned SAT result as follows:</p>
  
  <pre><code>sat
  (model 
    (define-fun f () Real
      (/ 1.0 2.0))
    (define-fun b () Int
      4)
    (define-fun a () Int
      2)
  )
  </code></pre>
  
  <p>However, if I write '(assert (= f (div a b)))' instead of '(assert (= f (/ a b)))', then the result is UNSAT. Why does not div return the same result? </p>
  
  <p>Moreover, and the main concern for me, I did not find a way to use operator '/' in z3 .Net API. I can see only function MkDiv, which actually for operator 'div'. Is there a way so that I can apply operator '/' in the case of z3 .Net API? Thank you in advance.</p>