blob: 22a4beb2e366ce4851dfe7e335900d9fa24af9c5 (
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
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
|
(benchmark fifo32in06k08.smt
:logic QF_AUFBV
:extrafuns ((full_fq_2 BitVec[1]))
:extrafuns ((full_fs_2 BitVec[1]))
:extrafuns ((reset_2 BitVec[1]))
:extrafuns ((full_fq_1 BitVec[1]))
:extrafuns ((reset_1 BitVec[1]))
:extrafuns ((a504 Array[6:32]))
:extrafuns ((enqeue_2 BitVec[1]))
:extrafuns ((deqeue_2 BitVec[1]))
:extrafuns ((a723 Array[6:32]))
:extrafuns ((a942 Array[6:32]))
:extrafuns ((a1161 Array[6:32]))
:extrafuns ((a1380 Array[6:32]))
:status unknown
:formula
(let (?n1 bv0[1])
(let (?n2 bv0[32])
(let (?n3 bv0[6])
(let (?n4 (select a1380 ?n3))
(flet ($n5 (= ?n2 ?n4))
(let (?n6 bv1[1])
(let (?n7 (ite $n5 ?n6 ?n1))
(flet ($n8 (= a1161 a1380))
(let (?n9 (ite $n8 ?n6 ?n1))
(flet ($n10 (= a942 a1161))
(let (?n11 (ite $n10 ?n6 ?n1))
(flet ($n12 (= a723 a942))
(let (?n13 (ite $n12 ?n6 ?n1))
(flet ($n14 (= ?n6 deqeue_2))
(flet ($n15 (= ?n6 enqeue_2))
(flet ($n16 (= ?n6 full_fs_2))
(let (?n17 (store a504 ?n3 ?n2))
(let (?n18 (ite $n16 a504 ?n17))
(let (?n19 (ite $n15 ?n18 a504))
(let (?n20 (ite $n14 ?n19 a504))
(flet ($n21 (= a723 ?n20))
(let (?n22 (ite $n21 ?n6 ?n1))
(flet ($n23 (= ?n6 reset_1))
(let (?n24 (ite $n23 full_fq_1 ?n1))
(flet ($n25 (= full_fq_2 ?n24))
(let (?n26 (ite $n25 ?n6 ?n1))
(let (?n27 (bvand reset_1 ?n26))
(let (?n28 (bvand reset_2 ?n27))
(flet ($n29 (= full_fs_2 full_fq_2))
(let (?n30 (ite $n29 ?n6 ?n1))
(let (?n31 (bvnot ?n30))
(let (?n32 (bvand reset_2 ?n31))
(let (?n33 (bvnot ?n32))
(let (?n34 (bvand ?n28 ?n33))
(let (?n35 (bvand ?n22 ?n34))
(let (?n36 (bvand ?n13 ?n35))
(let (?n37 (bvand ?n11 ?n36))
(let (?n38 (bvand ?n9 ?n37))
(let (?n39 (bvand ?n7 ?n38))
(flet ($n40 (= ?n1 ?n39))
(flet ($n41 (not $n40))
$n41
))))))))))))))))))))))))))))))))))))))))))
|
