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
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
|
(set-logic AUFLIA)
(set-info :source |
Tokeneer case study <http://www.adacore.com/home/products/gnatpro/tokeneer/>
|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun field.datat.length () Int)
(declare-fun field.datat.minmatchlength () Int)
(declare-fun field.datat.text () Int)
(declare-fun field.keyboard__datat.length () Int)
(declare-fun field.keyboard__datat.text () Int)
(declare-fun field.t.rolepresent () Int)
(declare-fun field.t.currentop () Int)
(declare-fun archivelog () Int)
(declare-fun character__base__first () Int)
(declare-fun character__base__last () Int)
(declare-fun character__first () Int)
(declare-fun character__last () Int)
(declare-fun character__size () Int)
(declare-fun datai__base__first () Int)
(declare-fun datai__base__last () Int)
(declare-fun datai__first () Int)
(declare-fun datai__last () Int)
(declare-fun datai__size () Int)
(declare-fun datalengtht__base__first () Int)
(declare-fun datalengtht__base__last () Int)
(declare-fun datalengtht__first () Int)
(declare-fun datalengtht__last () Int)
(declare-fun datalengtht__size () Int)
(declare-fun integer__base__first () Int)
(declare-fun integer__base__last () Int)
(declare-fun integer__first () Int)
(declare-fun integer__last () Int)
(declare-fun integer__size () Int)
(declare-fun isavailable () Int)
(declare-fun keyboard__datai__base__first () Int)
(declare-fun keyboard__datai__base__last () Int)
(declare-fun keyboard__datai__first () Int)
(declare-fun keyboard__datai__last () Int)
(declare-fun keyboard__datai__size () Int)
(declare-fun keyboard__datalengtht__base__first () Int)
(declare-fun keyboard__datalengtht__base__last () Int)
(declare-fun keyboard__datalengtht__first () Int)
(declare-fun keyboard__datalengtht__last () Int)
(declare-fun keyboard__datalengtht__size () Int)
(declare-fun null__string () Int)
(declare-fun nullop () Int)
(declare-fun opandnullt__base__first () Int)
(declare-fun opandnullt__base__last () Int)
(declare-fun opandnullt__first () Int)
(declare-fun opandnullt__last () Int)
(declare-fun opandnullt__size () Int)
(declare-fun opt__base__first () Int)
(declare-fun opt__base__last () Int)
(declare-fun opt__first () Int)
(declare-fun opt__last () Int)
(declare-fun opt__size () Int)
(declare-fun optokeyed () Int)
(declare-fun overridelock () Int)
(declare-fun positive__base__first () Int)
(declare-fun positive__base__last () Int)
(declare-fun positive__first () Int)
(declare-fun positive__last () Int)
(declare-fun positive__size () Int)
(declare-fun privtypes__adminprivileget__base__first () Int)
(declare-fun privtypes__adminprivileget__base__last () Int)
(declare-fun privtypes__adminprivileget__first () Int)
(declare-fun privtypes__adminprivileget__last () Int)
(declare-fun privtypes__adminprivileget__size () Int)
(declare-fun privtypes__auditmanager () Int)
(declare-fun privtypes__guard () Int)
(declare-fun privtypes__privileget__base__first () Int)
(declare-fun privtypes__privileget__base__last () Int)
(declare-fun privtypes__privileget__first () Int)
(declare-fun privtypes__privileget__last () Int)
(declare-fun privtypes__privileget__size () Int)
(declare-fun privtypes__securityofficer () Int)
(declare-fun privtypes__useronly () Int)
(declare-fun shutdownop () Int)
(declare-fun updateconfigdata () Int)
(declare-fun keyedop () Int)
(declare-fun keyedop__entry__loop__2 () Int)
(declare-fun init.keyedop__entry__loop__2 () Int)
(declare-fun init.keyedop () Int)
(declare-fun loop__1__op () Int)
(declare-fun init.loop__1__op () Int)
(declare-fun loop__2__i () Int)
(declare-fun init.loop__2__i () Int)
(declare-fun theadmin () Int)
(declare-fun init.theadmin () Int)
(declare-fun theop () Int)
(declare-fun init.theop () Int)
(declare-fun bit__and (Int Int) Int)
(declare-fun bit__not (Int Int) Int)
(declare-fun bit__or (Int Int) Int)
(declare-fun bit__xor (Int Int) Int)
(declare-fun character__pos (Int) Int)
(declare-fun character__val (Int) Int)
(declare-fun integer__pred (Int) Int)
(declare-fun integer__succ (Int) Int)
(declare-fun opandnullt__pos (Int) Int)
(declare-fun opandnullt__pred (Int) Int)
(declare-fun opandnullt__succ (Int) Int)
(declare-fun opandnullt__val (Int) Int)
(declare-fun privtypes__privileget__pos (Int) Int)
(declare-fun privtypes__privileget__pred (Int) Int)
(declare-fun privtypes__privileget__succ (Int) Int)
(declare-fun privtypes__privileget__val (Int) Int)
(declare-fun round__ (Int) Int)
(declare-fun i.div (Int Int) Int)
(declare-fun i.mod (Int Int) Int)
(declare-fun i.mult (Int Int) Int)
(declare-fun i.exp (Int Int) Int)
(declare-fun tm.true () Int)
(declare-fun tm.false () Int)
(declare-fun tm.not (Int) Int)
(declare-fun tm.and (Int Int) Int)
(declare-fun tm.or (Int Int) Int)
(declare-fun tm.iff (Int Int) Int)
(declare-fun tm.eq (Int Int) Int)
(declare-fun tm.ne (Int Int) Int)
(declare-fun tm.lt (Int Int) Int)
(declare-fun tm.le (Int Int) Int)
(declare-fun tuple.2 (Int Int) Int)
(declare-fun a.store (Int Int Int) Int)
(declare-fun a.select (Int Int) Int)
(declare-fun a.mk_const_array (Int) Int)
(declare-fun a.default_array () Int)
(declare-fun r.default_record () Int)
(declare-fun matched () Bool)
(declare-fun init.matched () Bool)
(declare-fun ispresent (Int) Bool)
(declare-fun opandnullt__LE (Int Int) Bool)
(declare-fun opandnullt__LT (Int Int) Bool)
(declare-fun privtypes__privileget__LE (Int Int) Bool)
(declare-fun privtypes__privileget__LT (Int Int) Bool)
(assert (forall ((?i Int)) (=> (and (<= 0 ?i) (< ?i 4)) (= (privtypes__privileget__pos ?i) ?i))))
(assert (forall ((?i Int)) (=> (and (<= 0 ?i) (< ?i 4)) (= (privtypes__privileget__val ?i) ?i))))
(assert (forall ((?i Int)) (=> (and (<= 0 ?i) (< ?i 3)) (= (privtypes__privileget__succ ?i) (+ ?i 1)))))
(assert (forall ((?i Int)) (=> (and (<= 1 ?i) (< ?i 4)) (= (privtypes__privileget__pred ?i) (- ?i 1)))))
(assert (= privtypes__useronly 0))
(assert (= privtypes__guard 1))
(assert (= privtypes__auditmanager 2))
(assert (= privtypes__securityofficer 3))
(assert (forall ((?i Int)) (=> (and (<= 0 ?i) (< ?i 5)) (= (opandnullt__pos ?i) ?i))))
(assert (forall ((?i Int)) (=> (and (<= 0 ?i) (< ?i 5)) (= (opandnullt__val ?i) ?i))))
(assert (forall ((?i Int)) (=> (and (<= 0 ?i) (< ?i 4)) (= (opandnullt__succ ?i) (+ ?i 1)))))
(assert (forall ((?i Int)) (=> (and (<= 1 ?i) (< ?i 5)) (= (opandnullt__pred ?i) (- ?i 1)))))
(assert (= nullop 0))
(assert (= archivelog 1))
(assert (= updateconfigdata 2))
(assert (= overridelock 3))
(assert (= shutdownop 4))
(assert (forall ((?I Int)) (=> (and (<= archivelog ?I) (<= ?I shutdownop)) (<= datalengtht__first (a.select (a.select optokeyed ?I) field.datat.length)))))
(assert (forall ((?I Int)) (=> (and (<= archivelog ?I) (<= ?I shutdownop)) (<= (a.select (a.select optokeyed ?I) field.datat.length) datalengtht__last))))
(assert (forall ((?I Int)) (=> (and (<= archivelog ?I) (<= ?I shutdownop)) (<= datai__first (a.select (a.select optokeyed ?I) field.datat.minmatchlength)))))
(assert (forall ((?I Int)) (=> (and (<= archivelog ?I) (<= ?I shutdownop)) (<= (a.select (a.select optokeyed ?I) field.datat.minmatchlength) datai__last))))
(assert (forall ((?I Int) (?J Int)) (=> (and (<= archivelog ?I) (<= ?I shutdownop) (<= 1 ?J) (<= ?J 18)) (<= character__first (a.select (a.select (a.select optokeyed ?I) field.datat.text) ?J)))))
(assert (forall ((?I Int) (?J Int)) (=> (and (<= archivelog ?I) (<= ?I shutdownop) (<= 1 ?J) (<= ?J 18)) (<= (a.select (a.select (a.select optokeyed ?I) field.datat.text) ?J) character__last))))
(assert (<= 0 integer__size))
(assert (= integer__first (- 2147483648)))
(assert (= integer__last 2147483647))
(assert (= integer__base__first (- 2147483648)))
(assert (= integer__base__last 2147483647))
(assert (<= 0 character__size))
(assert (= character__first 0))
(assert (= character__last 255))
(assert (= character__base__first 0))
(assert (= character__base__last 255))
(assert (<= 0 positive__size))
(assert (= positive__first 1))
(assert (= positive__last 2147483647))
(assert (= positive__base__first (- 2147483648)))
(assert (= positive__base__last 2147483647))
(assert (<= 0 privtypes__privileget__size))
(assert (= privtypes__privileget__first privtypes__useronly))
(assert (= privtypes__privileget__last privtypes__securityofficer))
(assert (= privtypes__privileget__base__first privtypes__useronly))
(assert (= privtypes__privileget__base__last privtypes__securityofficer))
(assert (<= 0 privtypes__adminprivileget__size))
(assert (= privtypes__adminprivileget__first privtypes__guard))
(assert (= privtypes__adminprivileget__last privtypes__securityofficer))
(assert (= privtypes__adminprivileget__base__first privtypes__useronly))
(assert (= privtypes__adminprivileget__base__last privtypes__securityofficer))
(assert (<= 0 keyboard__datalengtht__size))
(assert (= keyboard__datalengtht__first 0))
(assert (= keyboard__datalengtht__last 78))
(assert (= keyboard__datalengtht__base__first (- 2147483648)))
(assert (= keyboard__datalengtht__base__last 2147483647))
(assert (<= 0 keyboard__datai__size))
(assert (= keyboard__datai__first 1))
(assert (= keyboard__datai__last 78))
(assert (= keyboard__datai__base__first (- 2147483648)))
(assert (= keyboard__datai__base__last 2147483647))
(assert (<= 0 opandnullt__size))
(assert (= opandnullt__first nullop))
(assert (= opandnullt__last shutdownop))
(assert (= opandnullt__base__first nullop))
(assert (= opandnullt__base__last shutdownop))
(assert (<= 0 opt__size))
(assert (= opt__first archivelog))
(assert (= opt__last shutdownop))
(assert (= opt__base__first nullop))
(assert (= opt__base__last shutdownop))
(assert (<= 0 datalengtht__size))
(assert (= datalengtht__first 0))
(assert (= datalengtht__last 18))
(assert (= datalengtht__base__first (- 2147483648)))
(assert (= datalengtht__base__last 2147483647))
(assert (<= 0 datai__size))
(assert (= datai__first 1))
(assert (= datai__last 18))
(assert (= datai__base__first (- 2147483648)))
(assert (= datai__base__last 2147483647))
(assert (forall ((?X Int) (?Y Int)) (=> (< 0 ?Y) (<= 0 (i.mod ?X ?Y)))))
(assert (forall ((?X Int) (?Y Int)) (=> (< 0 ?Y) (< (i.mod ?X ?Y) ?Y))))
(assert (forall ((?X Int) (?Y Int)) (=> (and (<= 0 ?X) (< 0 ?Y)) (<= (i.mult ?Y (i.div ?X ?Y)) ?X))))
(assert (forall ((?X Int) (?Y Int)) (=> (and (<= 0 ?X) (< 0 ?Y)) (< (- ?X ?Y) (i.mult ?Y (i.div ?X ?Y))))))
(assert (forall ((?X Int) (?Y Int)) (=> (and (<= ?X 0) (< 0 ?Y)) (<= ?X (i.mult ?Y (i.div ?X ?Y))))))
(assert (forall ((?X Int) (?Y Int)) (=> (and (<= ?X 0) (< 0 ?Y)) (< (i.mult ?Y (i.div ?X ?Y)) (+ ?X ?Y)))))
(assert (forall ((?X Int) (?Y Int)) (=> (and (<= 0 ?X) (<= 0 ?Y)) (<= 0 (bit__or ?X ?Y)))))
(assert (forall ((?X Int) (?Y Int)) (=> (and (<= 0 ?X) (<= 0 ?Y)) (<= ?X (bit__or ?X ?Y)))))
(assert (forall ((?X Int) (?Y Int)) (=> (and (<= 0 ?X) (<= 0 ?Y)) (<= ?Y (bit__or ?X ?Y)))))
(assert (forall ((?X Int) (?Y Int)) (=> (and (<= 0 ?X) (<= 0 ?Y)) (<= (bit__or ?X ?Y) (+ ?X ?Y)))))
(assert (distinct field.datat.length field.datat.minmatchlength field.datat.text))
(assert (distinct field.keyboard__datat.length field.keyboard__datat.text))
(assert (distinct field.t.rolepresent field.t.currentop))
(assert (distinct tm.true tm.false))
(assert (forall ((?x Int)) (! (= (= (tm.not ?x) tm.true) (not (= ?x tm.true))) :pattern ((tm.not ?x)) )))
(assert (forall ((?x Int) (?y Int)) (! (= (= (tm.and ?x ?y) tm.true) (and (= ?x tm.true) (= ?y tm.true))) :pattern ((tm.and ?x ?y)) )))
(assert (forall ((?x Int) (?y Int)) (! (= (= (tm.or ?x ?y) tm.true) (or (= ?x tm.true) (= ?y tm.true))) :pattern ((tm.or ?x ?y)) )))
(assert (forall ((?x Int) (?y Int)) (! (= (= (tm.iff ?x ?y) tm.true) (= (= ?x tm.true) (= ?y tm.true))) :pattern ((tm.iff ?x ?y)) )))
(assert (forall ((?x Int) (?y Int)) (! (= (= (tm.eq ?x ?y) tm.true) (= ?x ?y)) :pattern ((tm.eq ?x ?y)) )))
(assert (forall ((?x Int) (?y Int)) (! (= (= (tm.ne ?x ?y) tm.true) (not (= ?x ?y))) :pattern ((tm.ne ?x ?y)) )))
(assert (forall ((?x Int) (?y Int)) (! (= (= (tm.lt ?x ?y) tm.true) (< ?x ?y)) :pattern ((tm.lt ?x ?y)) )))
(assert (forall ((?x Int) (?y Int)) (! (= (= (tm.le ?x ?y) tm.true) (<= ?x ?y)) :pattern ((tm.le ?x ?y)) )))
(assert (forall ((?a Int) (?i Int) (?v Int)) (! (= (a.select (a.store ?a ?i ?v) ?i) ?v) :pattern ((a.select (a.store ?a ?i ?v) ?i)) )))
(assert (forall ((?a Int) (?i Int) (?v Int) (?j Int)) (! (or (= ?i ?j) (= (a.select (a.store ?a ?i ?v) ?j) (a.select ?a ?j))) :pattern ((a.select (a.store ?a ?i ?v) ?j)) )))
(assert (forall ((?i Int) (?v Int)) (! (= (a.select (a.mk_const_array ?v) ?i) ?v) :pattern ((a.select (a.mk_const_array ?v) ?i)) )))
(assert (<= opt__first loop__1__op))
(assert (<= loop__1__op opt__last))
(assert (<= datai__first loop__2__i))
(assert (<= loop__2__i datai__last))
(assert (<= loop__2__i (a.select keyedop field.keyboard__datat.length)))
(assert (<= datai__first (a.select keyedop field.keyboard__datat.length)))
(assert (<= (a.select keyedop field.keyboard__datat.length) datai__last))
(assert (= keyedop keyedop__entry__loop__2))
(assert (<= privtypes__adminprivileget__first (a.select theadmin field.t.rolepresent)))
(assert (<= (a.select theadmin field.t.rolepresent) privtypes__adminprivileget__last))
(assert (= theop nullop))
(assert (<= opandnullt__first (a.select theadmin field.t.currentop)))
(assert (<= (a.select theadmin field.t.currentop) opandnullt__last))
(assert (<= privtypes__privileget__first (a.select theadmin field.t.rolepresent)))
(assert (<= (a.select theadmin field.t.rolepresent) privtypes__privileget__last))
(assert (forall ((?i___1 Int)) (let ((?v_0 (a.select (a.select keyedop field.keyboard__datat.text) ?i___1))) (=> (and (<= keyboard__datai__first ?i___1) (<= ?i___1 keyboard__datai__last)) (and (<= character__first ?v_0) (<= ?v_0 character__last))))))
(assert (<= keyboard__datalengtht__first (a.select keyedop field.keyboard__datat.length)))
(assert (<= (a.select keyedop field.keyboard__datat.length) keyboard__datalengtht__last))
(assert (ispresent theadmin))
(assert (<= datai__first loop__2__i))
(assert (<= loop__2__i datai__last))
(assert (<= loop__2__i (a.select keyedop__entry__loop__2 field.keyboard__datat.length)))
(assert (<= opt__first loop__1__op))
(assert (<= loop__1__op opt__last))
(assert (<= loop__1__op opt__last))
(assert (<= keyboard__datai__first loop__2__i))
(assert (<= loop__2__i keyboard__datai__last))
(assert (<= datai__first loop__2__i))
(assert (<= loop__2__i datai__last))
(assert (<= opt__first loop__1__op))
(assert (<= loop__1__op opt__last))
(assert (not (not (= (a.select (a.select (a.select optokeyed loop__1__op) field.datat.text) loop__2__i) (a.select (a.select keyedop field.keyboard__datat.text) loop__2__i)))))
(assert (not (= loop__2__i (a.select keyedop__entry__loop__2 field.keyboard__datat.length))))
(assert (let ((?v_6 (<= opt__first loop__1__op)) (?v_7 (<= loop__1__op opt__last)) (?v_1 (a.select keyedop field.keyboard__datat.length)) (?v_2 (a.select theadmin field.t.rolepresent)) (?v_3 (a.select theadmin field.t.currentop)) (?v_0 (+ loop__2__i 1))) (let ((?v_4 (<= datai__first ?v_0)) (?v_5 (<= ?v_0 datai__last))) (not (and ?v_6 ?v_7 ?v_4 ?v_5 (<= ?v_0 ?v_1) (<= datai__first ?v_1) (<= ?v_1 datai__last) (= keyedop keyedop__entry__loop__2) (<= privtypes__adminprivileget__first ?v_2) (<= ?v_2 privtypes__adminprivileget__last) (= theop nullop) (<= opandnullt__first ?v_3) (<= ?v_3 opandnullt__last) (<= privtypes__privileget__first ?v_2) (<= ?v_2 privtypes__privileget__last) (forall ((?i___1 Int)) (let ((?v_8 (a.select (a.select keyedop field.keyboard__datat.text) ?i___1))) (=> (and (<= keyboard__datai__first ?i___1) (<= ?i___1 keyboard__datai__last)) (and (<= character__first ?v_8) (<= ?v_8 character__last))))) (<= keyboard__datalengtht__first ?v_1) (<= ?v_1 keyboard__datalengtht__last) (ispresent theadmin) ?v_4 ?v_5 (<= ?v_0 (a.select keyedop__entry__loop__2 field.keyboard__datat.length)) ?v_6 ?v_7 ?v_7)))))
(check-sat)
(exit)
|
