blob: 90592392d503f4d499ecd5e4ca683b81feeaf2b5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
|
(benchmark fifo32bc06k08.smt
:logic QF_AUFBV
:extrafuns ((a1179 Array[6:32]))
:extrafuns ((reset_3 BitVec[1]))
:extrafuns ((full_fq_3 BitVec[1]))
:extrafuns ((a741 Array[6:32]))
:extrafuns ((a960 Array[6:32]))
:status unsat
:formula
(let (?n1 bv0[1])
(flet ($n2 (= a1179 a960))
(let (?n3 bv1[1])
(let (?n4 (ite $n2 ?n3 ?n1))
(flet ($n5 (= ?n3 full_fq_3))
(let (?n6 bv0[6])
(let (?n7 bv0[32])
(let (?n8 (store a741 ?n6 ?n7))
(let (?n9 (ite $n5 a741 ?n8))
(flet ($n10 (= a960 ?n9))
(let (?n11 (ite $n10 ?n3 ?n1))
(flet ($n12 (= ?n1 full_fq_3))
(let (?n13 (ite $n12 ?n3 ?n1))
(let (?n14 (bvnot ?n13))
(let (?n15 (bvand ?n14 reset_3))
(let (?n16 (bvnot ?n15))
(let (?n17 (bvand reset_3 ?n16))
(let (?n18 (bvand ?n11 ?n17))
(let (?n19 (bvand ?n4 ?n18))
(let (?n20 bv1[32])
(let (?n21 (select a1179 ?n6))
(flet ($n22 (= ?n20 ?n21))
(let (?n23 (ite $n22 ?n3 ?n1))
(let (?n24 (bvand ?n19 ?n23))
(flet ($n25 (= ?n1 ?n24))
(flet ($n26 (not $n25))
$n26
)))))))))))))))))))))))))))
|
