blob: d662207ddfeedc3090ebf1c90b37521825853908 (
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
|
(benchmark no_init_multi_member7.smt
:logic QF_AUFBV
:status unsat
:extrafuns ((member_6_curr_2 BitVec[32]))
:extrafuns ((arr_next_15 Array[32:32]))
:extrafuns ((member_3_curr_4 BitVec[32]))
:extrafuns ((main_0_x_3 BitVec[32]))
:extrafuns ((member_3_curr_5 BitVec[32]))
:extrafuns ((arr_val_8 Array[32:32]))
:status unknown
:formula
(flet ($n1 true)
(let (?n2 bv0[32])
(let (?n3 bv1[32])
(let (?n4 (select arr_val_8 member_6_curr_2))
(flet ($n5 (= ?n3 ?n4))
(let (?n6 (ite $n5 ?n3 ?n2))
(flet ($n7 (= ?n2 ?n6))
(let (?n8 (select arr_next_15 member_3_curr_5))
(flet ($n9 (= ?n2 ?n8))
(let (?n10 (select arr_next_15 ?n3))
(flet ($n11 (= ?n10 member_3_curr_4))
(let (?n12 (select arr_next_15 ?n2))
(flet ($n13 (= ?n3 ?n12))
(flet ($n14 (= ?n2 main_0_x_3))
(flet ($n15 (= ?n3 member_3_curr_4))
(flet ($n16 (and $n14 $n15))
(let (?n17 (ite $n16 ?n2 member_3_curr_4))
(flet ($n18 (= member_3_curr_5 ?n17))
(flet ($n19 (= member_6_curr_2 ?n12))
(let (?n20 (select arr_next_15 member_6_curr_2))
(flet ($n21 (= ?n2 ?n20))
(flet ($n22 (and $n7 $n9 $n11 $n13 $n18 $n19 $n1 $n21))
$n22
)))))))))))))))))))))))
|
