(set-option :incremental false)
(set-info :status sat)
(set-logic QF_AUFLIA)
(declare-fun p1 ((Array Int Int)) Bool)
(declare-fun f1 ((Array Int Int) (Array Int Int) (Array Int Int)) (Array Int Int))
(declare-fun v0 () Int)
(declare-fun v4 () (Array Int Int))
(declare-fun v3 () (Array Int Int))
(declare-fun v1 () Int)
(declare-fun p0 (Int) Bool)
(declare-fun f0 (Int Int Int) Int)
(check-sat-assuming ( (let ((_let_0 (store v4 v1 0))) (let ((_let_1 (store v4 0 v0))) (let ((_let_2 (* v1 3))) (let ((_let_3 (< (ite (p0 1) 1 0) _let_2))) (or (p1 (f1 (ite (> 0 v0) _let_0 (ite (p0 v0) _let_1 v4)) v4 (ite (= 0 (ite (p0 0) 1 0)) (ite _let_3 v3 (ite (p1 _let_1) _let_0 _let_1)) v3))) (p1 (f1 v4 (ite (<= _let_2 (ite (p0 (f0 0 0 0)) 1 0)) v4 v3) (ite _let_3 v3 _let_1)))))))) ))