;; this benchmark breaks harvey type system:
;; (< Real Integer) is disallowed
(benchmark arith_dl_47
  :logic QF_RDL
  :extrafuns ((a Real)
              (b Real)
              (c Real)
  )
  :formula
  (and
    (= a b)
    (= b c)
    ;; the problem is: 
    (or (< (- a c) 0) (> (- a c) 0))
  )
  :status unsat
)
