1(benchmark fuzzsmt
2:logic QF_AUFLIA
3:extrafuns ((v4 Array))
4:extrafuns ((f0 Int Int))
5:extrapreds ((p0 Int Int Int))
6:status sat
7:formula
8(let (?n1 0)
9(flet ($n2 (p0 ?n1 ?n1 ?n1))
10(let (?n3 1)
11(let (?n4 (ite $n2 ?n3 ?n1))
12(flet ($n5 (< ?n1 ?n4))
13(flet ($n6 (p0 ?n3 ?n1 ?n1))
14(let (?n7 (ite $n6 ?n3 ?n1))
15(let (?n8 (ite $n5 ?n7 ?n3))
16(flet ($n9 (< ?n1 ?n8))
17(flet ($n10 true)
18(let (?n11 3)
19(let (?n12 (f0 ?n1))
20(let (?n13 (* ?n11 ?n12))
21(let (?n14 (select v4 ?n1))
22(flet ($n15 (> ?n13 ?n14))
23(flet ($n16 (xor $n10 $n15))
24(flet ($n17 false)
25(flet ($n18 (implies $n16 $n17))
26(flet ($n19 (and $n9 $n18))
27$n19
28))))))))))))))))))))
29