diskperf_false-unreach-call.i.cil.c_4.smt2 87.9 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
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
(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~DiskPerfSendToNextDriver.base| () Int)
(declare-fun |#funAddr~DiskPerfSendToNextDriver.offset| () Int)
(declare-fun |#funAddr~DiskPerfCreate.base| () Int)
(declare-fun |#funAddr~DiskPerfCreate.offset| () Int)
(declare-fun |#funAddr~DiskPerfReadWrite.base| () Int)
(declare-fun |#funAddr~DiskPerfReadWrite.offset| () Int)
(declare-fun |#funAddr~DiskPerfDeviceControl.base| () Int)
(declare-fun |#funAddr~DiskPerfDeviceControl.offset| () Int)
(declare-fun |#funAddr~DiskPerfWmi.base| () Int)
(declare-fun |#funAddr~DiskPerfWmi.offset| () Int)
(declare-fun |#funAddr~DiskPerfShutdownFlush.base| () Int)
(declare-fun |#funAddr~DiskPerfShutdownFlush.offset| () Int)
(declare-fun |#funAddr~DiskPerfDispatchPnp.base| () Int)
(declare-fun |#funAddr~DiskPerfDispatchPnp.offset| () Int)
(declare-fun |#funAddr~DiskPerfDispatchPower.base| () Int)
(declare-fun |#funAddr~DiskPerfDispatchPower.offset| () Int)
(declare-fun |#funAddr~DiskPerfAddDevice.base| () Int)
(declare-fun |#funAddr~DiskPerfAddDevice.offset| () Int)
(declare-fun |#funAddr~DiskPerfUnload.base| () Int)
(declare-fun |#funAddr~DiskPerfUnload.offset| () Int)
(declare-fun |#funAddr~DiskperfQueryWmiRegInfo.base| () Int)
(declare-fun |#funAddr~DiskperfQueryWmiRegInfo.offset| () Int)
(declare-fun |#funAddr~DiskperfQueryWmiDataBlock.base| () Int)
(declare-fun |#funAddr~DiskperfQueryWmiDataBlock.offset| () Int)
(declare-fun |#funAddr~DiskperfWmiFunctionControl.base| () Int)
(declare-fun |#funAddr~DiskperfWmiFunctionControl.offset| () Int)
(declare-fun |#funAddr~DiskPerfIrpCompletion.base| () Int)
(declare-fun |#funAddr~DiskPerfIrpCompletion.offset| () Int)
(declare-fun |#funAddr~DiskPerfIoCompletion.base| () Int)
(declare-fun |#funAddr~DiskPerfIoCompletion.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)
(declare-fun ~__anonenum_WMIENABLEDISABLECONTROL_131~0~WmiEventControl () Int)
(declare-fun ~__anonenum_WMIENABLEDISABLECONTROL_131~0~WmiDataBlockControl () Int)
(declare-fun ~__anonenum_SYSCTL_IRP_DISPOSITION_132~0~IrpProcessed () Int)
(declare-fun ~__anonenum_SYSCTL_IRP_DISPOSITION_132~0~IrpNotCompleted () Int)
(declare-fun ~__anonenum_SYSCTL_IRP_DISPOSITION_132~0~IrpNotWmi () Int)
(declare-fun ~__anonenum_SYSCTL_IRP_DISPOSITION_132~0~IrpForward () Int)
(assert (and (= |#funAddr~DiskPerfSendToNextDriver.base| (- 1)) (= |#funAddr~DiskPerfSendToNextDriver.offset| 0)))
(assert (and (= (- 1) |#funAddr~DiskPerfCreate.base|) (= |#funAddr~DiskPerfCreate.offset| 1)))
(assert (and (= 2 |#funAddr~DiskPerfReadWrite.offset|) (= (- 1) |#funAddr~DiskPerfReadWrite.base|)))
(assert (and (= 3 |#funAddr~DiskPerfDeviceControl.offset|) (= |#funAddr~DiskPerfDeviceControl.base| (- 1))))
(assert (and (= |#funAddr~DiskPerfWmi.offset| 4) (= |#funAddr~DiskPerfWmi.base| (- 1))))
(assert (and (= |#funAddr~DiskPerfShutdownFlush.offset| 5) (= (- 1) |#funAddr~DiskPerfShutdownFlush.base|)))
(assert (and (= (- 1) |#funAddr~DiskPerfDispatchPnp.base|) (= 6 |#funAddr~DiskPerfDispatchPnp.offset|)))
(assert (and (= 7 |#funAddr~DiskPerfDispatchPower.offset|) (= (- 1) |#funAddr~DiskPerfDispatchPower.base|)))
(assert (and (= |#funAddr~DiskPerfAddDevice.offset| 8) (= (- 1) |#funAddr~DiskPerfAddDevice.base|)))
(assert (and (= (- 1) |#funAddr~DiskPerfUnload.base|) (= 9 |#funAddr~DiskPerfUnload.offset|)))
(assert (and (= 10 |#funAddr~DiskperfQueryWmiRegInfo.offset|) (= (- 1) |#funAddr~DiskperfQueryWmiRegInfo.base|)))
(assert (and (= 11 |#funAddr~DiskperfQueryWmiDataBlock.offset|) (= |#funAddr~DiskperfQueryWmiDataBlock.base| (- 1))))
(assert (and (= (- 1) |#funAddr~DiskperfWmiFunctionControl.base|) (= |#funAddr~DiskperfWmiFunctionControl.offset| 12)))
(assert (and (= (- 1) |#funAddr~DiskPerfIrpCompletion.base|) (= |#funAddr~DiskPerfIrpCompletion.offset| 13)))
(assert (and (= 14 |#funAddr~DiskPerfIoCompletion.offset|) (= |#funAddr~DiskPerfIoCompletion.base| (- 1))))
(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))
(assert (= 0 ~__anonenum_WMIENABLEDISABLECONTROL_131~0~WmiEventControl))
(assert (= 1 ~__anonenum_WMIENABLEDISABLECONTROL_131~0~WmiDataBlockControl))
(assert (= 0 ~__anonenum_SYSCTL_IRP_DISPOSITION_132~0~IrpProcessed))
(assert (= ~__anonenum_SYSCTL_IRP_DISPOSITION_132~0~IrpNotCompleted 1))
(assert (= 2 ~__anonenum_SYSCTL_IRP_DISPOSITION_132~0~IrpNotWmi))
(assert (= 3 ~__anonenum_SYSCTL_IRP_DISPOSITION_132~0~IrpForward))
(declare-fun |v_#memory_$Pointer$.offset_525_const_-1833314314| () (Array Int (Array Int Int)))
(declare-fun v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 () Int)
(declare-fun v_DiskPerfReadWrite_~Irp.offset_3_const_-769278520 () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union127.Thread.offset_2_const_68309764| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union127.ApcListEntry.Flink.offset_2_const_939329036| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union127.ApcListEntry.Blink.offset_2_const_-1333400440| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union127.KernelRoutine.offset_2_const_-1042712317| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union127.RundownRoutine.offset_2_const_-302188079| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union127.NormalRoutine.offset_2_const_-210740039| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union127.NormalContext.offset_2_const_-1857300188| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union127.SystemArgument1.offset_2_const_1644171553| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union127.SystemArgument2.offset_2_const_1447796674| () Int)
(declare-fun |v_#memory_$Pointer$.offset_515_const_-1833314351| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_526_const_-1833314319| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_527_const_-1833314320| () (Array Int (Array Int Int)))
(declare-fun v_DiskPerfReadWrite_~partitionCounters~0.base_1_const_-263982952 () Int)
(declare-fun v_DiskPerfReadWrite_~DeviceObject.offset_2_const_-436229975 () Int)
(declare-fun |v_DiskPerfReadWrite_#in~DeviceObject.offset_1_const_-1257417140| () Int)
(declare-fun v_DiskPerfReadWrite_~DeviceObject.base_2_const_-493017621 () Int)
(declare-fun |v_DiskPerfReadWrite_#in~DeviceObject.base_1_const_-847076338| () Int)
(declare-fun |v_#memory_int_504_const_-328415680| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_505_const_-328415677| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_527_const_-344038154| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_528_const_-344038159| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_517_const_-328415646| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_518_const_-328415635| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_490_const_-328414446| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_491_const_-328414435| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_506_const_-328415678| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_507_const_-328415667| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_471_const_-328414369| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_472_const_-328414370| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_514_const_-344038188| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_515_const_-344038185| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_485_const_-328414344| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_486_const_-328414341| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_478_const_-344036917| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_480_const_-344036896| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_495_const_-1833314162| () (Array Int (Array Int Int)))
(declare-fun v_DiskPerfReadWrite_~nextIrpStack~0.offset_1_const_-1978008837 () Int)
(declare-fun |v_#memory_int_501_const_-328415673| () (Array Int (Array Int Int)))
(declare-fun |v_DiskPerfReadWrite_#t~union129.ApcStateIndex_2_const_1067886468| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union129.ApcMode_2_const_1067788322| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union129.Inserted_2_const_-1471350585| () Int)
(declare-fun |v_#memory_int_497_const_-328414437| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_473_const_-328414375| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_474_const_-328414376| () (Array Int (Array Int Int)))
(declare-fun v_DiskPerfReadWrite_~partitionCounters~0.offset_1_const_617476182 () Int)
(declare-fun |v_#memory_int_508_const_-328415668| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_493_const_-344036990| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_494_const_-344036979| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_492_const_-1833314163| () (Array Int (Array Int Int)))
(declare-fun |v_DiskPerfReadWrite_#t~union133.Thread.offset_2_const_-2047039191| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union133.ApcListEntry.Flink.offset_2_const_-1821889391| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union133.ApcListEntry.Blink.offset_2_const_200479533| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union133.KernelRoutine.offset_2_const_1443063710| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union133.RundownRoutine.offset_2_const_-552133898| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union133.NormalRoutine.offset_2_const_-2019931340| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union133.NormalContext.offset_2_const_628475839| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union133.SystemArgument1.offset_2_const_-1813132036| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union133.SystemArgument2.offset_2_const_-2009637987| () Int)
(declare-fun |v_#memory_$Pointer$.offset_482_const_-1833314068| () (Array Int (Array Int Int)))
(declare-fun v_DiskPerfReadWrite_~tmp~5_1_const_-2141630104 () Int)
(declare-fun |v_#memory_$Pointer$.base_513_const_-344038187| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_484_const_-328414343| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_476_const_-1833314101| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_477_const_-1833314102| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_519_const_-328415636| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_492_const_-328414436| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_489_const_-328414460| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_469_const_-328414394| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_470_const_-328414372| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_523_const_-328415737| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_524_const_-328415738| () (Array Int (Array Int Int)))
(declare-fun v_DiskPerfReadWrite_~deviceExtension~6.base_2_const_763185029 () Int)
(declare-fun |v_#memory_$Pointer$.base_476_const_-344036919| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_477_const_-344036920| () (Array Int (Array Int Int)))
(declare-fun |v_DiskPerfReadWrite_#in~Irp.offset_1_const_1313573352| () Int)
(declare-fun |v_#memory_$Pointer$.offset_509_const_-1833314756| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_510_const_-1833314358| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_513_const_-1833314345| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_514_const_-1833314346| () (Array Int (Array Int Int)))
(declare-fun v_DiskPerfReadWrite_~processor~0_1_const_-334370990 () Int)
(declare-fun |v_#memory_$Pointer$.offset_465_const_-1833313493| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_466_const_-1833313494| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_525_const_-344038156| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_526_const_-344038153| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_480_const_-328414339| () (Array Int (Array Int Int)))
(declare-fun |v_DiskPerfReadWrite_#t~union135.Type_2_const_-849752736| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union135.Size_2_const_-892988807| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union135.Spare0_2_const_2107097249| () Int)
(declare-fun |v_#memory_int_476_const_-328414374| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_487_const_-328414342| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_488_const_-328414459| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_528_const_-1833314317| () (Array Int (Array Int Int)))
(declare-fun v_DiskPerfReadWrite_~deviceExtension~6.offset_2_const_-112264253 () Int)
(declare-fun |v_#memory_int_464_const_-328414277| () (Array Int (Array Int Int)))
(declare-fun |v_DiskPerfReadWrite_#t~union137_2_const_-1670868594| () Int)
(declare-fun |v_#memory_int_463_const_-328414280| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_492_const_-344036989| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_462_const_-1833313490| () (Array Int (Array Int Int)))
(declare-fun |v_DiskPerfReadWrite_#t~mem138.offset_1_const_-1670633659| () Int)
(declare-fun |v_#memory_$Pointer$.base_495_const_-344036980| () (Array Int (Array Int Int)))
(declare-fun v_DiskPerfReadWrite_~nextIrpStack~0.base_1_const_1739886717 () Int)
(declare-fun |v_#memory_int_521_const_-328415739| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_522_const_-328415740| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_462_const_-344037332| () (Array Int (Array Int Int)))
(declare-fun |v_DiskPerfReadWrite_#t~mem138.base_1_const_1016323911| () Int)
(declare-fun |v_#memory_$Pointer$.offset_493_const_-1833314164| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_494_const_-1833314161| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_481_const_-1833314067| () (Array Int (Array Int Int)))
(declare-fun v_DiskPerfReadWrite_~currentIrpStack~0.base_1_const_783712881 () Int)
(declare-fun |v_#memory_int_502_const_-328415674| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_481_const_-344036893| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_482_const_-344036894| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_465_const_-344037335| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_466_const_-344037336| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_509_const_-344037582| () (Array Int (Array Int Int)))
(declare-fun |v_DiskPerfReadWrite_#t~union129.Thread.base_2_const_-2031704444| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union129.ApcListEntry.Flink.base_2_const_-1527009652| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union129.ApcListEntry.Blink.base_2_const_-2043345912| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union129.KernelRoutine.base_2_const_1825775495| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union129.RundownRoutine.base_2_const_200013457| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union129.NormalRoutine.base_2_const_1433198781| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union129.NormalContext.base_2_const_-213203992| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union129.SystemArgument1.base_2_const_-589238619| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union129.SystemArgument2.base_2_const_1153565062| () Int)
(declare-fun |v_#memory_$Pointer$.base_499_const_-344036984| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_478_const_-1833314091| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_480_const_-1833314078| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_497_const_-344036978| () (Array Int (Array Int Int)))
(declare-fun |v_DiskPerfReadWrite_#t~union130.base_2_const_-595268668| () Int)
(declare-fun |v_DiskPerfReadWrite_#in~Irp.base_1_const_-562692438| () Int)
(declare-fun |v_#memory_int_468_const_-328414393| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_510_const_-344038200| () (Array Int (Array Int Int)))
(declare-fun |v_DiskPerfReadWrite_#t~union133.ApcStateIndex_2_const_541030827| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union133.ApcMode_2_const_-906448119| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union133.Inserted_2_const_1755714176| () Int)
(declare-fun |v_#memory_int_503_const_-328415679| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_464_const_-344037330| () (Array Int (Array Int Int)))
(declare-fun |v_DiskPerfReadWrite_#t~union135.Thread.offset_2_const_659582247| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union135.ApcListEntry.Flink.offset_2_const_-435559505| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union135.ApcListEntry.Blink.offset_2_const_1586547243| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union135.KernelRoutine.offset_2_const_1308920256| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union135.RundownRoutine.offset_2_const_-411598604| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union135.NormalRoutine.offset_2_const_2141154678| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union135.NormalContext.offset_2_const_494332385| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union135.SystemArgument1.offset_2_const_-1751226690| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union135.SystemArgument2.offset_2_const_-1947601569| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union133.Thread.base_2_const_1297352299| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union133.ApcListEntry.Flink.base_2_const_1038371795| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union133.ApcListEntry.Blink.base_2_const_522166639| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union133.KernelRoutine.base_2_const_-1881135616| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union133.RundownRoutine.base_2_const_1254358904| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union133.NormalRoutine.base_2_const_2021402422| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union133.NormalContext.base_2_const_374999649| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union133.SystemArgument1.base_2_const_2030697214| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union133.SystemArgument2.base_2_const_-521466401| () Int)
(declare-fun |v_#memory_$Pointer$.offset_497_const_-1833314168| () (Array Int (Array Int Int)))
(declare-fun |v_DiskPerfReadWrite_#t~union130.offset_2_const_207653954| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union131_2_const_-1670879116| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union133.Type_2_const_-40409282| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union133.Size_2_const_-83514313| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union133.Spare0_2_const_-1794972929| () Int)
(declare-fun |v_#memory_int_520_const_-328415622| () (Array Int (Array Int Int)))
(declare-fun v_DiskPerfReadWrite_~currentIrpStack~0.offset_1_const_-1731281009 () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union136.base_2_const_1271668362| () Int)
(declare-fun |v_#memory_$Pointer$.offset_498_const_-1833314165| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_464_const_-1833313496| () (Array Int (Array Int Int)))
(declare-fun |v_DiskPerfReadWrite_#t~union136.offset_2_const_-971299448| () Int)
(declare-fun |v_#memory_$Pointer$.base_498_const_-344036983| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_509_const_-328415665| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_int_525_const_-328415743| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_511_const_-1833314347| () (Array Int (Array Int Int)))
(declare-fun |v_DiskPerfReadWrite_#t~union127.ApcStateIndex_2_const_-1638734970| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union127.ApcMode_2_const_366726564| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union127.Inserted_2_const_-1729395835| () Int)
(declare-fun |v_#memory_int_513_const_-328415642| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.base_511_const_-344038197| () (Array Int (Array Int Int)))
(declare-fun |v_#memory_$Pointer$.offset_499_const_-1833314166| () (Array Int (Array Int Int)))
(declare-fun |v_DiskPerfReadWrite_#t~union135.ApcStateIndex_2_const_-1047315031| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union135.ApcMode_2_const_-205386361| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union135.Inserted_2_const_2014005186| () Int)
(declare-fun |v_#memory_int_475_const_-328414373| () (Array Int (Array Int Int)))
(declare-fun |v_DiskPerfReadWrite_#t~union129.Type_2_const_-661124891| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union129.Size_2_const_-704229890| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union129.Spare0_2_const_-1177096474| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union129.Thread.offset_2_const_-1520036094| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union129.ApcListEntry.Flink.offset_2_const_-1969554166| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union129.ApcListEntry.Blink.offset_2_const_52798342| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union129.KernelRoutine.offset_2_const_-1176855739| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union129.RundownRoutine.offset_2_const_-161505297| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union129.NormalRoutine.offset_2_const_-344621317| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union129.NormalContext.offset_2_const_-1991443610| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union129.SystemArgument1.offset_2_const_1706207971| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union129.SystemArgument2.offset_2_const_1509702020| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union127.Thread.base_2_const_-751699194| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union127.ApcListEntry.Flink.base_2_const_844730382| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union127.ApcListEntry.Blink.base_2_const_328263050| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union127.KernelRoutine.base_2_const_1606915269| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union127.RundownRoutine.base_2_const_2005313811| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union127.NormalRoutine.base_2_const_1214486011| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union127.NormalContext.base_2_const_-431916762| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union127.SystemArgument1.base_2_const_-455095197| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union127.SystemArgument2.base_2_const_1287724868| () Int)
(declare-fun |v_#memory_int_529_const_-328415731| () (Array Int (Array Int Int)))
(declare-fun |v_DiskPerfReadWrite_#t~union127.Type_2_const_148349603| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union127.Size_2_const_105244604| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union127.Spare0_2_const_-784068316| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union135.Thread.base_2_const_17494505| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union135.ApcListEntry.Flink.base_2_const_-1333368239| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union135.ApcListEntry.Blink.base_2_const_-1849557011| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union135.KernelRoutine.base_2_const_-1662144318| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union135.RundownRoutine.base_2_const_-551088906| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union135.NormalRoutine.base_2_const_-2054573576| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union135.NormalContext.base_2_const_593990947| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union135.SystemArgument1.base_2_const_1896684832| () Int)
(declare-fun |v_DiskPerfReadWrite_#t~union135.SystemArgument2.base_2_const_-655609855| () Int)
(assert (let ((.cse104 (select |v_#memory_$Pointer$.offset_495_const_-1833314162| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse111 (select |v_#memory_$Pointer$.base_495_const_-344036980| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse74 (+ v_DiskPerfReadWrite_~Irp.offset_3_const_-769278520 180))) (let ((.cse24 (select |v_#memory_int_507_const_-328415667| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse40 (select |v_#memory_int_473_const_-328414375| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse26 (select |v_#memory_int_472_const_-328414370| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse30 (select |v_#memory_$Pointer$.base_514_const_-344038188| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse32 (select |v_#memory_int_485_const_-328414344| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse9 (select |v_#memory_int_518_const_-328415635| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse22 (select |v_#memory_int_491_const_-328414435| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse23 (select |v_#memory_int_490_const_-328414446| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse34 (select |v_#memory_$Pointer$.base_478_const_-344036917| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse59 (select |v_#memory_$Pointer$.base_477_const_-344036920| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse58 (+ v_DiskPerfReadWrite_~DeviceObject.offset_2_const_-436229975 76)) (.cse43 (select |v_#memory_$Pointer$.base_493_const_-344036990| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse8 (select |v_#memory_$Pointer$.base_527_const_-344038154| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse67 (select |v_#memory_$Pointer$.base_526_const_-344038153| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse27 (select |v_#memory_int_471_const_-328414369| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse54 (select |v_#memory_int_470_const_-328414372| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse72 (select |v_#memory_int_487_const_-328414342| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse31 (select |v_#memory_int_486_const_-328414341| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse76 (+ v_DiskPerfReadWrite_~deviceExtension~6.offset_2_const_-112264253 56)) (.cse45 (select |v_#memory_$Pointer$.offset_482_const_-1833314068| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse6 (select |v_#memory_$Pointer$.base_528_const_-344038159| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse81 (select |v_#memory_$Pointer$.offset_493_const_-1833314164| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse44 (select |v_#memory_$Pointer$.offset_492_const_-1833314163| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse36 (select |v_#memory_int_501_const_-328415673| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse53 (select |v_#memory_int_489_const_-328414460| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse71 (select |v_#memory_int_488_const_-328414459| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse77 (select .cse111 .cse74)) (.cse0 (select |v_#memory_$Pointer$.offset_527_const_-1833314320| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse55 (select |v_#memory_int_469_const_-328414394| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse88 (select |v_#memory_$Pointer$.base_509_const_-344037582| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse47 (select |v_#memory_int_484_const_-328414343| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse69 (select |v_#memory_int_480_const_-328414339| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse5 (select |v_#memory_int_504_const_-328415680| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse87 (select |v_#memory_$Pointer$.base_465_const_-344037335| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse50 (select |v_#memory_$Pointer$.offset_476_const_-1833314101| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse65 (select |v_#memory_$Pointer$.offset_466_const_-1833313494| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse57 (select |v_#memory_int_523_const_-328415737| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse78 (select |v_#memory_int_522_const_-328415740| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse75 (select |v_#memory_$Pointer$.base_492_const_-344036989| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse84 (select |v_#memory_$Pointer$.base_482_const_-344036894| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse35 (select .cse104 .cse74)) (.cse38 (select |v_#memory_int_497_const_-328414437| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse52 (select |v_#memory_int_492_const_-328414436| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse25 (select |v_#memory_int_506_const_-328415678| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse3 (select |v_#memory_int_505_const_-328415677| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse51 (select |v_#memory_int_519_const_-328415636| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse93 (select |v_#memory_$Pointer$.offset_528_const_-1833314317| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse97 (select |v_#memory_$Pointer$.base_464_const_-344037330| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse98 (select |v_#memory_$Pointer$.offset_497_const_-1833314168| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse89 (select |v_#memory_$Pointer$.base_499_const_-344036984| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse41 (select |v_#memory_int_508_const_-328415668| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse2 (select |v_#memory_$Pointer$.offset_526_const_-1833314319| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse12 (select |v_#memory_$Pointer$.offset_525_const_-1833314314| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse80 (select |v_#memory_$Pointer$.offset_494_const_-1833314161| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse102 (select |v_#memory_$Pointer$.base_498_const_-344036983| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse92 (select |v_#memory_$Pointer$.base_497_const_-344036978| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse56 (select |v_#memory_int_524_const_-328415738| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse61 (select |v_#memory_$Pointer$.offset_510_const_-1833314358| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse66 (select |v_#memory_$Pointer$.offset_465_const_-1833313493| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse101 (select |v_#memory_$Pointer$.offset_464_const_-1833313496| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse96 (select |v_#memory_int_503_const_-328415679| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse83 (select |v_#memory_int_502_const_-328415674| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse11 (select |v_#memory_int_517_const_-328415646| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse95 (select |v_#memory_$Pointer$.base_510_const_-344038200| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse100 (select |v_#memory_$Pointer$.offset_498_const_-1833314165| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse94 (select |v_#memory_int_468_const_-328414393| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse73 (select |v_#memory_int_464_const_-328414277| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse70 (select |v_#memory_int_476_const_-328414374| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse85 (select |v_#memory_$Pointer$.base_481_const_-344036893| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse33 (select |v_#memory_$Pointer$.base_480_const_-344036896| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse46 (select |v_#memory_$Pointer$.base_513_const_-344038187| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse108 (select |v_#memory_$Pointer$.base_511_const_-344038197| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse107 (select |v_#memory_int_513_const_-328415642| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse103 (select |v_#memory_int_509_const_-328415665| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse64 (select |v_#memory_$Pointer$.offset_513_const_-1833314345| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse106 (select |v_#memory_$Pointer$.offset_511_const_-1833314347| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse21 (select |v_#memory_$Pointer$.offset_515_const_-1833314351| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse63 (select |v_#memory_$Pointer$.offset_514_const_-1833314346| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse29 (+ v_DiskPerfReadWrite_~Irp.offset_3_const_-769278520 201)) (.cse79 (select |v_#memory_int_521_const_-328415739| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse99 (select |v_#memory_int_520_const_-328415622| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse62 (select |v_#memory_$Pointer$.offset_509_const_-1833314756| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse109 (select |v_#memory_$Pointer$.offset_499_const_-1833314166| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse68 (select |v_#memory_$Pointer$.base_525_const_-344038156| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse28 (select |v_#memory_$Pointer$.base_515_const_-344038185| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse49 (+ v_DiskPerfReadWrite_~Irp.offset_3_const_-769278520 120)) (.cse105 (select |v_#memory_int_525_const_-328415743| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse82 (select |v_#memory_$Pointer$.offset_481_const_-1833314067| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse90 (select |v_#memory_$Pointer$.offset_480_const_-1833314078| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse37 (+ v_DiskPerfReadWrite_~Irp.offset_3_const_-769278520 202)) (.cse91 (select |v_#memory_$Pointer$.offset_478_const_-1833314091| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse48 (select |v_#memory_$Pointer$.offset_477_const_-1833314102| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse1 (+ v_DiskPerfReadWrite_~Irp.offset_3_const_-769278520 118)) (.cse42 (select |v_#memory_$Pointer$.base_494_const_-344036979| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse7 (+ v_DiskPerfReadWrite_~Irp.offset_3_const_-769278520 116)) (.cse60 (select |v_#memory_$Pointer$.base_476_const_-344036919| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse13 (+ v_DiskPerfReadWrite_~Irp.offset_3_const_-769278520 128)) (.cse14 (+ v_DiskPerfReadWrite_~Irp.offset_3_const_-769278520 136)) (.cse16 (+ v_DiskPerfReadWrite_~Irp.offset_3_const_-769278520 152)) (.cse17 (+ v_DiskPerfReadWrite_~Irp.offset_3_const_-769278520 160)) (.cse4 (+ v_DiskPerfReadWrite_~Irp.offset_3_const_-769278520 168)) (.cse18 (+ v_DiskPerfReadWrite_~Irp.offset_3_const_-769278520 176)) (.cse19 (+ v_DiskPerfReadWrite_~Irp.offset_3_const_-769278520 184)) (.cse10 (+ v_DiskPerfReadWrite_~Irp.offset_3_const_-769278520 192)) (.cse86 (select |v_#memory_$Pointer$.base_466_const_-344037336| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse20 (+ v_DiskPerfReadWrite_~Irp.offset_3_const_-769278520 200)) (.cse110 (select |v_#memory_int_475_const_-328414373| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse39 (select |v_#memory_int_474_const_-328414376| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378)) (.cse15 (+ v_DiskPerfReadWrite_~Irp.offset_3_const_-769278520 144))) (and (= |v_#memory_$Pointer$.offset_526_const_-1833314319| (store |v_#memory_$Pointer$.offset_527_const_-1833314320| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse0 .cse1 (select .cse2 .cse1)))) (= v_DiskPerfReadWrite_~partitionCounters~0.base_1_const_-263982952 0) (= v_DiskPerfReadWrite_~DeviceObject.offset_2_const_-436229975 |v_DiskPerfReadWrite_#in~DeviceObject.offset_1_const_-1257417140|) (= v_DiskPerfReadWrite_~DeviceObject.base_2_const_-493017621 |v_DiskPerfReadWrite_#in~DeviceObject.base_1_const_-847076338|) (= (store |v_#memory_int_505_const_-328415677| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse3 .cse4 (select .cse5 .cse4))) |v_#memory_int_504_const_-328415680|) (= |v_#memory_$Pointer$.base_527_const_-344038154| (store |v_#memory_$Pointer$.base_528_const_-344038159| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse6 .cse7 (select .cse8 .cse7)))) (= (store |v_#memory_int_518_const_-328415635| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse9 .cse10 (select .cse11 .cse10))) |v_#memory_int_517_const_-328415646|) (= |v_#memory_$Pointer$.offset_515_const_-1833314351| (store |v_#memory_$Pointer$.offset_525_const_-1833314314| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store (store (store (store (store (store (store (store (store (store .cse12 .cse13 |v_DiskPerfReadWrite_#t~union127.Thread.offset_2_const_68309764|) .cse14 |v_DiskPerfReadWrite_#t~union127.ApcListEntry.Flink.offset_2_const_939329036|) .cse15 |v_DiskPerfReadWrite_#t~union127.ApcListEntry.Blink.offset_2_const_-1333400440|) .cse16 |v_DiskPerfReadWrite_#t~union127.KernelRoutine.offset_2_const_-1042712317|) .cse17 |v_DiskPerfReadWrite_#t~union127.RundownRoutine.offset_2_const_-302188079|) .cse4 |v_DiskPerfReadWrite_#t~union127.NormalRoutine.offset_2_const_-210740039|) .cse18 |v_DiskPerfReadWrite_#t~union127.NormalContext.offset_2_const_-1857300188|) .cse19 |v_DiskPerfReadWrite_#t~union127.SystemArgument1.offset_2_const_1644171553|) .cse10 |v_DiskPerfReadWrite_#t~union127.SystemArgument2.offset_2_const_1447796674|) .cse20 (select .cse21 .cse20)))) (= |v_#memory_int_490_const_-328414446| (store |v_#memory_int_491_const_-328414435| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse22 .cse15 (select .cse23 .cse15)))) (= (store |v_#memory_int_507_const_-328415667| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse24 .cse16 (select .cse25 .cse16))) |v_#memory_int_506_const_-328415678|) (= |v_#memory_int_471_const_-328414369| (store |v_#memory_int_472_const_-328414370| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse26 .cse4 (select .cse27 .cse4)))) (= |v_#memory_$Pointer$.base_514_const_-344038188| (store |v_#memory_$Pointer$.base_515_const_-344038185| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse28 .cse29 (select .cse30 .cse29)))) (= (store |v_#memory_int_486_const_-328414341| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse31 .cse19 (select .cse32 .cse19))) |v_#memory_int_485_const_-328414344|) (= |v_#memory_$Pointer$.base_478_const_-344036917| (store |v_#memory_$Pointer$.base_480_const_-344036896| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse33 .cse7 (select .cse34 .cse7)))) (= (+ v_DiskPerfReadWrite_~nextIrpStack~0.offset_1_const_-1978008837 68) .cse35) (= (store |v_#memory_int_501_const_-328415673| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store (store (store (store .cse36 .cse20 |v_DiskPerfReadWrite_#t~union129.ApcStateIndex_2_const_1067886468|) .cse29 |v_DiskPerfReadWrite_#t~union129.ApcMode_2_const_1067788322|) .cse37 |v_DiskPerfReadWrite_#t~union129.Inserted_2_const_-1471350585|) .cse7 (select .cse38 .cse7))) |v_#memory_int_497_const_-328414437|) (= (store |v_#memory_int_474_const_-328414376| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse39 .cse16 (select .cse40 .cse16))) |v_#memory_int_473_const_-328414375|) (= v_DiskPerfReadWrite_~partitionCounters~0.offset_1_const_617476182 0) (= (store |v_#memory_int_508_const_-328415668| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse41 .cse15 (select .cse24 .cse15))) |v_#memory_int_507_const_-328415667|) (= |v_#memory_int_472_const_-328414370| (store |v_#memory_int_473_const_-328414375| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse40 .cse17 (select .cse26 .cse17)))) (= (store |v_#memory_$Pointer$.base_494_const_-344036979| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse42 .cse1 (select .cse43 .cse1))) |v_#memory_$Pointer$.base_493_const_-344036990|) (= |v_#memory_$Pointer$.offset_482_const_-1833314068| (store |v_#memory_$Pointer$.offset_492_const_-1833314163| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store (store (store (store (store (store (store (store (store (store .cse44 .cse13 |v_DiskPerfReadWrite_#t~union133.Thread.offset_2_const_-2047039191|) .cse14 |v_DiskPerfReadWrite_#t~union133.ApcListEntry.Flink.offset_2_const_-1821889391|) .cse15 |v_DiskPerfReadWrite_#t~union133.ApcListEntry.Blink.offset_2_const_200479533|) .cse16 |v_DiskPerfReadWrite_#t~union133.KernelRoutine.offset_2_const_1443063710|) .cse17 |v_DiskPerfReadWrite_#t~union133.RundownRoutine.offset_2_const_-552133898|) .cse4 |v_DiskPerfReadWrite_#t~union133.NormalRoutine.offset_2_const_-2019931340|) .cse18 |v_DiskPerfReadWrite_#t~union133.NormalContext.offset_2_const_628475839|) .cse19 |v_DiskPerfReadWrite_#t~union133.SystemArgument1.offset_2_const_-1813132036|) .cse10 |v_DiskPerfReadWrite_#t~union133.SystemArgument2.offset_2_const_-2009637987|) .cse20 (select .cse45 .cse20)))) (= v_DiskPerfReadWrite_~tmp~5_1_const_-2141630104 0) (= (store |v_#memory_$Pointer$.base_514_const_-344038188| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse30 .cse37 (select .cse46 .cse37))) |v_#memory_$Pointer$.base_513_const_-344038187|) (= (store |v_#memory_int_485_const_-328414344| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse32 .cse10 (select .cse47 .cse10))) |v_#memory_int_484_const_-328414343|) (= |v_#memory_$Pointer$.offset_476_const_-1833314101| (store |v_#memory_$Pointer$.offset_477_const_-1833314102| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse48 .cse49 (select .cse50 .cse49)))) (= (store |v_#memory_int_519_const_-328415636| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse51 .cse19 (select .cse9 .cse19))) |v_#memory_int_518_const_-328415635|) (= |v_#memory_int_491_const_-328414435| (store |v_#memory_int_492_const_-328414436| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse52 .cse14 (select .cse22 .cse14)))) (= (store |v_#memory_int_490_const_-328414446| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse23 .cse16 (select .cse53 .cse16))) |v_#memory_int_489_const_-328414460|) (= |v_#memory_int_469_const_-328414394| (store |v_#memory_int_470_const_-328414372| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse54 .cse19 (select .cse55 .cse19)))) (= |v_#memory_int_523_const_-328415737| (store |v_#memory_int_524_const_-328415738| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse56 .cse15 (select .cse57 .cse15)))) (= (select (select |v_#memory_$Pointer$.base_528_const_-344038159| v_DiskPerfReadWrite_~DeviceObject.base_2_const_-493017621) .cse58) v_DiskPerfReadWrite_~deviceExtension~6.base_2_const_763185029) (= |v_#memory_$Pointer$.base_476_const_-344036919| (store |v_#memory_$Pointer$.base_477_const_-344036920| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse59 .cse49 (select .cse60 .cse49)))) (= v_DiskPerfReadWrite_~Irp.offset_3_const_-769278520 |v_DiskPerfReadWrite_#in~Irp.offset_1_const_1313573352|) (= |v_#memory_$Pointer$.offset_509_const_-1833314756| (store |v_#memory_$Pointer$.offset_510_const_-1833314358| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse61 .cse49 (select .cse62 .cse49)))) (= |v_#memory_$Pointer$.offset_513_const_-1833314345| (store |v_#memory_$Pointer$.offset_514_const_-1833314346| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse63 .cse37 (select .cse64 .cse37)))) (= v_DiskPerfReadWrite_~processor~0_1_const_-334370990 v_DiskPerfReadWrite_~tmp~5_1_const_-2141630104) (= |v_#memory_$Pointer$.offset_465_const_-1833313493| (store |v_#memory_$Pointer$.offset_466_const_-1833313494| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse65 .cse29 (select .cse66 .cse29)))) (= |v_#memory_$Pointer$.base_525_const_-344038156| (store |v_#memory_$Pointer$.base_526_const_-344038153| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse67 .cse49 (select .cse68 .cse49)))) (= |v_#memory_int_476_const_-328414374| (store |v_#memory_int_480_const_-328414339| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store (store (store (store .cse69 .cse7 |v_DiskPerfReadWrite_#t~union135.Type_2_const_-849752736|) .cse1 |v_DiskPerfReadWrite_#t~union135.Size_2_const_-892988807|) .cse49 |v_DiskPerfReadWrite_#t~union135.Spare0_2_const_2107097249|) .cse13 (select .cse70 .cse13)))) (= |v_#memory_int_487_const_-328414342| (store |v_#memory_int_488_const_-328414459| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse71 .cse4 (select .cse72 .cse4)))) (= |v_#memory_$Pointer$.base_477_const_-344036920| (store |v_#memory_$Pointer$.base_478_const_-344036917| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse34 .cse1 (select .cse59 .cse1)))) (= (select (select |v_#memory_$Pointer$.offset_528_const_-1833314317| v_DiskPerfReadWrite_~DeviceObject.base_2_const_-493017621) .cse58) v_DiskPerfReadWrite_~deviceExtension~6.offset_2_const_-112264253) (= |v_#memory_int_463_const_-328414280| (store |v_#memory_int_464_const_-328414277| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse73 .cse74 |v_DiskPerfReadWrite_#t~union137_2_const_-1670868594|))) (= |v_#memory_$Pointer$.base_492_const_-344036989| (store |v_#memory_$Pointer$.base_493_const_-344036990| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse43 .cse49 (select .cse75 .cse49)))) (= |v_DiskPerfReadWrite_#t~mem138.offset_1_const_-1670633659| (select (select |v_#memory_$Pointer$.offset_462_const_-1833313490| v_DiskPerfReadWrite_~deviceExtension~6.base_2_const_763185029) .cse76)) (= .cse77 v_DiskPerfReadWrite_~nextIrpStack~0.base_1_const_1739886717) (= (store |v_#memory_int_522_const_-328415740| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse78 .cse17 (select .cse79 .cse17))) |v_#memory_int_521_const_-328415739|) (= |v_#memory_$Pointer$.base_526_const_-344038153| (store |v_#memory_$Pointer$.base_527_const_-344038154| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse8 .cse1 (select .cse67 .cse1)))) (= (store |v_#memory_int_471_const_-328414369| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse27 .cse18 (select .cse54 .cse18))) |v_#memory_int_470_const_-328414372|) (= |v_#memory_int_486_const_-328414341| (store |v_#memory_int_487_const_-328414342| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse72 .cse18 (select .cse31 .cse18)))) (= (select (select |v_#memory_$Pointer$.base_462_const_-344037332| v_DiskPerfReadWrite_~deviceExtension~6.base_2_const_763185029) .cse76) |v_DiskPerfReadWrite_#t~mem138.base_1_const_1016323911|) (= |v_#memory_$Pointer$.offset_493_const_-1833314164| (store |v_#memory_$Pointer$.offset_494_const_-1833314161| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse80 .cse1 (select .cse81 .cse1)))) (= |v_#memory_$Pointer$.offset_481_const_-1833314067| (store |v_#memory_$Pointer$.offset_482_const_-1833314068| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse45 .cse29 (select .cse82 .cse29)))) (= (select .cse6 .cse74) v_DiskPerfReadWrite_~currentIrpStack~0.base_1_const_783712881) (= |v_#memory_$Pointer$.offset_492_const_-1833314163| (store |v_#memory_$Pointer$.offset_493_const_-1833314164| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse81 .cse49 (select .cse44 .cse49)))) (= |v_#memory_int_501_const_-328415673| (store |v_#memory_int_502_const_-328415674| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse83 .cse10 (select .cse36 .cse10)))) (= |v_#memory_$Pointer$.base_481_const_-344036893| (store |v_#memory_$Pointer$.base_482_const_-344036894| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse84 .cse29 (select .cse85 .cse29)))) (= (store |v_#memory_$Pointer$.base_466_const_-344037336| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse86 .cse29 (select .cse87 .cse29))) |v_#memory_$Pointer$.base_465_const_-344037335|) (= |v_#memory_$Pointer$.base_499_const_-344036984| (store |v_#memory_$Pointer$.base_509_const_-344037582| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store (store (store (store (store (store (store (store (store (store .cse88 .cse13 |v_DiskPerfReadWrite_#t~union129.Thread.base_2_const_-2031704444|) .cse14 |v_DiskPerfReadWrite_#t~union129.ApcListEntry.Flink.base_2_const_-1527009652|) .cse15 |v_DiskPerfReadWrite_#t~union129.ApcListEntry.Blink.base_2_const_-2043345912|) .cse16 |v_DiskPerfReadWrite_#t~union129.KernelRoutine.base_2_const_1825775495|) .cse17 |v_DiskPerfReadWrite_#t~union129.RundownRoutine.base_2_const_200013457|) .cse4 |v_DiskPerfReadWrite_#t~union129.NormalRoutine.base_2_const_1433198781|) .cse18 |v_DiskPerfReadWrite_#t~union129.NormalContext.base_2_const_-213203992|) .cse19 |v_DiskPerfReadWrite_#t~union129.SystemArgument1.base_2_const_-589238619|) .cse10 |v_DiskPerfReadWrite_#t~union129.SystemArgument2.base_2_const_1153565062|) .cse20 (select .cse89 .cse20)))) (= |v_#memory_int_488_const_-328414459| (store |v_#memory_int_489_const_-328414460| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse53 .cse17 (select .cse71 .cse17)))) (= |v_#memory_$Pointer$.offset_478_const_-1833314091| (store |v_#memory_$Pointer$.offset_480_const_-1833314078| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse90 .cse7 (select .cse91 .cse7)))) (= (store |v_#memory_$Pointer$.base_497_const_-344036978| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store (store .cse92 .cse7 |v_DiskPerfReadWrite_#t~union130.base_2_const_-595268668|) .cse74 .cse77)) |v_#memory_$Pointer$.base_495_const_-344036980|) (= |v_#memory_$Pointer$.offset_527_const_-1833314320| (store |v_#memory_$Pointer$.offset_528_const_-1833314317| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse93 .cse7 (select .cse0 .cse7)))) (= v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 |v_DiskPerfReadWrite_#in~Irp.base_1_const_-562692438|) (= |v_#memory_int_468_const_-328414393| (store |v_#memory_int_469_const_-328414394| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse55 .cse10 (select .cse94 .cse10)))) (= |v_#memory_$Pointer$.base_509_const_-344037582| (store |v_#memory_$Pointer$.base_510_const_-344038200| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse95 .cse49 (select .cse88 .cse49)))) (= |v_#memory_int_480_const_-328414339| (store |v_#memory_int_484_const_-328414343| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store (store (store (store .cse47 .cse20 |v_DiskPerfReadWrite_#t~union133.ApcStateIndex_2_const_541030827|) .cse29 |v_DiskPerfReadWrite_#t~union133.ApcMode_2_const_-906448119|) .cse37 |v_DiskPerfReadWrite_#t~union133.Inserted_2_const_1755714176|) .cse7 (select .cse69 .cse7)))) (= (store |v_#memory_int_504_const_-328415680| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse5 .cse18 (select .cse96 .cse18))) |v_#memory_int_503_const_-328415679|) (= (store |v_#memory_$Pointer$.base_465_const_-344037335| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse87 .cse37 (select .cse97 .cse37))) |v_#memory_$Pointer$.base_464_const_-344037330|) (= |v_#memory_$Pointer$.offset_466_const_-1833313494| (store |v_#memory_$Pointer$.offset_476_const_-1833314101| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store (store (store (store (store (store (store (store (store (store .cse50 .cse13 |v_DiskPerfReadWrite_#t~union135.Thread.offset_2_const_659582247|) .cse14 |v_DiskPerfReadWrite_#t~union135.ApcListEntry.Flink.offset_2_const_-435559505|) .cse15 |v_DiskPerfReadWrite_#t~union135.ApcListEntry.Blink.offset_2_const_1586547243|) .cse16 |v_DiskPerfReadWrite_#t~union135.KernelRoutine.offset_2_const_1308920256|) .cse17 |v_DiskPerfReadWrite_#t~union135.RundownRoutine.offset_2_const_-411598604|) .cse4 |v_DiskPerfReadWrite_#t~union135.NormalRoutine.offset_2_const_2141154678|) .cse18 |v_DiskPerfReadWrite_#t~union135.NormalContext.offset_2_const_494332385|) .cse19 |v_DiskPerfReadWrite_#t~union135.SystemArgument1.offset_2_const_-1751226690|) .cse10 |v_DiskPerfReadWrite_#t~union135.SystemArgument2.offset_2_const_-1947601569|) .cse20 (select .cse65 .cse20)))) (= (store |v_#memory_int_523_const_-328415737| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse57 .cse16 (select .cse78 .cse16))) |v_#memory_int_522_const_-328415740|) (= |v_#memory_$Pointer$.base_482_const_-344036894| (store |v_#memory_$Pointer$.base_492_const_-344036989| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store (store (store (store (store (store (store (store (store (store .cse75 .cse13 |v_DiskPerfReadWrite_#t~union133.Thread.base_2_const_1297352299|) .cse14 |v_DiskPerfReadWrite_#t~union133.ApcListEntry.Flink.base_2_const_1038371795|) .cse15 |v_DiskPerfReadWrite_#t~union133.ApcListEntry.Blink.base_2_const_522166639|) .cse16 |v_DiskPerfReadWrite_#t~union133.KernelRoutine.base_2_const_-1881135616|) .cse17 |v_DiskPerfReadWrite_#t~union133.RundownRoutine.base_2_const_1254358904|) .cse4 |v_DiskPerfReadWrite_#t~union133.NormalRoutine.base_2_const_2021402422|) .cse18 |v_DiskPerfReadWrite_#t~union133.NormalContext.base_2_const_374999649|) .cse19 |v_DiskPerfReadWrite_#t~union133.SystemArgument1.base_2_const_2030697214|) .cse10 |v_DiskPerfReadWrite_#t~union133.SystemArgument2.base_2_const_-521466401|) .cse20 (select .cse84 .cse20)))) (= |v_#memory_$Pointer$.offset_495_const_-1833314162| (store |v_#memory_$Pointer$.offset_497_const_-1833314168| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store (store .cse98 .cse7 |v_DiskPerfReadWrite_#t~union130.offset_2_const_207653954|) .cse74 .cse35))) (= |v_#memory_int_492_const_-328414436| (store |v_#memory_int_497_const_-328414437| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store (store (store (store (store .cse38 .cse74 |v_DiskPerfReadWrite_#t~union131_2_const_-1670879116|) .cse7 |v_DiskPerfReadWrite_#t~union133.Type_2_const_-40409282|) .cse1 |v_DiskPerfReadWrite_#t~union133.Size_2_const_-83514313|) .cse49 |v_DiskPerfReadWrite_#t~union133.Spare0_2_const_-1794972929|) .cse13 (select .cse52 .cse13)))) (= |v_#memory_int_505_const_-328415677| (store |v_#memory_int_506_const_-328415678| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse25 .cse17 (select .cse3 .cse17)))) (= |v_#memory_int_519_const_-328415636| (store |v_#memory_int_520_const_-328415622| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse99 .cse18 (select .cse51 .cse18)))) (= v_DiskPerfReadWrite_~currentIrpStack~0.offset_1_const_-1731281009 (select .cse93 .cse74)) (= (store |v_#memory_$Pointer$.base_464_const_-344037330| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store (store .cse97 .cse7 |v_DiskPerfReadWrite_#t~union136.base_2_const_1271668362|) .cse74 (select (select |v_#memory_$Pointer$.base_462_const_-344037332| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378) .cse74))) |v_#memory_$Pointer$.base_462_const_-344037332|) (= |v_#memory_$Pointer$.offset_497_const_-1833314168| (store |v_#memory_$Pointer$.offset_498_const_-1833314165| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse100 .cse37 (select .cse98 .cse37)))) (= |v_#memory_$Pointer$.offset_462_const_-1833313490| (store |v_#memory_$Pointer$.offset_464_const_-1833313496| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store (store .cse101 .cse7 |v_DiskPerfReadWrite_#t~union136.offset_2_const_-971299448|) .cse74 (select (select |v_#memory_$Pointer$.offset_462_const_-1833313490| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378) .cse74)))) (= (store |v_#memory_$Pointer$.base_499_const_-344036984| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse89 .cse29 (select .cse102 .cse29))) |v_#memory_$Pointer$.base_498_const_-344036983|) (= |v_#memory_int_508_const_-328415668| (store |v_#memory_int_509_const_-328415665| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse103 .cse14 (select .cse41 .cse14)))) (= |v_#memory_$Pointer$.offset_525_const_-1833314314| (store |v_#memory_$Pointer$.offset_526_const_-1833314319| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse2 .cse49 (select .cse12 .cse49)))) (= |v_#memory_$Pointer$.offset_494_const_-1833314161| (store |v_#memory_$Pointer$.offset_495_const_-1833314162| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse104 .cse7 (select .cse80 .cse7)))) (= |v_#memory_$Pointer$.base_497_const_-344036978| (store |v_#memory_$Pointer$.base_498_const_-344036983| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse102 .cse37 (select .cse92 .cse37)))) (= |v_#memory_int_524_const_-328415738| (store |v_#memory_int_525_const_-328415743| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse105 .cse14 (select .cse56 .cse14)))) (= |v_#memory_$Pointer$.offset_510_const_-1833314358| (store |v_#memory_$Pointer$.offset_511_const_-1833314347| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse106 .cse1 (select .cse61 .cse1)))) (= |v_#memory_$Pointer$.offset_464_const_-1833313496| (store |v_#memory_$Pointer$.offset_465_const_-1833313493| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse66 .cse37 (select .cse101 .cse37)))) (= |v_#memory_int_502_const_-328415674| (store |v_#memory_int_503_const_-328415679| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse96 .cse19 (select .cse83 .cse19)))) (= |v_#memory_int_513_const_-328415642| (store |v_#memory_int_517_const_-328415646| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store (store (store (store .cse11 .cse20 |v_DiskPerfReadWrite_#t~union127.ApcStateIndex_2_const_-1638734970|) .cse29 |v_DiskPerfReadWrite_#t~union127.ApcMode_2_const_366726564|) .cse37 |v_DiskPerfReadWrite_#t~union127.Inserted_2_const_-1729395835|) .cse7 (select .cse107 .cse7)))) (= (store |v_#memory_$Pointer$.base_511_const_-344038197| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse108 .cse1 (select .cse95 .cse1))) |v_#memory_$Pointer$.base_510_const_-344038200|) (= |v_#memory_$Pointer$.offset_498_const_-1833314165| (store |v_#memory_$Pointer$.offset_499_const_-1833314166| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse109 .cse29 (select .cse100 .cse29)))) (= |v_#memory_int_464_const_-328414277| (store |v_#memory_int_468_const_-328414393| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store (store (store (store .cse94 .cse20 |v_DiskPerfReadWrite_#t~union135.ApcStateIndex_2_const_-1047315031|) .cse29 |v_DiskPerfReadWrite_#t~union135.ApcMode_2_const_-205386361|) .cse37 |v_DiskPerfReadWrite_#t~union135.Inserted_2_const_2014005186|) .cse7 (select .cse73 .cse7)))) (= |v_#memory_int_475_const_-328414373| (store |v_#memory_int_476_const_-328414374| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse70 .cse14 (select .cse110 .cse14)))) (= (store |v_#memory_$Pointer$.base_481_const_-344036893| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse85 .cse37 (select .cse33 .cse37))) |v_#memory_$Pointer$.base_480_const_-344036896|) (= |v_#memory_$Pointer$.base_511_const_-344038197| (store |v_#memory_$Pointer$.base_513_const_-344038187| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse46 .cse7 (select .cse108 .cse7)))) (= |v_#memory_int_509_const_-328415665| (store |v_#memory_int_513_const_-328415642| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store (store (store (store .cse107 .cse7 |v_DiskPerfReadWrite_#t~union129.Type_2_const_-661124891|) .cse1 |v_DiskPerfReadWrite_#t~union129.Size_2_const_-704229890|) .cse49 |v_DiskPerfReadWrite_#t~union129.Spare0_2_const_-1177096474|) .cse13 (select .cse103 .cse13)))) (= |v_#memory_$Pointer$.offset_511_const_-1833314347| (store |v_#memory_$Pointer$.offset_513_const_-1833314345| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse64 .cse7 (select .cse106 .cse7)))) (= |v_#memory_$Pointer$.offset_514_const_-1833314346| (store |v_#memory_$Pointer$.offset_515_const_-1833314351| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse21 .cse29 (select .cse63 .cse29)))) (= |v_#memory_int_520_const_-328415622| (store |v_#memory_int_521_const_-328415739| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse79 .cse4 (select .cse99 .cse4)))) (= |v_#memory_$Pointer$.offset_499_const_-1833314166| (store |v_#memory_$Pointer$.offset_509_const_-1833314756| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store (store (store (store (store (store (store (store (store (store .cse62 .cse13 |v_DiskPerfReadWrite_#t~union129.Thread.offset_2_const_-1520036094|) .cse14 |v_DiskPerfReadWrite_#t~union129.ApcListEntry.Flink.offset_2_const_-1969554166|) .cse15 |v_DiskPerfReadWrite_#t~union129.ApcListEntry.Blink.offset_2_const_52798342|) .cse16 |v_DiskPerfReadWrite_#t~union129.KernelRoutine.offset_2_const_-1176855739|) .cse17 |v_DiskPerfReadWrite_#t~union129.RundownRoutine.offset_2_const_-161505297|) .cse4 |v_DiskPerfReadWrite_#t~union129.NormalRoutine.offset_2_const_-344621317|) .cse18 |v_DiskPerfReadWrite_#t~union129.NormalContext.offset_2_const_-1991443610|) .cse19 |v_DiskPerfReadWrite_#t~union129.SystemArgument1.offset_2_const_1706207971|) .cse10 |v_DiskPerfReadWrite_#t~union129.SystemArgument2.offset_2_const_1509702020|) .cse20 (select .cse109 .cse20)))) (= |v_#memory_$Pointer$.base_515_const_-344038185| (store |v_#memory_$Pointer$.base_525_const_-344038156| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store (store (store (store (store (store (store (store (store (store .cse68 .cse13 |v_DiskPerfReadWrite_#t~union127.Thread.base_2_const_-751699194|) .cse14 |v_DiskPerfReadWrite_#t~union127.ApcListEntry.Flink.base_2_const_844730382|) .cse15 |v_DiskPerfReadWrite_#t~union127.ApcListEntry.Blink.base_2_const_328263050|) .cse16 |v_DiskPerfReadWrite_#t~union127.KernelRoutine.base_2_const_1606915269|) .cse17 |v_DiskPerfReadWrite_#t~union127.RundownRoutine.base_2_const_2005313811|) .cse4 |v_DiskPerfReadWrite_#t~union127.NormalRoutine.base_2_const_1214486011|) .cse18 |v_DiskPerfReadWrite_#t~union127.NormalContext.base_2_const_-431916762|) .cse19 |v_DiskPerfReadWrite_#t~union127.SystemArgument1.base_2_const_-455095197|) .cse10 |v_DiskPerfReadWrite_#t~union127.SystemArgument2.base_2_const_1287724868|) .cse20 (select .cse28 .cse20)))) (= |v_#memory_int_525_const_-328415743| (store |v_#memory_int_529_const_-328415731| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store (store (store (store (select |v_#memory_int_529_const_-328415731| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378) .cse7 |v_DiskPerfReadWrite_#t~union127.Type_2_const_148349603|) .cse1 |v_DiskPerfReadWrite_#t~union127.Size_2_const_105244604|) .cse49 |v_DiskPerfReadWrite_#t~union127.Spare0_2_const_-784068316|) .cse13 (select .cse105 .cse13)))) (= |v_#memory_$Pointer$.offset_480_const_-1833314078| (store |v_#memory_$Pointer$.offset_481_const_-1833314067| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse82 .cse37 (select .cse90 .cse37)))) (= |v_#memory_$Pointer$.offset_477_const_-1833314102| (store |v_#memory_$Pointer$.offset_478_const_-1833314091| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse91 .cse1 (select .cse48 .cse1)))) (= |v_#memory_$Pointer$.base_494_const_-344036979| (store |v_#memory_$Pointer$.base_495_const_-344036980| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse111 .cse7 (select .cse42 .cse7)))) (= |v_#memory_$Pointer$.base_466_const_-344037336| (store |v_#memory_$Pointer$.base_476_const_-344036919| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store (store (store (store (store (store (store (store (store (store .cse60 .cse13 |v_DiskPerfReadWrite_#t~union135.Thread.base_2_const_17494505|) .cse14 |v_DiskPerfReadWrite_#t~union135.ApcListEntry.Flink.base_2_const_-1333368239|) .cse15 |v_DiskPerfReadWrite_#t~union135.ApcListEntry.Blink.base_2_const_-1849557011|) .cse16 |v_DiskPerfReadWrite_#t~union135.KernelRoutine.base_2_const_-1662144318|) .cse17 |v_DiskPerfReadWrite_#t~union135.RundownRoutine.base_2_const_-551088906|) .cse4 |v_DiskPerfReadWrite_#t~union135.NormalRoutine.base_2_const_-2054573576|) .cse18 |v_DiskPerfReadWrite_#t~union135.NormalContext.base_2_const_593990947|) .cse19 |v_DiskPerfReadWrite_#t~union135.SystemArgument1.base_2_const_1896684832|) .cse10 |v_DiskPerfReadWrite_#t~union135.SystemArgument2.base_2_const_-655609855|) .cse20 (select .cse86 .cse20)))) (= |v_#memory_int_474_const_-328414376| (store |v_#memory_int_475_const_-328414373| v_DiskPerfReadWrite_~Irp.base_3_const_1182618378 (store .cse110 .cse15 (select .cse39 .cse15))))))))
(check-sat)
(exit)