;; Extracted from fischer3-mutex-12.smt, soundness error
(benchmark autogen
  :logic QF_RDL
  :extrafuns ((a Real)
              (b Real)
              (c Real)
              (d Real))
  :formula
(and
  (not (<= 0 (- a b)))
  (<= 0 (- c a))
  (= 0 (- c b))
  (<= (- c d) (~ 2))
)
  :status sat
)
