ar/tests/test1.smt

   1 (benchmark test1.smt
   2 :logic QF_UFLIA
   3 :extrafuns ((A Int) (B Int) (C Int) (D Int))
   4 :formula (and
   5 (> (* 2 A) (+ B C))
   6 (> (* 2 B) (+ C D))
   7 (> (* 2 C) (* 3 D))
   8 (> (* 3 D) (+ A C))
   9 ))