(benchmark qf_arith21
  :logic UNKNOWN
  :extrafuns ((x Int) (y Int) (a Int) (z Int))
  :formula
  (and (= x y) (= x 1) (= y 2) (= (- y x) 0)
       (= (- 2 1) x) (= (- 2 1) z) (= (- y x) a))
  :status unsat
)
