(set-option :incremental false)
(set-info :status sat)
(set-logic QF_UFLIA)
(declare-fun fmt_length () Int)
(declare-fun fmt1 () Int)
(declare-fun x_count (Int) Int)
(declare-fun select_format (Int) Int)
(declare-fun percent () Int)
(declare-fun s_count (Int) Int)
(check-sat-assuming ( (let ((_let_0 (select_format 3))) (let ((_let_1 (x_count 0))) (let ((_let_2 (select_format 2))) (let ((_let_3 (x_count 1))) (and (and (= 1 (x_count 5)) (and (= 1 (x_count 4)) (and (= (x_count 3) (x_count 2)) (and (= 0 _let_0) (and (and (= 1 _let_1) (and (ite (= 1 percent) true (= 0 (s_count 0))) (ite (and (= percent _let_2) (= 1 _let_0)) false true))) (ite (and (= 0 percent) (= 0 _let_2)) (= 0 _let_3) (= _let_1 _let_3))))))) (and (= 9 fmt_length) (and (= 0 (+ 1 (x_count (- fmt1 2)))) (and (> fmt1 1) (< fmt1 (- fmt_length 1)))))))))) ))