(benchmark fuzzsmt
:logic QF_AUFLIA
:extrapreds ((p1 Array))
:extrafuns ((f1 Array Array Array Array))
:extrafuns ((v0 Int))
:extrafuns ((v4 Array))
:extrafuns ((v3 Array))
:extrafuns ((v1 Int))
:extrapreds ((p0 Int))
:extrafuns ((f0 Int Int Int Int))
:status sat
:formula
(let (?n1 0)
(flet ($n2 (> ?n1 v0))
(let (?n3 (store v4 v1 ?n1))
(flet ($n4 (p0 v0))
(let (?n5 (store v4 ?n1 v0))
(let (?n6 (ite $n4 ?n5 v4))
(let (?n7 (ite $n2 ?n3 ?n6))
(flet ($n8 (p0 ?n1))
(let (?n9 1)
(let (?n10 (ite $n8 ?n9 ?n1))
(flet ($n11 (= ?n1 ?n10))
(flet ($n12 (p0 ?n9))
(let (?n13 (ite $n12 ?n9 ?n1))
(let (?n14 3)
(let (?n15 (* v1 ?n14))
(flet ($n16 (< ?n13 ?n15))
(flet ($n17 (p1 ?n5))
(let (?n18 (ite $n17 ?n3 ?n5))
(let (?n19 (ite $n16 v3 ?n18))
(let (?n20 (ite $n11 ?n19 v3))
(let (?n21 (f1 ?n7 v4 ?n20))
(flet ($n22 (p1 ?n21))
(let (?n23 (f0 ?n1 ?n1 ?n1))
(flet ($n24 (p0 ?n23))
(let (?n25 (ite $n24 ?n9 ?n1))
(flet ($n26 (<= ?n15 ?n25))
(let (?n27 (ite $n26 v4 v3))
(let (?n28 (ite $n16 v3 ?n5))
(let (?n29 (f1 v4 ?n27 ?n28))
(flet ($n30 (p1 ?n29))
(flet ($n31 (or $n22 $n30))
$n31
))))))))))))))))))))))))))))))))