blob: d7ae495afca7d63bbe9a0946f2774c36b20284c4 (
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
|
(benchmark B_
:source {
Source unknown
}
:status unknown
:category { unknown }
:logic QF_AUFBV
:extrafuns ((m Array[8:8]))
:extrafuns ((regionSize Array[8:8]))
:extrafuns ((m_0 Array[8:8]))
:extrafuns ((regionSize_0 Array[8:8]))
:extrafuns ((addr_of_j BitVec[8]))
:extrafuns ((m_1 Array[8:8]))
:extrafuns ((regionSize_1 Array[8:8]))
:extrafuns ((m_2 Array[8:8]))
:extrafuns ((regionSize_2 Array[8:8]))
:extrafuns ((addr_of_a BitVec[8]))
:extrafuns ((m_3 Array[8:8]))
:extrafuns ((regionSize_3 Array[8:8]))
:extrafuns ((m_4 Array[8:8]))
:extrafuns ((regionSize_4 Array[8:8]))
:extrafuns ((m_5 Array[8:8]))
:extrafuns ((regionSize_5 Array[8:8]))
:extrafuns ((m_6 Array[8:8]))
:extrafuns ((regionSize_6 Array[8:8]))
:extrafuns ((addr_of_i BitVec[8]))
:extrafuns ((m_7 Array[8:8]))
:extrafuns ((regionSize_7 Array[8:8]))
:extrafuns ((m_8 Array[8:8]))
:extrafuns ((regionSize_8 Array[8:8]))
:formula (let (?v_3 (bvadd addr_of_a (select (store regionSize addr_of_a (bvmul bv8[8] bv1[8])) addr_of_a))) (let (?v_0 (store m addr_of_j bv0[8])) (let (?v_1 (store ?v_0 addr_of_j (bvadd (select ?v_0 addr_of_j) bv2[8]))) (let (?v_2 (bvadd addr_of_a (bvmul (select (store ?v_1 addr_of_i (bvadd (select ?v_1 addr_of_j) bv2[8])) addr_of_i) bv1[8]))) (not (implies (if_then_else true (and (bvule addr_of_a ?v_3) (and (bvult addr_of_j addr_of_a) (bvult addr_of_i addr_of_j))) false) (and (bvule addr_of_a ?v_2) (bvult ?v_2 ?v_3))))))))
:extrafuns ((m_9 Array[8:8]))
:extrafuns ((regionSize_9 Array[8:8]))
:extrafuns ((m_10 Array[8:8]))
:extrafuns ((regionSize_10 Array[8:8]))
:extrafuns ((m_11 Array[8:8]))
:extrafuns ((regionSize_11 Array[8:8]))
:extrafuns ((addr_of_TEST_VAR_0 BitVec[8]))
:extrafuns ((m_12 Array[8:8]))
:extrafuns ((regionSize_12 Array[8:8]))
:extrafuns ((m_13 Array[8:8]))
:extrafuns ((regionSize_13 Array[8:8]))
:extrafuns ((m_14 Array[8:8]))
:extrafuns ((regionSize_14 Array[8:8]))
:extrafuns ((m_15 Array[8:8]))
:extrafuns ((regionSize_15 Array[8:8]))
:extrafuns ((m_16 Array[8:8]))
:extrafuns ((regionSize_16 Array[8:8]))
:extrafuns ((m_17 Array[8:8]))
:extrafuns ((regionSize_17 Array[8:8]))
:extrafuns ((m_18 Array[8:8]))
:extrafuns ((regionSize_18 Array[8:8]))
:formula (let (?v_9 (bvadd addr_of_a (select (store regionSize addr_of_a (bvmul bv8[8] bv1[8])) addr_of_a))) (flet ($v_4 (bvule addr_of_a ?v_9)) (flet ($v_5 (bvult addr_of_i addr_of_j)) (let (?v_0 (store m addr_of_j bv0[8])) (let (?v_1 (store ?v_0 addr_of_j (bvadd (select ?v_0 addr_of_j) bv2[8]))) (let (?v_2 (store ?v_1 addr_of_i (bvadd (select ?v_1 addr_of_j) bv2[8]))) (let (?v_3 (store ?v_2 (bvadd addr_of_a (bvmul (select ?v_2 addr_of_i) bv1[8])) bv0[8])) (let (?v_6 (store ?v_3 addr_of_TEST_VAR_0 (ite (bvult (select ?v_3 addr_of_j) bv8[8]) bv1[8] bv0[8]))) (let (?v_7 (store ?v_6 addr_of_j (bvadd (select ?v_6 addr_of_j) bv2[8]))) (let (?v_8 (bvadd addr_of_a (bvmul (select (store ?v_7 addr_of_i (bvadd (select ?v_7 addr_of_j) bv2[8])) addr_of_i) bv1[8]))) (not (implies (if_then_else (if_then_else (if_then_else true (and $v_4 (and (bvult addr_of_j addr_of_a) $v_5)) false) (not (= (select ?v_6 addr_of_TEST_VAR_0) bv0[8])) false) (and $v_4 (and (bvult addr_of_TEST_VAR_0 addr_of_a) (and (bvult addr_of_j addr_of_TEST_VAR_0) $v_5))) false) (and (bvule addr_of_a ?v_8) (bvult ?v_8 ?v_9))))))))))))))
)
|
