cdaudio_false-unreach-call.i.cil.c_8.smt2 65.5 KB
Newer Older
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
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
(set-info :smt-lib-version 2.6)
(set-logic QF_ALIA)
(set-info :source "|
Generated by the tool Ultimate Automizer [1,2] which implements
an automata theoretic approach [3] to software verification.

This SMT script belongs to a set of SMT scripts that was generated by
applying Ultimate Automizer to benchmarks [4] from the SV-COMP 2019 [5,6].
This script might _not_ contain all SMT commands that are used by
Ultimate Automizer. In order to satisfy the restrictions of
the SMT-COMP we have to drop e.g., the commands for getting
values (resp. models), unsatisfiable cores and interpolants.

2019-04-27, Matthias Heizmann (heizmann@informatik.uni-freiburg.de)

[1] https://ultimate.informatik.uni-freiburg.de/automizer/
[2] Matthias Heizmann, Yu-Fang Chen, Daniel Dietsch, Marius Greitschus,
     Jochen Hoenicke, Yong Li, Alexander Nutz, Betim Musa, Christian
     Schilling, Tanja Schindler, Andreas Podelski: Ultimate Automizer
     and the Search for Perfect Interpolants - (Competition Contribution).
     TACAS (2) 2018: 447-451
[3] Matthias Heizmann, Jochen Hoenicke, Andreas Podelski: Software Model
     Checking for People Who Love Automata. CAV 2013:36-52
[4] https://github.com/sosy-lab/sv-benchmarks
[5] Dirk Beyer: Automatic Verification of C and Java Programs: SV-COMP 2019.
     TACAS (3) 2019: 133-155
[6] https://sv-comp.sosy-lab.org/2019/
|")
(set-info :license "https://creativecommons.org/licenses/by/4.0/")
(set-info :category "industrial")
(set-info :status sat)
(declare-fun |#funAddr~CdAudioNECDeviceControl.base| () Int)
(declare-fun |#funAddr~CdAudioNECDeviceControl.offset| () Int)
(declare-fun |#funAddr~CdAudioPioneerDeviceControl.base| () Int)
(declare-fun |#funAddr~CdAudioPioneerDeviceControl.offset| () Int)
(declare-fun |#funAddr~CdAudioDenonDeviceControl.base| () Int)
(declare-fun |#funAddr~CdAudioDenonDeviceControl.offset| () Int)
(declare-fun |#funAddr~CdAudioHitachiDeviceControl.base| () Int)
(declare-fun |#funAddr~CdAudioHitachiDeviceControl.offset| () Int)
(declare-fun |#funAddr~CdAudio535DeviceControl.base| () Int)
(declare-fun |#funAddr~CdAudio535DeviceControl.offset| () Int)
(declare-fun |#funAddr~CdAudio435DeviceControl.base| () Int)
(declare-fun |#funAddr~CdAudio435DeviceControl.offset| () Int)
(declare-fun |#funAddr~CdAudioAtapiDeviceControl.base| () Int)
(declare-fun |#funAddr~CdAudioAtapiDeviceControl.offset| () Int)
(declare-fun |#funAddr~CdAudioHPCdrDeviceControl.base| () Int)
(declare-fun |#funAddr~CdAudioHPCdrDeviceControl.offset| () Int)
(declare-fun |#funAddr~CdAudioSendToNextDriver.base| () Int)
(declare-fun |#funAddr~CdAudioSendToNextDriver.offset| () Int)
(declare-fun |#funAddr~CdAudioReadWrite.base| () Int)
(declare-fun |#funAddr~CdAudioReadWrite.offset| () Int)
(declare-fun |#funAddr~CdAudioDeviceControl.base| () Int)
(declare-fun |#funAddr~CdAudioDeviceControl.offset| () Int)
(declare-fun |#funAddr~CdAudioPnp.base| () Int)
(declare-fun |#funAddr~CdAudioPnp.offset| () Int)
(declare-fun |#funAddr~CdAudioPower.base| () Int)
(declare-fun |#funAddr~CdAudioPower.offset| () Int)
(declare-fun |#funAddr~CdAudioAddDevice.base| () Int)
(declare-fun |#funAddr~CdAudioAddDevice.offset| () Int)
(declare-fun |#funAddr~CdAudioUnload.base| () Int)
(declare-fun |#funAddr~CdAudioUnload.offset| () Int)
(declare-fun |#funAddr~HPCdrCompletion.base| () Int)
(declare-fun |#funAddr~HPCdrCompletion.offset| () Int)
(declare-fun |#funAddr~CdAudioSignalCompletion.base| () Int)
(declare-fun |#funAddr~CdAudioSignalCompletion.offset| () Int)
(declare-fun ~_EVENT_TYPE~0~NotificationEvent () Int)
(declare-fun ~_EVENT_TYPE~0~SynchronizationEvent () Int)
(declare-fun ~_SECURITY_IMPERSONATION_LEVEL~0~SecurityAnonymous () Int)
(declare-fun ~_SECURITY_IMPERSONATION_LEVEL~0~SecurityIdentification () Int)
(declare-fun ~_SECURITY_IMPERSONATION_LEVEL~0~SecurityImpersonation () Int)
(declare-fun ~_SECURITY_IMPERSONATION_LEVEL~0~SecurityDelegation () Int)
(declare-fun ~_FILE_INFORMATION_CLASS~0~FileDirectoryInformation () Int)
(declare-fun ~_FILE_INFORMATION_CLASS~0~FileFullDirectoryInformation () Int)
(declare-fun ~_FILE_INFORMATION_CLASS~0~FileBothDirectoryInformation () Int)
(declare-fun ~_FILE_INFORMATION_CLASS~0~FileBasicInformation () Int)
(declare-fun ~_FILE_INFORMATION_CLASS~0~FileStandardInformation () Int)
(declare-fun ~_FILE_INFORMATION_CLASS~0~FileInternalInformation () Int)
(declare-fun ~_FILE_INFORMATION_CLASS~0~FileEaInformation () Int)
(declare-fun ~_FILE_INFORMATION_CLASS~0~FileAccessInformation () Int)
(declare-fun ~_FILE_INFORMATION_CLASS~0~FileNameInformation () Int)
(declare-fun ~_FILE_INFORMATION_CLASS~0~FileRenameInformation () Int)
(declare-fun ~_FILE_INFORMATION_CLASS~0~FileLinkInformation () Int)
(declare-fun ~_FILE_INFORMATION_CLASS~0~FileNamesInformation () Int)
(declare-fun ~_FILE_INFORMATION_CLASS~0~FileDispositionInformation () Int)
(declare-fun ~_FILE_INFORMATION_CLASS~0~FilePositionInformation () Int)
(declare-fun ~_FILE_INFORMATION_CLASS~0~FileFullEaInformation () Int)
(declare-fun ~_FILE_INFORMATION_CLASS~0~FileModeInformation () Int)
(declare-fun ~_FILE_INFORMATION_CLASS~0~FileAlignmentInformation () Int)
(declare-fun ~_FILE_INFORMATION_CLASS~0~FileAllInformation () Int)
(declare-fun ~_FILE_INFORMATION_CLASS~0~FileAllocationInformation () Int)
(declare-fun ~_FILE_INFORMATION_CLASS~0~FileEndOfFileInformation () Int)
(declare-fun ~_FILE_INFORMATION_CLASS~0~FileAlternateNameInformation () Int)
(declare-fun ~_FILE_INFORMATION_CLASS~0~FileStreamInformation () Int)
(declare-fun ~_FILE_INFORMATION_CLASS~0~FilePipeInformation () Int)
(declare-fun ~_FILE_INFORMATION_CLASS~0~FilePipeLocalInformation () Int)
(declare-fun ~_FILE_INFORMATION_CLASS~0~FilePipeRemoteInformation () Int)
(declare-fun ~_FILE_INFORMATION_CLASS~0~FileMailslotQueryInformation () Int)
(declare-fun ~_FILE_INFORMATION_CLASS~0~FileMailslotSetInformation () Int)
(declare-fun ~_FILE_INFORMATION_CLASS~0~FileCompressionInformation () Int)
(declare-fun ~_FILE_INFORMATION_CLASS~0~FileObjectIdInformation () Int)
(declare-fun ~_FILE_INFORMATION_CLASS~0~FileCompletionInformation () Int)
(declare-fun ~_FILE_INFORMATION_CLASS~0~FileMoveClusterInformation () Int)
(declare-fun ~_FILE_INFORMATION_CLASS~0~FileQuotaInformation () Int)
(declare-fun ~_FILE_INFORMATION_CLASS~0~FileReparsePointInformation () Int)
(declare-fun ~_FILE_INFORMATION_CLASS~0~FileNetworkOpenInformation () Int)
(declare-fun ~_FILE_INFORMATION_CLASS~0~FileAttributeTagInformation () Int)
(declare-fun ~_FILE_INFORMATION_CLASS~0~FileTrackingInformation () Int)
(declare-fun ~_FILE_INFORMATION_CLASS~0~FileMaximumInformation () Int)
(declare-fun ~_FSINFOCLASS~0~FileFsVolumeInformation () Int)
(declare-fun ~_FSINFOCLASS~0~FileFsLabelInformation () Int)
(declare-fun ~_FSINFOCLASS~0~FileFsSizeInformation () Int)
(declare-fun ~_FSINFOCLASS~0~FileFsDeviceInformation () Int)
(declare-fun ~_FSINFOCLASS~0~FileFsAttributeInformation () Int)
(declare-fun ~_FSINFOCLASS~0~FileFsControlInformation () Int)
(declare-fun ~_FSINFOCLASS~0~FileFsFullSizeInformation () Int)
(declare-fun ~_FSINFOCLASS~0~FileFsObjectIdInformation () Int)
(declare-fun ~_FSINFOCLASS~0~FileFsMaximumInformation () Int)
(declare-fun ~_INTERFACE_TYPE~0~InterfaceTypeUndefined () Int)
(declare-fun ~_INTERFACE_TYPE~0~Internal () Int)
(declare-fun ~_INTERFACE_TYPE~0~Isa () Int)
(declare-fun ~_INTERFACE_TYPE~0~Eisa () Int)
(declare-fun ~_INTERFACE_TYPE~0~MicroChannel () Int)
(declare-fun ~_INTERFACE_TYPE~0~TurboChannel () Int)
(declare-fun ~_INTERFACE_TYPE~0~PCIBus () Int)
(declare-fun ~_INTERFACE_TYPE~0~VMEBus () Int)
(declare-fun ~_INTERFACE_TYPE~0~NuBus () Int)
(declare-fun ~_INTERFACE_TYPE~0~PCMCIABus () Int)
(declare-fun ~_INTERFACE_TYPE~0~CBus () Int)
(declare-fun ~_INTERFACE_TYPE~0~MPIBus () Int)
(declare-fun ~_INTERFACE_TYPE~0~MPSABus () Int)
(declare-fun ~_INTERFACE_TYPE~0~ProcessorInternal () Int)
(declare-fun ~_INTERFACE_TYPE~0~InternalPowerBus () Int)
(declare-fun ~_INTERFACE_TYPE~0~PNPISABus () Int)
(declare-fun ~_INTERFACE_TYPE~0~PNPBus () Int)
(declare-fun ~_INTERFACE_TYPE~0~MaximumInterfaceType () Int)
(declare-fun ~_SYSTEM_POWER_STATE~0~PowerSystemUnspecified () Int)
(declare-fun ~_SYSTEM_POWER_STATE~0~PowerSystemWorking () Int)
(declare-fun ~_SYSTEM_POWER_STATE~0~PowerSystemSleeping1 () Int)
(declare-fun ~_SYSTEM_POWER_STATE~0~PowerSystemSleeping2 () Int)
(declare-fun ~_SYSTEM_POWER_STATE~0~PowerSystemSleeping3 () Int)
(declare-fun ~_SYSTEM_POWER_STATE~0~PowerSystemHibernate () Int)
(declare-fun ~_SYSTEM_POWER_STATE~0~PowerSystemShutdown () Int)
(declare-fun ~_SYSTEM_POWER_STATE~0~PowerSystemMaximum () Int)
(declare-fun ~__anonenum_POWER_ACTION_11~0~PowerActionNone () Int)
(declare-fun ~__anonenum_POWER_ACTION_11~0~PowerActionReserved () Int)
(declare-fun ~__anonenum_POWER_ACTION_11~0~PowerActionSleep () Int)
(declare-fun ~__anonenum_POWER_ACTION_11~0~PowerActionHibernate () Int)
(declare-fun ~__anonenum_POWER_ACTION_11~0~PowerActionShutdown () Int)
(declare-fun ~__anonenum_POWER_ACTION_11~0~PowerActionShutdownReset () Int)
(declare-fun ~__anonenum_POWER_ACTION_11~0~PowerActionShutdownOff () Int)
(declare-fun ~__anonenum_POWER_ACTION_11~0~PowerActionWarmEject () Int)
(declare-fun ~_DEVICE_POWER_STATE~0~PowerDeviceUnspecified () Int)
(declare-fun ~_DEVICE_POWER_STATE~0~PowerDeviceD0 () Int)
(declare-fun ~_DEVICE_POWER_STATE~0~PowerDeviceD1 () Int)
(declare-fun ~_DEVICE_POWER_STATE~0~PowerDeviceD2 () Int)
(declare-fun ~_DEVICE_POWER_STATE~0~PowerDeviceD3 () Int)
(declare-fun ~_DEVICE_POWER_STATE~0~PowerDeviceMaximum () Int)
(declare-fun ~_POWER_STATE_TYPE~0~SystemPowerState () Int)
(declare-fun ~_POWER_STATE_TYPE~0~DevicePowerState () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~ArcSystem () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~CentralProcessor () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~FloatingPointProcessor () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~PrimaryIcache () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~PrimaryDcache () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~SecondaryIcache () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~SecondaryDcache () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~SecondaryCache () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~EisaAdapter () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~TcAdapter () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~ScsiAdapter () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~DtiAdapter () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~MultiFunctionAdapter () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~DiskController () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~TapeController () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~CdromController () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~WormController () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~SerialController () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~NetworkController () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~DisplayController () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~ParallelController () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~PointerController () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~KeyboardController () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~AudioController () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~OtherController () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~DiskPeripheral () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~FloppyDiskPeripheral () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~TapePeripheral () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~ModemPeripheral () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~MonitorPeripheral () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~PrinterPeripheral () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~PointerPeripheral () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~KeyboardPeripheral () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~TerminalPeripheral () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~OtherPeripheral () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~LinePeripheral () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~NetworkPeripheral () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~SystemMemory () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~DockingInformation () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~RealModeIrqRoutingTable () Int)
(declare-fun ~_CONFIGURATION_TYPE~0~MaximumType () Int)
(declare-fun ~_KWAIT_REASON~0~Executive () Int)
(declare-fun ~_KWAIT_REASON~0~FreePage () Int)
(declare-fun ~_KWAIT_REASON~0~PageIn () Int)
(declare-fun ~_KWAIT_REASON~0~PoolAllocation () Int)
(declare-fun ~_KWAIT_REASON~0~DelayExecution () Int)
(declare-fun ~_KWAIT_REASON~0~Suspended () Int)
(declare-fun ~_KWAIT_REASON~0~UserRequest () Int)
(declare-fun ~_KWAIT_REASON~0~WrExecutive () Int)
(declare-fun ~_KWAIT_REASON~0~WrFreePage () Int)
(declare-fun ~_KWAIT_REASON~0~WrPageIn () Int)
(declare-fun ~_KWAIT_REASON~0~WrPoolAllocation () Int)
(declare-fun ~_KWAIT_REASON~0~WrDelayExecution () Int)
(declare-fun ~_KWAIT_REASON~0~WrSuspended () Int)
(declare-fun ~_KWAIT_REASON~0~WrUserRequest () Int)
(declare-fun ~_KWAIT_REASON~0~WrEventPair () Int)
(declare-fun ~_KWAIT_REASON~0~WrQueue () Int)
(declare-fun ~_KWAIT_REASON~0~WrLpcReceive () Int)
(declare-fun ~_KWAIT_REASON~0~WrLpcReply () Int)
(declare-fun ~_KWAIT_REASON~0~WrVirtualMemory () Int)
(declare-fun ~_KWAIT_REASON~0~WrPageOut () Int)
(declare-fun ~_KWAIT_REASON~0~WrRendezvous () Int)
(declare-fun ~_KWAIT_REASON~0~Spare2 () Int)
(declare-fun ~_KWAIT_REASON~0~Spare3 () Int)
(declare-fun ~_KWAIT_REASON~0~Spare4 () Int)
(declare-fun ~_KWAIT_REASON~0~Spare5 () Int)
(declare-fun ~_KWAIT_REASON~0~Spare6 () Int)
(declare-fun ~_KWAIT_REASON~0~WrKernel () Int)
(declare-fun ~_KWAIT_REASON~0~MaximumWaitReason () Int)
(declare-fun ~_MEMORY_CACHING_TYPE~0~MmNonCached () Int)
(declare-fun ~_MEMORY_CACHING_TYPE~0~MmCached () Int)
(declare-fun ~_MEMORY_CACHING_TYPE~0~MmWriteCombined () Int)
(declare-fun ~_MEMORY_CACHING_TYPE~0~MmHardwareCoherentCached () Int)
(declare-fun ~_MEMORY_CACHING_TYPE~0~MmNonCachedUnordered () Int)
(declare-fun ~_MEMORY_CACHING_TYPE~0~MmUSWCCached () Int)
(declare-fun ~_MEMORY_CACHING_TYPE~0~MmMaximumCacheType () Int)
(declare-fun ~_POOL_TYPE~0~NonPagedPool () Int)
(declare-fun ~_POOL_TYPE~0~PagedPool () Int)
(declare-fun ~_POOL_TYPE~0~NonPagedPoolMustSucceed () Int)
(declare-fun ~_POOL_TYPE~0~DontUseThisType () Int)
(declare-fun ~_POOL_TYPE~0~NonPagedPoolCacheAligned () Int)
(declare-fun ~_POOL_TYPE~0~PagedPoolCacheAligned () Int)
(declare-fun ~_POOL_TYPE~0~NonPagedPoolCacheAlignedMustS () Int)
(declare-fun ~_POOL_TYPE~0~MaxPoolType () Int)
(declare-fun ~_POOL_TYPE~0~NonPagedPoolSession () Int)
(declare-fun ~_POOL_TYPE~0~PagedPoolSession () Int)
(declare-fun ~_POOL_TYPE~0~NonPagedPoolMustSucceedSession () Int)
(declare-fun ~_POOL_TYPE~0~DontUseThisTypeSession () Int)
(declare-fun ~_POOL_TYPE~0~NonPagedPoolCacheAlignedSession () Int)
(declare-fun ~_POOL_TYPE~0~PagedPoolCacheAlignedSession () Int)
(declare-fun ~_POOL_TYPE~0~NonPagedPoolCacheAlignedMustSSession () Int)
(declare-fun ~_MM_PAGE_PRIORITY~0~LowPagePriority () Int)
(declare-fun ~_MM_PAGE_PRIORITY~0~NormalPagePriority () Int)
(declare-fun ~_MM_PAGE_PRIORITY~0~HighPagePriority () Int)
(declare-fun ~_IO_ALLOCATION_ACTION~0~KeepObject () Int)
(declare-fun ~_IO_ALLOCATION_ACTION~0~DeallocateObject () Int)
(declare-fun ~_IO_ALLOCATION_ACTION~0~DeallocateObjectKeepRegisters () Int)
(declare-fun ~_DEVICE_RELATION_TYPE~0~BusRelations () Int)
(declare-fun ~_DEVICE_RELATION_TYPE~0~EjectionRelations () Int)
(declare-fun ~_DEVICE_RELATION_TYPE~0~PowerRelations () Int)
(declare-fun ~_DEVICE_RELATION_TYPE~0~RemovalRelations () Int)
(declare-fun ~_DEVICE_RELATION_TYPE~0~TargetDeviceRelation () Int)
(declare-fun ~_DEVICE_USAGE_NOTIFICATION_TYPE~0~DeviceUsageTypeUndefined () Int)
(declare-fun ~_DEVICE_USAGE_NOTIFICATION_TYPE~0~DeviceUsageTypePaging () Int)
(declare-fun ~_DEVICE_USAGE_NOTIFICATION_TYPE~0~DeviceUsageTypeHibernation () Int)
(declare-fun ~_DEVICE_USAGE_NOTIFICATION_TYPE~0~DeviceUsageTypeDumpFile () Int)
(declare-fun ~__anonenum_BUS_QUERY_ID_TYPE_53~0~BusQueryDeviceID () Int)
(declare-fun ~__anonenum_BUS_QUERY_ID_TYPE_53~0~BusQueryHardwareIDs () Int)
(declare-fun ~__anonenum_BUS_QUERY_ID_TYPE_53~0~BusQueryCompatibleIDs () Int)
(declare-fun ~__anonenum_BUS_QUERY_ID_TYPE_53~0~BusQueryInstanceID () Int)
(declare-fun ~__anonenum_BUS_QUERY_ID_TYPE_53~0~BusQueryDeviceSerialNumber () Int)
(declare-fun ~__anonenum_DEVICE_TEXT_TYPE_54~0~DeviceTextDescription () Int)
(declare-fun ~__anonenum_DEVICE_TEXT_TYPE_54~0~DeviceTextLocationInformation () Int)
(assert (and (= |#funAddr~CdAudioNECDeviceControl.base| (- 1)) (= |#funAddr~CdAudioNECDeviceControl.offset| 0)))
(assert (and (= |#funAddr~CdAudioPioneerDeviceControl.offset| 1) (= (- 1) |#funAddr~CdAudioPioneerDeviceControl.base|)))
(assert (and (= (- 1) |#funAddr~CdAudioDenonDeviceControl.base|) (= 2 |#funAddr~CdAudioDenonDeviceControl.offset|)))
(assert (and (= 3 |#funAddr~CdAudioHitachiDeviceControl.offset|) (= (- 1) |#funAddr~CdAudioHitachiDeviceControl.base|)))
(assert (and (= (- 1) |#funAddr~CdAudio535DeviceControl.base|) (= 4 |#funAddr~CdAudio535DeviceControl.offset|)))
(assert (and (= 5 |#funAddr~CdAudio435DeviceControl.offset|) (= |#funAddr~CdAudio435DeviceControl.base| (- 1))))
(assert (and (= (- 1) |#funAddr~CdAudioAtapiDeviceControl.base|) (= |#funAddr~CdAudioAtapiDeviceControl.offset| 6)))
(assert (and (= (- 1) |#funAddr~CdAudioHPCdrDeviceControl.base|) (= |#funAddr~CdAudioHPCdrDeviceControl.offset| 7)))
(assert (and (= 8 |#funAddr~CdAudioSendToNextDriver.offset|) (= (- 1) |#funAddr~CdAudioSendToNextDriver.base|)))
(assert (and (= |#funAddr~CdAudioReadWrite.base| (- 1)) (= 9 |#funAddr~CdAudioReadWrite.offset|)))
(assert (and (= |#funAddr~CdAudioDeviceControl.base| (- 1)) (= 10 |#funAddr~CdAudioDeviceControl.offset|)))
(assert (and (= (- 1) |#funAddr~CdAudioPnp.base|) (= |#funAddr~CdAudioPnp.offset| 11)))
(assert (and (= |#funAddr~CdAudioPower.base| (- 1)) (= 12 |#funAddr~CdAudioPower.offset|)))
(assert (and (= |#funAddr~CdAudioAddDevice.offset| 13) (= (- 1) |#funAddr~CdAudioAddDevice.base|)))
(assert (and (= (- 1) |#funAddr~CdAudioUnload.base|) (= |#funAddr~CdAudioUnload.offset| 14)))
(assert (and (= |#funAddr~HPCdrCompletion.offset| 15) (= |#funAddr~HPCdrCompletion.base| (- 1))))
(assert (and (= |#funAddr~CdAudioSignalCompletion.base| (- 1)) (= 16 |#funAddr~CdAudioSignalCompletion.offset|)))
(assert (= ~_EVENT_TYPE~0~NotificationEvent 0))
(assert (= ~_EVENT_TYPE~0~SynchronizationEvent 1))
(assert (= 0 ~_SECURITY_IMPERSONATION_LEVEL~0~SecurityAnonymous))
(assert (= ~_SECURITY_IMPERSONATION_LEVEL~0~SecurityIdentification 1))
(assert (= ~_SECURITY_IMPERSONATION_LEVEL~0~SecurityImpersonation 2))
(assert (= 3 ~_SECURITY_IMPERSONATION_LEVEL~0~SecurityDelegation))
(assert (= 1 ~_FILE_INFORMATION_CLASS~0~FileDirectoryInformation))
(assert (= ~_FILE_INFORMATION_CLASS~0~FileFullDirectoryInformation 2))
(assert (= 3 ~_FILE_INFORMATION_CLASS~0~FileBothDirectoryInformation))
(assert (= 4 ~_FILE_INFORMATION_CLASS~0~FileBasicInformation))
(assert (= ~_FILE_INFORMATION_CLASS~0~FileStandardInformation 5))
(assert (= ~_FILE_INFORMATION_CLASS~0~FileInternalInformation 6))
(assert (= 7 ~_FILE_INFORMATION_CLASS~0~FileEaInformation))
(assert (= 8 ~_FILE_INFORMATION_CLASS~0~FileAccessInformation))
(assert (= ~_FILE_INFORMATION_CLASS~0~FileNameInformation 9))
(assert (= ~_FILE_INFORMATION_CLASS~0~FileRenameInformation 10))
(assert (= 11 ~_FILE_INFORMATION_CLASS~0~FileLinkInformation))
(assert (= 12 ~_FILE_INFORMATION_CLASS~0~FileNamesInformation))
(assert (= ~_FILE_INFORMATION_CLASS~0~FileDispositionInformation 13))
(assert (= ~_FILE_INFORMATION_CLASS~0~FilePositionInformation 14))
(assert (= 15 ~_FILE_INFORMATION_CLASS~0~FileFullEaInformation))
(assert (= 16 ~_FILE_INFORMATION_CLASS~0~FileModeInformation))
(assert (= 17 ~_FILE_INFORMATION_CLASS~0~FileAlignmentInformation))
(assert (= ~_FILE_INFORMATION_CLASS~0~FileAllInformation 18))
(assert (= 19 ~_FILE_INFORMATION_CLASS~0~FileAllocationInformation))
(assert (= 20 ~_FILE_INFORMATION_CLASS~0~FileEndOfFileInformation))
(assert (= 21 ~_FILE_INFORMATION_CLASS~0~FileAlternateNameInformation))
(assert (= 22 ~_FILE_INFORMATION_CLASS~0~FileStreamInformation))
(assert (= 23 ~_FILE_INFORMATION_CLASS~0~FilePipeInformation))
(assert (= ~_FILE_INFORMATION_CLASS~0~FilePipeLocalInformation 24))
(assert (= 25 ~_FILE_INFORMATION_CLASS~0~FilePipeRemoteInformation))
(assert (= 26 ~_FILE_INFORMATION_CLASS~0~FileMailslotQueryInformation))
(assert (= ~_FILE_INFORMATION_CLASS~0~FileMailslotSetInformation 27))
(assert (= ~_FILE_INFORMATION_CLASS~0~FileCompressionInformation 28))
(assert (= ~_FILE_INFORMATION_CLASS~0~FileObjectIdInformation 29))
(assert (= ~_FILE_INFORMATION_CLASS~0~FileCompletionInformation 30))
(assert (= ~_FILE_INFORMATION_CLASS~0~FileMoveClusterInformation 31))
(assert (= ~_FILE_INFORMATION_CLASS~0~FileQuotaInformation 32))
(assert (= ~_FILE_INFORMATION_CLASS~0~FileReparsePointInformation 33))
(assert (= ~_FILE_INFORMATION_CLASS~0~FileNetworkOpenInformation 34))
(assert (= 35 ~_FILE_INFORMATION_CLASS~0~FileAttributeTagInformation))
(assert (= 36 ~_FILE_INFORMATION_CLASS~0~FileTrackingInformation))
(assert (= 37 ~_FILE_INFORMATION_CLASS~0~FileMaximumInformation))
(assert (= 1 ~_FSINFOCLASS~0~FileFsVolumeInformation))
(assert (= ~_FSINFOCLASS~0~FileFsLabelInformation 2))
(assert (= 3 ~_FSINFOCLASS~0~FileFsSizeInformation))
(assert (= 4 ~_FSINFOCLASS~0~FileFsDeviceInformation))
(assert (= ~_FSINFOCLASS~0~FileFsAttributeInformation 5))
(assert (= ~_FSINFOCLASS~0~FileFsControlInformation 6))
(assert (= ~_FSINFOCLASS~0~FileFsFullSizeInformation 7))
(assert (= ~_FSINFOCLASS~0~FileFsObjectIdInformation 8))
(assert (= ~_FSINFOCLASS~0~FileFsMaximumInformation 9))
(assert (= (- 1) ~_INTERFACE_TYPE~0~InterfaceTypeUndefined))
(assert (= 0 ~_INTERFACE_TYPE~0~Internal))
(assert (= 1 ~_INTERFACE_TYPE~0~Isa))
(assert (= 2 ~_INTERFACE_TYPE~0~Eisa))
(assert (= ~_INTERFACE_TYPE~0~MicroChannel 3))
(assert (= 4 ~_INTERFACE_TYPE~0~TurboChannel))
(assert (= ~_INTERFACE_TYPE~0~PCIBus 5))
(assert (= ~_INTERFACE_TYPE~0~VMEBus 6))
(assert (= ~_INTERFACE_TYPE~0~NuBus 7))
(assert (= 8 ~_INTERFACE_TYPE~0~PCMCIABus))
(assert (= 9 ~_INTERFACE_TYPE~0~CBus))
(assert (= ~_INTERFACE_TYPE~0~MPIBus 10))
(assert (= ~_INTERFACE_TYPE~0~MPSABus 11))
(assert (= 12 ~_INTERFACE_TYPE~0~ProcessorInternal))
(assert (= 13 ~_INTERFACE_TYPE~0~InternalPowerBus))
(assert (= 14 ~_INTERFACE_TYPE~0~PNPISABus))
(assert (= ~_INTERFACE_TYPE~0~PNPBus 15))
(assert (= ~_INTERFACE_TYPE~0~MaximumInterfaceType 16))
(assert (= 0 ~_SYSTEM_POWER_STATE~0~PowerSystemUnspecified))
(assert (= 1 ~_SYSTEM_POWER_STATE~0~PowerSystemWorking))
(assert (= ~_SYSTEM_POWER_STATE~0~PowerSystemSleeping1 2))
(assert (= ~_SYSTEM_POWER_STATE~0~PowerSystemSleeping2 3))
(assert (= ~_SYSTEM_POWER_STATE~0~PowerSystemSleeping3 4))
(assert (= ~_SYSTEM_POWER_STATE~0~PowerSystemHibernate 5))
(assert (= ~_SYSTEM_POWER_STATE~0~PowerSystemShutdown 6))
(assert (= 7 ~_SYSTEM_POWER_STATE~0~PowerSystemMaximum))
(assert (= 0 ~__anonenum_POWER_ACTION_11~0~PowerActionNone))
(assert (= 1 ~__anonenum_POWER_ACTION_11~0~PowerActionReserved))
(assert (= ~__anonenum_POWER_ACTION_11~0~PowerActionSleep 2))
(assert (= 3 ~__anonenum_POWER_ACTION_11~0~PowerActionHibernate))
(assert (= 4 ~__anonenum_POWER_ACTION_11~0~PowerActionShutdown))
(assert (= 5 ~__anonenum_POWER_ACTION_11~0~PowerActionShutdownReset))
(assert (= 6 ~__anonenum_POWER_ACTION_11~0~PowerActionShutdownOff))
(assert (= ~__anonenum_POWER_ACTION_11~0~PowerActionWarmEject 7))
(assert (= 0 ~_DEVICE_POWER_STATE~0~PowerDeviceUnspecified))
(assert (= 1 ~_DEVICE_POWER_STATE~0~PowerDeviceD0))
(assert (= 2 ~_DEVICE_POWER_STATE~0~PowerDeviceD1))
(assert (= 3 ~_DEVICE_POWER_STATE~0~PowerDeviceD2))
(assert (= 4 ~_DEVICE_POWER_STATE~0~PowerDeviceD3))
(assert (= ~_DEVICE_POWER_STATE~0~PowerDeviceMaximum 5))
(assert (= 0 ~_POWER_STATE_TYPE~0~SystemPowerState))
(assert (= ~_POWER_STATE_TYPE~0~DevicePowerState 1))
(assert (= 0 ~_CONFIGURATION_TYPE~0~ArcSystem))
(assert (= 1 ~_CONFIGURATION_TYPE~0~CentralProcessor))
(assert (= 2 ~_CONFIGURATION_TYPE~0~FloatingPointProcessor))
(assert (= 3 ~_CONFIGURATION_TYPE~0~PrimaryIcache))
(assert (= 4 ~_CONFIGURATION_TYPE~0~PrimaryDcache))
(assert (= 5 ~_CONFIGURATION_TYPE~0~SecondaryIcache))
(assert (= 6 ~_CONFIGURATION_TYPE~0~SecondaryDcache))
(assert (= ~_CONFIGURATION_TYPE~0~SecondaryCache 7))
(assert (= ~_CONFIGURATION_TYPE~0~EisaAdapter 8))
(assert (= 9 ~_CONFIGURATION_TYPE~0~TcAdapter))
(assert (= 10 ~_CONFIGURATION_TYPE~0~ScsiAdapter))
(assert (= 11 ~_CONFIGURATION_TYPE~0~DtiAdapter))
(assert (= ~_CONFIGURATION_TYPE~0~MultiFunctionAdapter 12))
(assert (= ~_CONFIGURATION_TYPE~0~DiskController 13))
(assert (= ~_CONFIGURATION_TYPE~0~TapeController 14))
(assert (= ~_CONFIGURATION_TYPE~0~CdromController 15))
(assert (= 16 ~_CONFIGURATION_TYPE~0~WormController))
(assert (= ~_CONFIGURATION_TYPE~0~SerialController 17))
(assert (= ~_CONFIGURATION_TYPE~0~NetworkController 18))
(assert (= 19 ~_CONFIGURATION_TYPE~0~DisplayController))
(assert (= ~_CONFIGURATION_TYPE~0~ParallelController 20))
(assert (= ~_CONFIGURATION_TYPE~0~PointerController 21))
(assert (= ~_CONFIGURATION_TYPE~0~KeyboardController 22))
(assert (= ~_CONFIGURATION_TYPE~0~AudioController 23))
(assert (= 24 ~_CONFIGURATION_TYPE~0~OtherController))
(assert (= ~_CONFIGURATION_TYPE~0~DiskPeripheral 25))
(assert (= ~_CONFIGURATION_TYPE~0~FloppyDiskPeripheral 26))
(assert (= ~_CONFIGURATION_TYPE~0~TapePeripheral 27))
(assert (= 28 ~_CONFIGURATION_TYPE~0~ModemPeripheral))
(assert (= 29 ~_CONFIGURATION_TYPE~0~MonitorPeripheral))
(assert (= 30 ~_CONFIGURATION_TYPE~0~PrinterPeripheral))
(assert (= ~_CONFIGURATION_TYPE~0~PointerPeripheral 31))
(assert (= ~_CONFIGURATION_TYPE~0~KeyboardPeripheral 32))
(assert (= 33 ~_CONFIGURATION_TYPE~0~TerminalPeripheral))
(assert (= 34 ~_CONFIGURATION_TYPE~0~OtherPeripheral))
(assert (= ~_CONFIGURATION_TYPE~0~LinePeripheral 35))
(assert (= ~_CONFIGURATION_TYPE~0~NetworkPeripheral 36))
(assert (= 37 ~_CONFIGURATION_TYPE~0~SystemMemory))
(assert (= ~_CONFIGURATION_TYPE~0~DockingInformation 38))
(assert (= 39 ~_CONFIGURATION_TYPE~0~RealModeIrqRoutingTable))
(assert (= 40 ~_CONFIGURATION_TYPE~0~MaximumType))
(assert (= ~_KWAIT_REASON~0~Executive 0))
(assert (= 1 ~_KWAIT_REASON~0~FreePage))
(assert (= 2 ~_KWAIT_REASON~0~PageIn))
(assert (= ~_KWAIT_REASON~0~PoolAllocation 3))
(assert (= ~_KWAIT_REASON~0~DelayExecution 4))
(assert (= ~_KWAIT_REASON~0~Suspended 5))
(assert (= 6 ~_KWAIT_REASON~0~UserRequest))
(assert (= 7 ~_KWAIT_REASON~0~WrExecutive))
(assert (= 8 ~_KWAIT_REASON~0~WrFreePage))
(assert (= ~_KWAIT_REASON~0~WrPageIn 9))
(assert (= 10 ~_KWAIT_REASON~0~WrPoolAllocation))
(assert (= ~_KWAIT_REASON~0~WrDelayExecution 11))
(assert (= 12 ~_KWAIT_REASON~0~WrSuspended))
(assert (= 13 ~_KWAIT_REASON~0~WrUserRequest))
(assert (= 14 ~_KWAIT_REASON~0~WrEventPair))
(assert (= ~_KWAIT_REASON~0~WrQueue 15))
(assert (= ~_KWAIT_REASON~0~WrLpcReceive 16))
(assert (= 17 ~_KWAIT_REASON~0~WrLpcReply))
(assert (= ~_KWAIT_REASON~0~WrVirtualMemory 18))
(assert (= 19 ~_KWAIT_REASON~0~WrPageOut))
(assert (= 20 ~_KWAIT_REASON~0~WrRendezvous))
(assert (= 21 ~_KWAIT_REASON~0~Spare2))
(assert (= 22 ~_KWAIT_REASON~0~Spare3))
(assert (= 23 ~_KWAIT_REASON~0~Spare4))
(assert (= 24 ~_KWAIT_REASON~0~Spare5))
(assert (= 25 ~_KWAIT_REASON~0~Spare6))
(assert (= ~_KWAIT_REASON~0~WrKernel 26))
(assert (= 27 ~_KWAIT_REASON~0~MaximumWaitReason))
(assert (= 0 ~_MEMORY_CACHING_TYPE~0~MmNonCached))
(assert (= ~_MEMORY_CACHING_TYPE~0~MmCached 1))
(assert (= ~_MEMORY_CACHING_TYPE~0~MmWriteCombined 2))
(assert (= ~_MEMORY_CACHING_TYPE~0~MmHardwareCoherentCached 3))
(assert (= 4 ~_MEMORY_CACHING_TYPE~0~MmNonCachedUnordered))
(assert (= ~_MEMORY_CACHING_TYPE~0~MmUSWCCached 5))
(assert (= 6 ~_MEMORY_CACHING_TYPE~0~MmMaximumCacheType))
(assert (= 0 ~_POOL_TYPE~0~NonPagedPool))
(assert (= 1 ~_POOL_TYPE~0~PagedPool))
(assert (= 2 ~_POOL_TYPE~0~NonPagedPoolMustSucceed))
(assert (= 3 ~_POOL_TYPE~0~DontUseThisType))
(assert (= 4 ~_POOL_TYPE~0~NonPagedPoolCacheAligned))
(assert (= ~_POOL_TYPE~0~PagedPoolCacheAligned 5))
(assert (= ~_POOL_TYPE~0~NonPagedPoolCacheAlignedMustS 6))
(assert (= 7 ~_POOL_TYPE~0~MaxPoolType))
(assert (= 32 ~_POOL_TYPE~0~NonPagedPoolSession))
(assert (= 33 ~_POOL_TYPE~0~PagedPoolSession))
(assert (= 34 ~_POOL_TYPE~0~NonPagedPoolMustSucceedSession))
(assert (= 35 ~_POOL_TYPE~0~DontUseThisTypeSession))
(assert (= ~_POOL_TYPE~0~NonPagedPoolCacheAlignedSession 36))
(assert (= 37 ~_POOL_TYPE~0~PagedPoolCacheAlignedSession))
(assert (= ~_POOL_TYPE~0~NonPagedPoolCacheAlignedMustSSession 38))
(assert (= 0 ~_MM_PAGE_PRIORITY~0~LowPagePriority))
(assert (= 16 ~_MM_PAGE_PRIORITY~0~NormalPagePriority))
(assert (= 32 ~_MM_PAGE_PRIORITY~0~HighPagePriority))
(assert (= ~_IO_ALLOCATION_ACTION~0~KeepObject 1))
(assert (= ~_IO_ALLOCATION_ACTION~0~DeallocateObject 2))
(assert (= 3 ~_IO_ALLOCATION_ACTION~0~DeallocateObjectKeepRegisters))
(assert (= ~_DEVICE_RELATION_TYPE~0~BusRelations 0))
(assert (= ~_DEVICE_RELATION_TYPE~0~EjectionRelations 1))
(assert (= ~_DEVICE_RELATION_TYPE~0~PowerRelations 2))
(assert (= ~_DEVICE_RELATION_TYPE~0~RemovalRelations 3))
(assert (= 4 ~_DEVICE_RELATION_TYPE~0~TargetDeviceRelation))
(assert (= 0 ~_DEVICE_USAGE_NOTIFICATION_TYPE~0~DeviceUsageTypeUndefined))
(assert (= ~_DEVICE_USAGE_NOTIFICATION_TYPE~0~DeviceUsageTypePaging 1))
(assert (= 2 ~_DEVICE_USAGE_NOTIFICATION_TYPE~0~DeviceUsageTypeHibernation))
(assert (= ~_DEVICE_USAGE_NOTIFICATION_TYPE~0~DeviceUsageTypeDumpFile 3))
(assert (= ~__anonenum_BUS_QUERY_ID_TYPE_53~0~BusQueryDeviceID 0))
(assert (= ~__anonenum_BUS_QUERY_ID_TYPE_53~0~BusQueryHardwareIDs 1))
(assert (= 2 ~__anonenum_BUS_QUERY_ID_TYPE_53~0~BusQueryCompatibleIDs))
(assert (= ~__anonenum_BUS_QUERY_ID_TYPE_53~0~BusQueryInstanceID 3))
(assert (= 4 ~__anonenum_BUS_QUERY_ID_TYPE_53~0~BusQueryDeviceSerialNumber))
(assert (= 0 ~__anonenum_DEVICE_TEXT_TYPE_54~0~DeviceTextDescription))
(assert (= 1 ~__anonenum_DEVICE_TEXT_TYPE_54~0~DeviceTextLocationInformation))
(declare-fun |v_#memory_$Pointer$.offset_1517_const_-574584726| () (Array Int (Array Int Int)))
(declare-fun v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 () Int)
(declare-fun v_CdAudioHitachiDeviceControl_~Irp.offset_20_const_673585352 () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union774.Thread.offset_2_const_-157300445| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union774.ApcListEntry.Flink.offset_2_const_309159339| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union774.ApcListEntry.Blink.offset_2_const_-1963701209| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union774.KernelRoutine.offset_2_const_-1289389500| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union774.RundownRoutine.offset_2_const_640721136| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union774.NormalRoutine.offset_2_const_-457417222| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union774.NormalContext.offset_2_const_-2103977371| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union774.SystemArgument1.offset_2_const_810108450| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union774.SystemArgument2.offset_2_const_613471427| () Int)
(declare-fun |v_#memory_$Pointer$.offset_1507_const_-574584747| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_1160_const_1186198539| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_1161_const_1186198538| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_1519_const_-42853450| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_1521_const_-42853553| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_1173_const_1186198581| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_1174_const_1186198580| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_1151_const_1186198645| () (Array Int (Array Int Int)))
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union780_2_const_-1566705455| () Int)
(declare-fun |v_#memory_int_1150_const_1186198634| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_1178_const_1186198576| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_1179_const_1186198579| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_1518_const_-574584715| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_1157_const_1186198643| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_1158_const_1186198642| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_1175_const_1186198583| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_1519_const_-574584716| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_1521_const_-574584819| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_1503_const_-574584759| () (Array Int (Array Int Int)))
(declare-fun v_CdAudioHitachiDeviceControl_~cdaudioDataOut~3.offset_10_const_143392562 () Int)
(declare-fun |v_#memory_$Pointer$.offset_1505_const_-574584757| () (Array Int (Array Int Int)))
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union775.offset_2_const_707431692| () Int)
(declare-fun |v_#memory_$Pointer$.base_1535_const_-42853528| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_1536_const_-42853525| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_1180_const_1186198985| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_1181_const_1186198984| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_1506_const_-574584758| () (Array Int (Array Int Int)))
(declare-fun |v_#valid_76_const_-1605542317| () (Array Int Bool))
(declare-fun |v_CdAudioHitachiDeviceControl_~#srb~5.base_16_const_1039272055| () Int)
(declare-fun v_CdAudioHitachiDeviceControl_~DeviceObject.base_8_const_-1187297464 () Int)
(declare-fun v_CdAudioHitachiDeviceControl_~DeviceObject.offset_8_const_-1919963834 () Int)
(declare-fun v_CdAudioHitachiDeviceControl_~deviceExtension~10.offset_18_const_-1804285158 () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union774.ApcStateIndex_2_const_-1864459867| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union774.ApcMode_2_const_299751043| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union774.Inserted_2_const_489070150| () Int)
(declare-fun |v_#memory_int_1153_const_1186198647| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_1503_const_-42853493| () (Array Int (Array Int Int)))
(declare-fun v_CdAudioHitachiDeviceControl_~deviceExtension~10.base_18_const_1540097432 () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#in~DeviceObject.base_1_const_401750923| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_~#srb~5.offset_16_const_-2062345543| () Int)
(declare-fun |v_#memory_int_1159_const_1186198653| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_1169_const_1186198546| () (Array Int (Array Int Int)))
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union774.Type_2_const_765396452| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union774.Size_2_const_722291453| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union774.Spare0_2_const_-509007835| () Int)
(declare-fun |v_#memory_int_1165_const_1186198550| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_1533_const_-574584788| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_1534_const_-574584785| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_1501_const_-42853495| () (Array Int (Array Int Int)))
(declare-fun |v_#StackHeapBarrier_5_const_531197052| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union772.ApcStateIndex_2_const_-276114009| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union772.ApcMode_2_const_-401441787| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union772.Inserted_2_const_231024900| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#in~Irp.offset_1_const_1942582475| () Int)
(declare-fun |v_#memory_int_1176_const_1186198582| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_1177_const_1186198577| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_1536_const_-574584791| () (Array Int (Array Int Int)))
(declare-fun v_CdAudioHitachiDeviceControl_~currentIrpStack~3.offset_14_const_2052058715 () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#in~Irp.base_1_const_-1808968115| () Int)
(declare-fun |v_#valid_75_const_-1605542316| () (Array Int Bool))
(declare-fun |v_#memory_$Pointer$.base_1505_const_-42853483| () (Array Int (Array Int Int)))
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union775.base_2_const_-1408018674| () Int)
(declare-fun v_CdAudioHitachiDeviceControl_~cdb~5.offset_7_const_253752466 () Int)
(declare-fun v_CdAudioHitachiDeviceControl_~cdb~5.base_7_const_1371397460 () Int)
(declare-fun |v_#memory_$Pointer$.base_1522_const_-42853554| () (Array Int (Array Int Int)))
(declare-fun v_CdAudioHitachiDeviceControl_~cdaudioDataOut~3.base_10_const_-115970640 () Int)
(declare-fun |v_#memory_$Pointer$.offset_1501_const_-574584753| () (Array Int (Array Int Int)))
(declare-fun |v_CdAudioHitachiDeviceControl_#in~DeviceObject.offset_1_const_558006921| () Int)
(declare-fun |v_#memory_$Pointer$.base_1517_const_-42853452| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_1518_const_-42853449| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_1523_const_-42853559| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_1535_const_-574584786| () (Array Int (Array Int Int)))
(declare-fun |v_#length_66_const_-660983928| () (Array Int Int))
(declare-fun |v_#length_65_const_-660983927| () (Array Int Int))
(declare-fun |v_#memory_$Pointer$.base_1506_const_-42853484| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_1507_const_-42853481| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_1185_const_1186198996| () (Array Int (Array Int Int)))
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union772.Type_2_const_1574625186| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union772.Size_2_const_1531503803| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union772.Spare0_2_const_-116110749| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union774.Thread.base_2_const_2108398821| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union774.ApcListEntry.Flink.base_2_const_754695021| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union774.ApcListEntry.Blink.base_2_const_238358761| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union774.KernelRoutine.base_2_const_19935814| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union774.RundownRoutine.base_2_const_57703410| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union774.NormalRoutine.base_2_const_-372493444| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union774.NormalContext.base_2_const_-2018896217| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union774.SystemArgument1.base_2_const_-701772380| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union774.SystemArgument2.base_2_const_1040900229| () Int)
(declare-fun |v_#memory_$Pointer$.offset_1522_const_-574584820| () (Array Int (Array Int Int)))
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union772.Thread.offset_2_const_1430914341| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union772.ApcListEntry.Flink.offset_2_const_-1077039443| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union772.ApcListEntry.Blink.offset_2_const_945067305| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union772.KernelRoutine.offset_2_const_-1155508222| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union772.RundownRoutine.offset_2_const_500185842| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union772.NormalRoutine.offset_2_const_-323273800| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union772.NormalContext.offset_2_const_-1970096093| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union772.SystemArgument1.offset_2_const_747940960| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union772.SystemArgument2.offset_2_const_551435009| () Int)
(declare-fun |v_#memory_$Pointer$.offset_1523_const_-574584817| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_1162_const_1186198549| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_1163_const_1186198548| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_1533_const_-42853522| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_1534_const_-42853527| () (Array Int (Array Int Int)))
(declare-fun v_CdAudioHitachiDeviceControl_~currentIrpStack~3.base_14_const_2143130649 () Int)
(declare-fun |v_#memory_int_1164_const_1186198551| () (Array Int (Array Int Int)))
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union776_2_const_-1566730614| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union772.Thread.base_2_const_-906841753| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union772.ApcListEntry.Flink.base_2_const_-1168532241| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union772.ApcListEntry.Blink.base_2_const_-1684999573| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union772.KernelRoutine.base_2_const_-198924412| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union772.RundownRoutine.base_2_const_1863265908| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union772.NormalRoutine.base_2_const_-591353670| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union772.NormalContext.base_2_const_2057210853| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union772.SystemArgument1.base_2_const_-567891102| () Int)
(declare-fun |v_CdAudioHitachiDeviceControl_#t~union772.SystemArgument2.base_2_const_1175060035| () Int)
(assert (let ((.cse6 (select |v_#memory_int_1174_const_1186198580| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse24 (select |v_#memory_$Pointer$.offset_1505_const_-574584757| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse18 (select |v_#memory_int_1157_const_1186198643| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse31 (select |v_#memory_$Pointer$.offset_1506_const_-574584758| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse33 (+ v_CdAudioHitachiDeviceControl_~DeviceObject.offset_8_const_-1919963834 76)) (.cse2 (select |v_#memory_int_1160_const_1186198539| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse39 (select |v_#memory_int_1159_const_1186198653| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse17 (select |v_#memory_int_1158_const_1186198642| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse8 (select |v_#memory_int_1173_const_1186198581| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse40 (select |v_#memory_int_1169_const_1186198546| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse3 (select |v_#memory_$Pointer$.base_1521_const_-42853553| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse16 (select |v_#memory_$Pointer$.offset_1517_const_-574584726| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse37 (select |v_#memory_$Pointer$.offset_1507_const_-574584747| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse46 (select |v_#memory_$Pointer$.base_1503_const_-42853493| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse23 (select |v_#memory_$Pointer$.offset_1503_const_-574584759| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse51 (select |v_#memory_$Pointer$.base_1522_const_-42853554| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse44 (select |v_#memory_$Pointer$.offset_1534_const_-574584785| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse5 (select |v_#memory_$Pointer$.base_1519_const_-42853450| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse54 (select |v_#memory_$Pointer$.base_1518_const_-42853449| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse49 (select |v_#memory_$Pointer$.offset_1536_const_-574584791| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse57 (select |v_#memory_$Pointer$.offset_1535_const_-574584786| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse30 (select |v_#memory_int_1180_const_1186198985| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse11 (select |v_#memory_int_1179_const_1186198579| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse4 (+ v_CdAudioHitachiDeviceControl_~Irp.offset_20_const_673585352 116)) (.cse28 (select |v_#memory_int_1181_const_1186198984| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse55 (select |v_#memory_$Pointer$.base_1517_const_-42853452| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse58 (select |v_#memory_$Pointer$.base_1507_const_-42853481| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse22 (select |v_#memory_$Pointer$.offset_1519_const_-574584716| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse14 (select |v_#memory_$Pointer$.offset_1518_const_-574584715| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse21 (select |v_#memory_$Pointer$.offset_1521_const_-574584819| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse45 (select |v_#memory_$Pointer$.offset_1533_const_-574584788| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse15 (+ v_CdAudioHitachiDeviceControl_~Irp.offset_20_const_673585352 120)) (.cse26 (select |v_#memory_$Pointer$.base_1536_const_-42853525| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse48 (select |v_#memory_int_1176_const_1186198582| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse19 (select |v_#memory_int_1175_const_1186198583| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse61 (select |v_#memory_$Pointer$.offset_1523_const_-574584817| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse60 (select |v_#memory_$Pointer$.offset_1522_const_-574584820| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse35 (+ v_CdAudioHitachiDeviceControl_~Irp.offset_20_const_673585352 201)) (.cse62 (select |v_#memory_int_1163_const_1186198548| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse43 (select |v_#memory_int_1165_const_1186198550| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse66 (select |v_#memory_int_1164_const_1186198551| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse63 (select |v_#memory_int_1162_const_1186198549| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse0 (select |v_#memory_int_1161_const_1186198538| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse36 (select |v_#memory_int_1153_const_1186198647| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse25 (+ v_CdAudioHitachiDeviceControl_~Irp.offset_20_const_673585352 180)) (.cse9 (select |v_#memory_int_1151_const_1186198645| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse10 (+ v_CdAudioHitachiDeviceControl_~Irp.offset_20_const_673585352 20)) (.cse13 (select |v_#memory_int_1178_const_1186198576| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse47 (select |v_#memory_int_1177_const_1186198577| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse59 (select |v_#memory_$Pointer$.base_1506_const_-42853484| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse50 (select |v_#memory_$Pointer$.base_1505_const_-42853483| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse32 (+ v_CdAudioHitachiDeviceControl_~Irp.offset_20_const_673585352 202)) (.cse27 (select |v_#memory_$Pointer$.base_1535_const_-42853528| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse64 (select |v_#memory_$Pointer$.base_1534_const_-42853527| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse41 (+ v_CdAudioHitachiDeviceControl_~Irp.offset_20_const_673585352 118)) (.cse65 (select |v_#memory_$Pointer$.base_1533_const_-42853522| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse42 (+ v_CdAudioHitachiDeviceControl_~Irp.offset_20_const_673585352 128)) (.cse29 (+ v_CdAudioHitachiDeviceControl_~Irp.offset_20_const_673585352 136)) (.cse52 (+ v_CdAudioHitachiDeviceControl_~Irp.offset_20_const_673585352 144)) (.cse12 (+ v_CdAudioHitachiDeviceControl_~Irp.offset_20_const_673585352 152)) (.cse53 (+ v_CdAudioHitachiDeviceControl_~Irp.offset_20_const_673585352 160)) (.cse1 (+ v_CdAudioHitachiDeviceControl_~Irp.offset_20_const_673585352 168)) (.cse38 (+ v_CdAudioHitachiDeviceControl_~Irp.offset_20_const_673585352 176)) (.cse20 (+ v_CdAudioHitachiDeviceControl_~Irp.offset_20_const_673585352 184)) (.cse7 (+ v_CdAudioHitachiDeviceControl_~Irp.offset_20_const_673585352 192)) (.cse56 (select |v_#memory_$Pointer$.base_1523_const_-42853559| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130)) (.cse34 (+ v_CdAudioHitachiDeviceControl_~Irp.offset_20_const_673585352 200))) (and (= (store |v_#memory_int_1161_const_1186198538| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store .cse0 .cse1 (select .cse2 .cse1))) |v_#memory_int_1160_const_1186198539|) (= |v_#memory_$Pointer$.base_1519_const_-42853450| (store |v_#memory_$Pointer$.base_1521_const_-42853553| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store .cse3 .cse4 (select .cse5 .cse4)))) (= (store |v_#memory_int_1174_const_1186198580| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store .cse6 .cse7 (select .cse8 .cse7))) |v_#memory_int_1173_const_1186198581|) (= |v_#memory_int_1150_const_1186198634| (store |v_#memory_int_1151_const_1186198645| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store .cse9 .cse10 |v_CdAudioHitachiDeviceControl_#t~union780_2_const_-1566705455|))) (= (store |v_#memory_int_1179_const_1186198579| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store .cse11 .cse12 (select .cse13 .cse12))) |v_#memory_int_1178_const_1186198576|) (= |v_#memory_$Pointer$.offset_1517_const_-574584726| (store |v_#memory_$Pointer$.offset_1518_const_-574584715| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store .cse14 .cse15 (select .cse16 .cse15)))) (= (store |v_#memory_int_1158_const_1186198642| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store .cse17 .cse7 (select .cse18 .cse7))) |v_#memory_int_1157_const_1186198643|) (= (store |v_#memory_int_1175_const_1186198583| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store .cse19 .cse20 (select .cse6 .cse20))) |v_#memory_int_1174_const_1186198580|) (= |v_#memory_$Pointer$.offset_1519_const_-574584716| (store |v_#memory_$Pointer$.offset_1521_const_-574584819| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store .cse21 .cse4 (select .cse22 .cse4)))) (= v_CdAudioHitachiDeviceControl_~cdaudioDataOut~3.offset_10_const_143392562 (select .cse23 .cse10)) (= (store |v_#memory_$Pointer$.offset_1505_const_-574584757| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store (store .cse24 .cse4 |v_CdAudioHitachiDeviceControl_#t~union775.offset_2_const_707431692|) .cse25 (select .cse23 .cse25))) |v_#memory_$Pointer$.offset_1503_const_-574584759|) (= |v_#memory_$Pointer$.base_1535_const_-42853528| (store |v_#memory_$Pointer$.base_1536_const_-42853525| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store .cse26 .cse4 (select .cse27 .cse4)))) (= (store |v_#memory_int_1181_const_1186198984| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store .cse28 .cse29 (select .cse30 .cse29))) |v_#memory_int_1180_const_1186198985|) (= (store |v_#memory_$Pointer$.offset_1506_const_-574584758| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store .cse31 .cse32 (select .cse24 .cse32))) |v_#memory_$Pointer$.offset_1505_const_-574584757|) (not (select |v_#valid_76_const_-1605542317| |v_CdAudioHitachiDeviceControl_~#srb~5.base_16_const_1039272055|)) (= v_CdAudioHitachiDeviceControl_~deviceExtension~10.offset_18_const_-1804285158 (select (select |v_#memory_$Pointer$.offset_1503_const_-574584759| v_CdAudioHitachiDeviceControl_~DeviceObject.base_8_const_-1187297464) .cse33)) (= (store |v_#memory_int_1157_const_1186198643| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store (store (store (store .cse18 .cse34 |v_CdAudioHitachiDeviceControl_#t~union774.ApcStateIndex_2_const_-1864459867|) .cse35 |v_CdAudioHitachiDeviceControl_#t~union774.ApcMode_2_const_299751043|) .cse32 |v_CdAudioHitachiDeviceControl_#t~union774.Inserted_2_const_489070150|) .cse4 (select .cse36 .cse4))) |v_#memory_int_1153_const_1186198647|) (= |v_#memory_$Pointer$.offset_1506_const_-574584758| (store |v_#memory_$Pointer$.offset_1507_const_-574584747| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store .cse37 .cse35 (select .cse31 .cse35)))) (= (select (select |v_#memory_$Pointer$.base_1503_const_-42853493| v_CdAudioHitachiDeviceControl_~DeviceObject.base_8_const_-1187297464) .cse33) v_CdAudioHitachiDeviceControl_~deviceExtension~10.base_18_const_1540097432) (= v_CdAudioHitachiDeviceControl_~DeviceObject.base_8_const_-1187297464 |v_CdAudioHitachiDeviceControl_#in~DeviceObject.base_1_const_401750923|) (= |v_CdAudioHitachiDeviceControl_~#srb~5.offset_16_const_-2062345543| 0) (= (store |v_#memory_int_1160_const_1186198539| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store .cse2 .cse38 (select .cse39 .cse38))) |v_#memory_int_1159_const_1186198653|) (= (store |v_#memory_int_1169_const_1186198546| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store (store (store (store .cse40 .cse4 |v_CdAudioHitachiDeviceControl_#t~union774.Type_2_const_765396452|) .cse41 |v_CdAudioHitachiDeviceControl_#t~union774.Size_2_const_722291453|) .cse15 |v_CdAudioHitachiDeviceControl_#t~union774.Spare0_2_const_-509007835|) .cse42 (select .cse43 .cse42))) |v_#memory_int_1165_const_1186198550|) (= |v_#memory_$Pointer$.offset_1533_const_-574584788| (store |v_#memory_$Pointer$.offset_1534_const_-574584785| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store .cse44 .cse15 (select .cse45 .cse15)))) (= (store |v_#memory_$Pointer$.base_1503_const_-42853493| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store .cse46 .cse10 (select (select |v_#memory_$Pointer$.base_1501_const_-42853495| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130) .cse10))) |v_#memory_$Pointer$.base_1501_const_-42853495|) (= (store |v_#memory_int_1159_const_1186198653| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store .cse39 .cse20 (select .cse17 .cse20))) |v_#memory_int_1158_const_1186198642|) (< |v_CdAudioHitachiDeviceControl_~#srb~5.base_16_const_1039272055| |v_#StackHeapBarrier_5_const_531197052|) (= |v_#memory_int_1169_const_1186198546| (store |v_#memory_int_1173_const_1186198581| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store (store (store (store .cse8 .cse34 |v_CdAudioHitachiDeviceControl_#t~union772.ApcStateIndex_2_const_-276114009|) .cse35 |v_CdAudioHitachiDeviceControl_#t~union772.ApcMode_2_const_-401441787|) .cse32 |v_CdAudioHitachiDeviceControl_#t~union772.Inserted_2_const_231024900|) .cse4 (select .cse40 .cse4)))) (= v_CdAudioHitachiDeviceControl_~Irp.offset_20_const_673585352 |v_CdAudioHitachiDeviceControl_#in~Irp.offset_1_const_1942582475|) (= (store |v_#memory_int_1177_const_1186198577| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store .cse47 .cse1 (select .cse48 .cse1))) |v_#memory_int_1176_const_1186198582|) (= (select .cse49 .cse25) v_CdAudioHitachiDeviceControl_~currentIrpStack~3.offset_14_const_2052058715) (= v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 |v_CdAudioHitachiDeviceControl_#in~Irp.base_1_const_-1808968115|) (= (store |v_#valid_76_const_-1605542317| |v_CdAudioHitachiDeviceControl_~#srb~5.base_16_const_1039272055| true) |v_#valid_75_const_-1605542316|) (= |v_#memory_$Pointer$.base_1503_const_-42853493| (store |v_#memory_$Pointer$.base_1505_const_-42853483| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store (store .cse50 .cse4 |v_CdAudioHitachiDeviceControl_#t~union775.base_2_const_-1408018674|) .cse25 (select .cse46 .cse25)))) (= v_CdAudioHitachiDeviceControl_~cdb~5.offset_7_const_253752466 (+ |v_CdAudioHitachiDeviceControl_~#srb~5.offset_16_const_-2062345543| 41)) (= v_CdAudioHitachiDeviceControl_~cdb~5.base_7_const_1371397460 |v_CdAudioHitachiDeviceControl_~#srb~5.base_16_const_1039272055|) (= |v_#memory_$Pointer$.base_1521_const_-42853553| (store |v_#memory_$Pointer$.base_1522_const_-42853554| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store .cse51 .cse32 (select .cse3 .cse32)))) (= (store |v_#memory_$Pointer$.offset_1517_const_-574584726| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store (store (store (store (store (store (store (store (store (store .cse16 .cse42 |v_CdAudioHitachiDeviceControl_#t~union774.Thread.offset_2_const_-157300445|) .cse29 |v_CdAudioHitachiDeviceControl_#t~union774.ApcListEntry.Flink.offset_2_const_309159339|) .cse52 |v_CdAudioHitachiDeviceControl_#t~union774.ApcListEntry.Blink.offset_2_const_-1963701209|) .cse12 |v_CdAudioHitachiDeviceControl_#t~union774.KernelRoutine.offset_2_const_-1289389500|) .cse53 |v_CdAudioHitachiDeviceControl_#t~union774.RundownRoutine.offset_2_const_640721136|) .cse1 |v_CdAudioHitachiDeviceControl_#t~union774.NormalRoutine.offset_2_const_-457417222|) .cse38 |v_CdAudioHitachiDeviceControl_#t~union774.NormalContext.offset_2_const_-2103977371|) .cse20 |v_CdAudioHitachiDeviceControl_#t~union774.SystemArgument1.offset_2_const_810108450|) .cse7 |v_CdAudioHitachiDeviceControl_#t~union774.SystemArgument2.offset_2_const_613471427|) .cse34 (select .cse37 .cse34))) |v_#memory_$Pointer$.offset_1507_const_-574584747|) (= (select .cse46 .cse10) v_CdAudioHitachiDeviceControl_~cdaudioDataOut~3.base_10_const_-115970640) (= |v_#memory_$Pointer$.offset_1501_const_-574584753| (store |v_#memory_$Pointer$.offset_1503_const_-574584759| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store .cse23 .cse10 (select (select |v_#memory_$Pointer$.offset_1501_const_-574584753| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130) .cse10)))) (= v_CdAudioHitachiDeviceControl_~DeviceObject.offset_8_const_-1919963834 |v_CdAudioHitachiDeviceControl_#in~DeviceObject.offset_1_const_558006921|) (= (store |v_#memory_$Pointer$.base_1518_const_-42853449| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store .cse54 .cse15 (select .cse55 .cse15))) |v_#memory_$Pointer$.base_1517_const_-42853452|) (= (store |v_#memory_$Pointer$.base_1523_const_-42853559| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store .cse56 .cse35 (select .cse51 .cse35))) |v_#memory_$Pointer$.base_1522_const_-42853554|) (= |v_#memory_$Pointer$.offset_1534_const_-574584785| (store |v_#memory_$Pointer$.offset_1535_const_-574584786| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store .cse57 .cse41 (select .cse44 .cse41)))) (= (store |v_#memory_$Pointer$.base_1519_const_-42853450| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store .cse5 .cse41 (select .cse54 .cse41))) |v_#memory_$Pointer$.base_1518_const_-42853449|) (= (store |v_#length_66_const_-660983928| |v_CdAudioHitachiDeviceControl_~#srb~5.base_16_const_1039272055| 57) |v_#length_65_const_-660983927|) (= |v_#memory_$Pointer$.offset_1535_const_-574584786| (store |v_#memory_$Pointer$.offset_1536_const_-574584791| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store .cse49 .cse4 (select .cse57 .cse4)))) (not (= 0 |v_CdAudioHitachiDeviceControl_~#srb~5.base_16_const_1039272055|)) (= |v_#memory_$Pointer$.base_1506_const_-42853484| (store |v_#memory_$Pointer$.base_1507_const_-42853481| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store .cse58 .cse35 (select .cse59 .cse35)))) (= (store |v_#memory_int_1180_const_1186198985| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store .cse30 .cse52 (select .cse11 .cse52))) |v_#memory_int_1179_const_1186198579|) (= (store |v_#memory_int_1185_const_1186198996| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store (store (store (store (select |v_#memory_int_1185_const_1186198996| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130) .cse4 |v_CdAudioHitachiDeviceControl_#t~union772.Type_2_const_1574625186|) .cse41 |v_CdAudioHitachiDeviceControl_#t~union772.Size_2_const_1531503803|) .cse15 |v_CdAudioHitachiDeviceControl_#t~union772.Spare0_2_const_-116110749|) .cse42 (select .cse28 .cse42))) |v_#memory_int_1181_const_1186198984|) (= |v_#memory_$Pointer$.base_1507_const_-42853481| (store |v_#memory_$Pointer$.base_1517_const_-42853452| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store (store (store (store (store (store (store (store (store (store .cse55 .cse42 |v_CdAudioHitachiDeviceControl_#t~union774.Thread.base_2_const_2108398821|) .cse29 |v_CdAudioHitachiDeviceControl_#t~union774.ApcListEntry.Flink.base_2_const_754695021|) .cse52 |v_CdAudioHitachiDeviceControl_#t~union774.ApcListEntry.Blink.base_2_const_238358761|) .cse12 |v_CdAudioHitachiDeviceControl_#t~union774.KernelRoutine.base_2_const_19935814|) .cse53 |v_CdAudioHitachiDeviceControl_#t~union774.RundownRoutine.base_2_const_57703410|) .cse1 |v_CdAudioHitachiDeviceControl_#t~union774.NormalRoutine.base_2_const_-372493444|) .cse38 |v_CdAudioHitachiDeviceControl_#t~union774.NormalContext.base_2_const_-2018896217|) .cse20 |v_CdAudioHitachiDeviceControl_#t~union774.SystemArgument1.base_2_const_-701772380|) .cse7 |v_CdAudioHitachiDeviceControl_#t~union774.SystemArgument2.base_2_const_1040900229|) .cse34 (select .cse58 .cse34)))) (= |v_#memory_$Pointer$.offset_1518_const_-574584715| (store |v_#memory_$Pointer$.offset_1519_const_-574584716| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store .cse22 .cse41 (select .cse14 .cse41)))) (= |v_#memory_$Pointer$.offset_1521_const_-574584819| (store |v_#memory_$Pointer$.offset_1522_const_-574584820| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store .cse60 .cse32 (select .cse21 .cse32)))) (= (store |v_#memory_$Pointer$.offset_1533_const_-574584788| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store (store (store (store (store (store (store (store (store (store .cse45 .cse42 |v_CdAudioHitachiDeviceControl_#t~union772.Thread.offset_2_const_1430914341|) .cse29 |v_CdAudioHitachiDeviceControl_#t~union772.ApcListEntry.Flink.offset_2_const_-1077039443|) .cse52 |v_CdAudioHitachiDeviceControl_#t~union772.ApcListEntry.Blink.offset_2_const_945067305|) .cse12 |v_CdAudioHitachiDeviceControl_#t~union772.KernelRoutine.offset_2_const_-1155508222|) .cse53 |v_CdAudioHitachiDeviceControl_#t~union772.RundownRoutine.offset_2_const_500185842|) .cse1 |v_CdAudioHitachiDeviceControl_#t~union772.NormalRoutine.offset_2_const_-323273800|) .cse38 |v_CdAudioHitachiDeviceControl_#t~union772.NormalContext.offset_2_const_-1970096093|) .cse20 |v_CdAudioHitachiDeviceControl_#t~union772.SystemArgument1.offset_2_const_747940960|) .cse7 |v_CdAudioHitachiDeviceControl_#t~union772.SystemArgument2.offset_2_const_551435009|) .cse34 (select .cse61 .cse34))) |v_#memory_$Pointer$.offset_1523_const_-574584817|) (= (store |v_#memory_int_1163_const_1186198548| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store .cse62 .cse12 (select .cse63 .cse12))) |v_#memory_int_1162_const_1186198549|) (= (store |v_#memory_$Pointer$.base_1534_const_-42853527| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store .cse64 .cse15 (select .cse65 .cse15))) |v_#memory_$Pointer$.base_1533_const_-42853522|) (= (select .cse26 .cse25) v_CdAudioHitachiDeviceControl_~currentIrpStack~3.base_14_const_2143130649) (= (store |v_#memory_int_1176_const_1186198582| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store .cse48 .cse38 (select .cse19 .cse38))) |v_#memory_int_1175_const_1186198583|) (= (store |v_#memory_$Pointer$.offset_1523_const_-574584817| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store .cse61 .cse35 (select .cse60 .cse35))) |v_#memory_$Pointer$.offset_1522_const_-574584820|) (= |v_#memory_int_1163_const_1186198548| (store |v_#memory_int_1164_const_1186198551| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store .cse66 .cse52 (select .cse62 .cse52)))) (= (store |v_#memory_int_1165_const_1186198550| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store .cse43 .cse29 (select .cse66 .cse29))) |v_#memory_int_1164_const_1186198551|) (= (store |v_#memory_int_1162_const_1186198549| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store .cse63 .cse53 (select .cse0 .cse53))) |v_#memory_int_1161_const_1186198538|) (= (store |v_#memory_int_1153_const_1186198647| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store (store .cse36 .cse25 |v_CdAudioHitachiDeviceControl_#t~union776_2_const_-1566730614|) .cse10 (select .cse9 .cse10))) |v_#memory_int_1151_const_1186198645|) (= (store |v_#memory_int_1178_const_1186198576| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store .cse13 .cse53 (select .cse47 .cse53))) |v_#memory_int_1177_const_1186198577|) (= (store |v_#memory_$Pointer$.base_1506_const_-42853484| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store .cse59 .cse32 (select .cse50 .cse32))) |v_#memory_$Pointer$.base_1505_const_-42853483|) (= (store |v_#memory_$Pointer$.base_1535_const_-42853528| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store .cse27 .cse41 (select .cse64 .cse41))) |v_#memory_$Pointer$.base_1534_const_-42853527|) (= |v_#memory_$Pointer$.base_1523_const_-42853559| (store |v_#memory_$Pointer$.base_1533_const_-42853522| v_CdAudioHitachiDeviceControl_~Irp.base_20_const_-1161099130 (store (store (store (store (store (store (store (store (store (store .cse65 .cse42 |v_CdAudioHitachiDeviceControl_#t~union772.Thread.base_2_const_-906841753|) .cse29 |v_CdAudioHitachiDeviceControl_#t~union772.ApcListEntry.Flink.base_2_const_-1168532241|) .cse52 |v_CdAudioHitachiDeviceControl_#t~union772.ApcListEntry.Blink.base_2_const_-1684999573|) .cse12 |v_CdAudioHitachiDeviceControl_#t~union772.KernelRoutine.base_2_const_-198924412|) .cse53 |v_CdAudioHitachiDeviceControl_#t~union772.RundownRoutine.base_2_const_1863265908|) .cse1 |v_CdAudioHitachiDeviceControl_#t~union772.NormalRoutine.base_2_const_-591353670|) .cse38 |v_CdAudioHitachiDeviceControl_#t~union772.NormalContext.base_2_const_2057210853|) .cse20 |v_CdAudioHitachiDeviceControl_#t~union772.SystemArgument1.base_2_const_-567891102|) .cse7 |v_CdAudioHitachiDeviceControl_#t~union772.SystemArgument2.base_2_const_1175060035|) .cse34 (select .cse56 .cse34)))))))
(check-sat)
(exit)