(benchmark gasburner_prop3_1.smt
  :source {
SAL benchmark suite.  Created at SRI by Bruno Dutertre, John Rushby, Maria
Sorea, and Leonardo de Moura.  Contact demoura@csl.sri.com for more
information.

This benchmark was automatically translated into SMT-LIB format from
CVC format using CVC Lite
}
  :status unknown
  :logic QF_LRA
  :extrasorts (ANY)
  :extrapreds ((x_0))
  :extrafuns ((x_1 Real))
  :extrafuns ((x_2 Real))
  :extrafuns ((x_3 Real))
  :extrafuns ((x_4 Real))
  :extrapreds ((x_5))
  :extrafuns ((x_6 Real))
  :extrafuns ((x_7 Real))
  :extrafuns ((x_8 Real))
  :extrapreds ((x_9))
  :formula
(flet ($cvcl_0 (not x_0)) (flet ($cvcl_2 (= x_1 0)) (flet ($cvcl_1 (not x_5)) (flet ($cvcl_3 (= x_4 0)) (flet ($cvcl_4 (= x_3 0)) (and (and (and (and (and (and (<= x_7 1) (>= x_7 0)) $cvcl_0) (not (< x_6 0))) (= x_7 (ite x_5 0 1))) (or (or (and (and (and (and (and (and (= x_8 0) $cvcl_1) $cvcl_0) x_9) $cvcl_2) $cvcl_3) $cvcl_4)  (and (and (and (and (and (and (and (= x_8 1) $cvcl_1) x_0) (not (> 30 0))) (not x_9)) $cvcl_2) $cvcl_3) $cvcl_4) )  (and (and (and (and (and (and (and (= x_8 2) x_5) (not (< x_2 0))) (or x_0  (<= (+ 0 x_2) 1) )) (= x_1 (+ 0 x_2))) (= x_4 (+ 0 x_2))) (= x_3 (ite $cvcl_0 (+ 0 x_2) 0))) (iff x_9 x_0)) )) (or (and (not (< x_4 60)) (not (<= (* x_3 20) x_4)))  (and (not (> 60 0)) (not (<= (* 0 20) 0))) )))))))
)