1; COMMAND-LINE: --decision=justification
2; EXPECT: unsat
3
4(benchmark pp_regfile.smt
5:logic QF_AUFLIA
6:extrafuns ((REGFILE_INIT Array))
7:extrafuns ((BDEST_S2E_INIT Int))
8:extrafuns ((IMEM_INIT Array))
9:extrafuns ((OPCODE_OF Int Int))
10:status unknown
11:formula
12(let (?n1 0)
13(let (?n2 (select REGFILE_INIT ?n1))
14(let (?n3 (select IMEM_INIT ?n1))
15(let (?n4 (OPCODE_OF ?n3))
16(let (?n5 1)
17(flet ($n6 (= ?n4 ?n5))
18(flet ($n7 (= ?n1 ?n3))
19(flet ($n8 false)
20(flet ($n9 true)
21(flet ($n10 (if_then_else $n7 $n8 $n9))
22(flet ($n11 (= BDEST_S2E_INIT ?n1))
23(flet ($n12 (if_then_else $n11 $n8 $n9))
24(let (?n13 (store REGFILE_INIT BDEST_S2E_INIT ?n1))
25(let (?n14 (ite $n12 ?n13 REGFILE_INIT))
26(let (?n15 (store ?n14 ?n3 ?n1))
27(let (?n16 (ite $n10 ?n15 ?n14))
28(flet ($n17 (= ?n1 ?n4))
29(let (?n18 16)
30(flet ($n19 (= ?n18 ?n4))
31(let (?n20 (ite $n19 ?n16 ?n14))
32(let (?n21 (ite $n17 ?n14 ?n20))
33(let (?n22 (ite $n6 ?n16 ?n21))
34(let (?n23 (select ?n22 ?n1))
35(flet ($n24 (= ?n2 ?n23))
36(flet ($n25 (not $n24))
37$n25
38))))))))))))))))))))))))))
39