(benchmark autogen
  :logic QF_IDL
  :extrafuns ((a Int)
              (b Int)
              (c Int)
              (x Int))
  :formula
(and
  (= x a)
  (= (+ b 1) c)
  (= x c)
  (= b (+ a 1))
  )
  :status unknown
)
