Support Real Division

[yangky11]

Hi,

smtlib::theories::reals::Real currently only supports floor division (div) but not real division (/). I'm wondering if there is a way to use real division. Thank you!

Simple examples to demonstrate the difference:

(declare-const a Real)
(assert (= a (div 1.0 2.0)))
(check-sat)
(get-model)

sat
(
  (define-fun a () Real
    0.0)
)

(declare-const a Real)
(assert (= a (/ 1.0 2.0)))
(check-sat)
(get-model)

sat
(
  (define-fun a () Real
    (/ 1.0 2.0))
)