1(benchmark fuzzsmt
2:logic QF_AUFLIA
3:extrapreds ((p1 Array Array))
4:extrafuns ((f1 Array Array Array Array))
5:extrafuns ((v3 Array))
6:status sat
7:formula
8(let (?n1 (f1 v3 v3 v3))
9(let (?n2 0)
10(let (?n3 (store v3 ?n2 ?n2))
11(let (?n4 (f1 v3 v3 ?n3))
12(let (?n5 (f1 v3 ?n4 v3))
13(flet ($n6 (p1 ?n1 ?n5))
14$n6
15)))))))
16