为什么 Z3 中的运算符“/”和“div”给出不同的结果？

我试图用两个整数来表示一个实数，并将它们用作实数的分子和分母。我写了以下程序：

(declare-const a Int)
(declare-const b Int)
(declare-const f Real)

(assert (= f (/ a b)))
(assert (= f 0.5))
(assert (> b 2))
(assert (> b a))

(check-sat)
(get-model)

程序返回SAT结果如下：

sat
(model 
  (define-fun f () Real
    (/ 1.0 2.0))
  (define-fun b () Int
    4)
  (define-fun a () Int
    2)
)

但是，如果我写“(assert (= f (div a b)))”而不是“(assert (= f (/ a b)))”，那么结果是 UNSAT。为什么 div 不返回相同的结果？

此外，我最关心的是，我没有找到在 z3 .Net API 中使用运算符“/”的方法。我只能看到函数 MkDiv，它实际上用于运算符“div”。有没有办法让我可以在 z3 .Net API 的情况下应用运算符“/”？先感谢您。

严格来说，这些公式都不符合 SMT-LIB2，因为/是一个接受两个实数输入并产生一个实数输出的函数，而div是一个接受两个 Int 输入并生成一个 Int 的函数（请参阅SMT-LIB理论 http://smtlib.cs.uiowa.edu/theories.shtml）。 Z3更轻松，自动转换那些对象。如果我们启用该选项smtlib2_compliant=true那么在这两种情况下它确实会报告错误。

原因是div版本不能满足的地方是确实没有解决办法f是一个整数，根据(= f (/ a b))，但确实不存在满足的整数(= f 0.5)