(benchmark autogen
; Used to be a bug from fischer3-mutex-5-conflict-109.smt.save 
; This is satisfiable, but was found unsatisfiable
; Model: b=0; c=1; a=f=2; d=3; e=4
  :logic QF_RDL
  :extrafuns ((a Real)
              (b Real)
              (c Real)
              (d Real)
              (e Real)
              (f Real)
)
  :formula
(and
  (not (<= 0 (- d e)))
  (not (<= 0 (- f d)))
  (<= 0 (- a b))
  (not (<= 0 (- b c)))
  (<= 0 (- a c))
  (= 0 (- f a))
  )
  :status sat
)
