(set-option :incremental false)
(set-info :status sat)
(set-logic QF_BV)
(declare-fun UCL_p16 () Bool)
(declare-fun UCL_p34 () Bool)
(check-sat-assuming ( (let ((_let_0 (ite (= (_ bv0 4) (ite UCL_p16 (_ bv1 4) (_ bv0 4))) (_ bv1 2) (_ bv0 2)))) (let ((_let_1 (= (_ bv1 2) _let_0))) (let ((_let_2 (bvadd (ite (= (_ bv0 4) (ite (= (_ bv1 2) (ite UCL_p34 (_ bv0 2) (_ bv1 2))) (_ bv1 4) (_ bv0 4))) (_ bv1 5) (_ bv0 5)) (ite (= (_ bv0 5) (ite (or (= (_ bv0 2) _let_0) _let_1) (_ bv1 5) (_ bv0 5))) (_ bv1 5) (_ bv0 5))))) (let ((_let_3 (ite _let_1 (_ bv1 5) (_ bv0 5)))) (let ((_let_4 (ite (= (_ bv0 5) (ite (= (_ bv0 5) (ite (= (_ bv0 4) (ite UCL_p16 (_ bv1 4) (_ bv0 4))) (_ bv1 5) (_ bv0 5))) (ite (or (= (_ bv0 2) _let_0) _let_1) (_ bv1 5) (_ bv0 5)) (_ bv0 5))) (_ bv0 5) (bvsub (_ bv0 5) (_ bv1 5))))) (let ((_let_5 (ite (= (_ bv1 5) (ite (= (_ bv0 5) _let_3) (_ bv0 5) (ite (= (_ bv0 5) _let_4) (_ bv1 5) _let_4))) (concat (concat (concat (concat (_ bv1 4) (_ bv1 2)) (_ bv0 2)) (_ bv0 32)) (_ bv0 32)) (ite (= (_ bv1 5) (bvadd _let_3 _let_4)) (_ bv0 72) (concat (concat (concat (_ bv1 6) (_ bv1 2)) (_ bv0 32)) (_ bv0 32)))))) (= (ite (= (_ bv1 1) ((_ extract 0 0) (ite (= (_ bv0 2) (ite (= (_ bv0 2) ((_ extract 3 2) ((_ extract 67 64) (ite (= (_ bv1 5) (ite (= (_ bv0 5) (ite (= (_ bv0 5) (ite (or (= (_ bv0 2) _let_0) _let_1) (_ bv1 5) (_ bv0 5))) (_ bv1 5) (_ bv0 5))) (bvadd (_ bv1 5) _let_2) _let_2)) (concat (concat (concat (_ bv1 6) (_ bv1 2)) (_ bv0 32)) (_ bv0 32)) (_ bv0 72))))) (_ bv1 2) (_ bv0 2))) (_ bv0 3) (_ bv1 3)))) (_ bv1 2) (_ bv0 2)) (ite (= (_ bv0 2) ((_ extract 3 2) ((_ extract 67 64) _let_5))) (ite (= (_ bv0 4) ((_ extract 71 68) _let_5)) (_ bv0 2) (_ bv1 2)) (_ bv0 2))))))))) ))