blob: 82b54a231b7f47d0f9e26f5e594f0cf152e91a0b (
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
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
|
; COMMAND-LINE: --cbqi-bv --cbqi-bv-ineq=eq-boundary
; EXPECT: unsat
(set-logic BV)
(set-info :status unsat)
(declare-fun W_S1_V6 () Bool)
(declare-fun W_S1_V4 () Bool)
(declare-fun W_S1_V2 () Bool)
(declare-fun W_S1_V3 () Bool)
(declare-fun W_S1_V1 () Bool)
(declare-fun R_E2_V1 () Bool)
(declare-fun R_E2_V3 () Bool)
(declare-fun R_E1_V3 () Bool)
(declare-fun R_E1_V1 () Bool)
(declare-fun R_E1_V6 () Bool)
(declare-fun R_E1_V4 () Bool)
(declare-fun R_E1_V5 () Bool)
(declare-fun R_E1_V2 () Bool)
(declare-fun DISJ_W_S1_R_E1 () Bool)
(declare-fun R_S1_V6 () Bool)
(declare-fun R_S1_V4 () Bool)
(declare-fun R_S1_V5 () Bool)
(declare-fun R_S1_V2 () Bool)
(declare-fun R_S1_V3 () Bool)
(declare-fun R_S1_V1 () Bool)
(declare-fun DISJ_W_S1_R_S1 () Bool)
(declare-fun R_E2_V6 () Bool)
(declare-fun R_E2_V4 () Bool)
(declare-fun R_E2_V5 () Bool)
(declare-fun R_E2_V2 () Bool)
(declare-fun DISJ_W_S1_R_E2 () Bool)
(declare-fun W_S1_V5 () Bool)
(assert
(let
(($x59848
(forall
((V1_0 (_ BitVec 32)) (V3_0 (_ BitVec 32))
(V2_0 (_ BitVec 32)) (V5_0 (_ BitVec 32))
(V4_0 (_ BitVec 32)) (V6_0 (_ BitVec 32))
(MW_S1_V1 Bool) (MW_S1_V3 Bool)
(MW_S1_V2 Bool) (MW_S1_V5 Bool)
(MW_S1_V4 Bool) (MW_S1_V6 Bool)
(S1_V1_!5000 (_ BitVec 32)) (S1_V3_!5001 (_ BitVec 32))
(S1_V2_!5002 (_ BitVec 32)) (E1_!4994 (_ BitVec 32))
(E1_!4997 (_ BitVec 32)) (E1_!4999 (_ BitVec 32))
(S1_V5_!5003 (_ BitVec 32)) (E2_!4995 (_ BitVec 32))
(E2_!4996 (_ BitVec 32)) (E2_!4998 (_ BitVec 32))
(S1_V4_!5004 (_ BitVec 32)) (S1_V6_!5005 (_ BitVec 32)))
(let ((?x62719 (ite MW_S1_V6 S1_V6_!5005 V6_0)))
(let (($x60064 (= V6_0 ?x62719)))
(let ((?x61425 (ite MW_S1_V4 S1_V4_!5004 V4_0)))
(let (($x59873 (= V4_0 ?x61425)))
(let ((?x59861 (ite MW_S1_V5 S1_V5_!5003 V5_0)))
(let (($x62312 (= V5_0 ?x59861)))
(let ((?x60966 (ite MW_S1_V2 S1_V2_!5002 V2_0)))
(let (($x61331 (= V2_0 ?x60966)))
(let ((?x62280 (ite MW_S1_V3 S1_V3_!5001 E2_!4998)))
(let ((?x60903 (bvadd (_ bv1 32) ?x62280)))
(let (($x61268 (= E2_!4996 ?x60903)))
(let ((?x60065 (ite MW_S1_V1 S1_V1_!5000 E1_!4999)))
(let (($x60169 (= E1_!4994 ?x60065)))
(let (($x62661 (and $x60169 $x61268 $x61331 $x62312 $x59873 $x60064)))
(let ((?x62301 (bvadd (bvneg (_ bv1 32)) ?x61425)))
(let (($x61124 (bvsge ?x62280 ?x62301)))
(let ((?x61096 (bvadd (bvneg (_ bv1 32)) ?x60966)))
(let (($x60960 (bvsge ?x60065 ?x61096)))
(let (($x62453 (bvsle V2_0 E1_!4999)))
(let (($x61140 (not $x62453)))
(let (($x60239 (bvsle V4_0 E2_!4998)))
(let (($x61367 (not $x60239)))
(let (($x59857 (bvsle V2_0 E1_!4997)))
(let (($x62570 (not $x59857)))
(let ((?x62418 (bvadd (bvneg (_ bv1 32)) V2_0)))
(let (($x60189 (bvsge E1_!4994 ?x62418)))
(let (($x62421 (bvsge E2_!4996 V4_0)))
(let (($x60898 (bvsle V2_0 E1_!4994)))
(let (($x59938 (not $x60898)))
(let (($x62400 (bvsle V4_0 E2_!4995)))
(let (($x60971 (not $x62400)))
(let
(($x62394
(and $x60971 $x59938 $x62421 $x60189 $x62570 $x61367 $x61140 $x60960
$x61124)))
(let (($x62485 (not $x62394)))
(let (($x60905 (not MW_S1_V6)))
(let (($x61285 (or $x60905 W_S1_V6)))
(let (($x61317 (not MW_S1_V4)))
(let (($x60137 (or $x61317 W_S1_V4)))
(let (($x62306 (not MW_S1_V2)))
(let (($x62708 (or $x62306 W_S1_V2)))
(let (($x62310 (not MW_S1_V3)))
(let (($x60291 (or $x62310 W_S1_V3)))
(let (($x62641 (not MW_S1_V1)))
(let (($x61174 (or $x62641 W_S1_V1)))
(let (($x62627 (= E2_!4998 E2_!4995)))
(let (($x60904 (= E1_!4997 E1_!4994)))
(let (($x128 (not R_E2_V1)))
(let (($x60161 (or $x128 $x60904)))
(let (($x62415 (not $x60161)))
(let (($x62645 (or $x62415 $x62627)))
(let (($x60924 (= E2_!4996 E2_!4998)))
(let (($x62711 (= E2_!4995 V3_0)))
(let (($x130 (not R_E2_V3)))
(let (($x62623 (or $x130 $x62711)))
(let (($x60954 (= E1_!4994 E1_!4997)))
(let (($x59868 (or $x128 $x60954)))
(let (($x62319 (and $x59868 $x62623)))
(let (($x62554 (not $x62319)))
(let (($x60985 (or $x62554 $x60924)))
(let (($x62256 (= E2_!4996 E2_!4995)))
(let (($x62540 (not $x62623)))
(let (($x60968 (or $x62540 $x62256)))
(let (($x62486 (= E1_!4999 E1_!4997)))
(let (($x60109 (= E2_!4998 V3_0)))
(let (($x115 (not R_E1_V3)))
(let (($x60129 (or $x115 $x60109)))
(let (($x60976 (= E1_!4997 V1_0)))
(let (($x113 (not R_E1_V1)))
(let (($x62568 (or $x113 $x60976)))
(let (($x60942 (and $x62568 $x60129)))
(let (($x60209 (not $x60942)))
(let (($x62263 (or $x60209 $x62486)))
(let (($x60965 (= E1_!4999 E1_!4994)))
(let (($x62348 (or $x60209 $x60965)))
(let
(($x60285
(and $x60954 $x62348 $x62263 $x60968 $x60985 $x62645 $x61174 $x60291
$x62708 $x60137 $x61285)))
(let (($x62430 (not $x60285))) (or $x62430 $x62485 $x62661)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(let (($x56 (and W_S1_V6 R_E1_V6)))
(let (($x54 (and W_S1_V4 R_E1_V4)))
(let (($x50 (and W_S1_V2 R_E1_V2)))
(let (($x48 (and W_S1_V3 R_E1_V3)))
(let (($x46 (and W_S1_V1 R_E1_V1)))
(let (($x69 (or $x46 $x48 $x50 R_E1_V5 $x54 $x56)))
(let (($x70 (not $x69)))
(let (($x71 (= DISJ_W_S1_R_E1 $x70)))
(let (($x40 (and W_S1_V6 R_S1_V6)))
(let (($x38 (and W_S1_V4 R_S1_V4)))
(let (($x34 (and W_S1_V2 R_S1_V2)))
(let (($x32 (and W_S1_V3 R_S1_V3)))
(let (($x30 (and W_S1_V1 R_S1_V1)))
(let (($x66 (or $x30 $x32 $x34 R_S1_V5 $x38 $x40)))
(let (($x67 (not $x66)))
(let (($x68 (= DISJ_W_S1_R_S1 $x67)))
(let (($x24 (and W_S1_V6 R_E2_V6)))
(let (($x21 (and W_S1_V4 R_E2_V4)))
(let (($x16 (and W_S1_V2 R_E2_V2)))
(let (($x13 (and W_S1_V3 R_E2_V3)))
(let (($x10 (and W_S1_V1 R_E2_V1)))
(let (($x63 (or $x10 $x13 $x16 R_E2_V5 $x21 $x24)))
(let (($x64 (not $x63)))
(let (($x65 (= DISJ_W_S1_R_E2 $x64)))
(let (($x130 (not R_E2_V3)))
(let (($x115 (not R_E1_V3)))
(let (($x113 (not R_E1_V1)))
(let (($x60916 (and $x113 $x115)))
(let (($x62291 (or $x60916 $x130)))
(and $x62291 W_S1_V5 $x65 $x68 $x71 $x59848))))))))))))))))))))))))))))))))
(assert R_E2_V3)
(check-sat)
(exit)
|
