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
|
(set-logic UFLIA)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(set-info :status unsat)
(declare-fun boolIff (Int Int) Int)
(declare-fun PeerGroupPlaceholder_ () Int)
(declare-fun intGreater (Int Int) Int)
(declare-fun IfThenElse_ (Int Int Int) Int)
(declare-fun System.IConvertible () Int)
(declare-fun CONCVARSYM (Int) Int)
(declare-fun throwException_in () Int)
(declare-fun SharingMode_Unshared_ () Int)
(declare-fun System.Reflection.IReflect () Int)
(declare-fun result_0_ () Int)
(declare-fun block3502_2_block3553_correct () Int)
(declare-fun int_m2147483648 () Int)
(declare-fun local0_0 () Int)
(declare-fun System.Int32 () Int)
(declare-fun local0_1 () Int)
(declare-fun block3536_2_block3553_correct () Int)
(declare-fun block3553_correct () Int)
(declare-fun intAtMost (Int Int) Int)
(declare-fun multiply (Int Int) Int)
(declare-fun Is_ (Int Int) Int)
(declare-fun Smt.true () Int)
(declare-fun ElementType_ (Int) Int)
(declare-fun divide (Int Int) Int)
(declare-fun int_m9223372036854775808 () Int)
(declare-fun divides (Int Int) Int)
(declare-fun stack0b_0 () Int)
(declare-fun select1 (Int Int) Int)
(declare-fun stack0b_1 () Int)
(declare-fun store1 (Int Int Int) Int)
(declare-fun select2 (Int Int Int) Int)
(declare-fun nullObject () Int)
(declare-fun store2 (Int Int Int Int) Int)
(declare-fun false3451to3468_correct () Int)
(declare-fun modulo (Int Int) Int)
(declare-fun System.IComparable () Int)
(declare-fun ownerRef_ () Int)
(declare-fun StructSet_ (Int Int Int) Int)
(declare-fun AsDirectSubClass (Int Int) Int)
(declare-fun System.IEquatable_1...System.String () Int)
(declare-fun System.Boolean () Int)
(declare-fun shl_ (Int Int) Int)
(declare-fun DimLength_ (Int Int) Int)
(declare-fun anyEqual (Int Int) Int)
(declare-fun System.Array () Int)
(declare-fun block3451_correct () Int)
(declare-fun System.Collections.Generic.IEnumerable_1...System.Char () Int)
(declare-fun System.Reflection.ICustomAttributeProvider () Int)
(declare-fun SharingMode_LockProtected_ () Int)
(declare-fun IsMemberlessType_ (Int) Int)
(declare-fun PartOfLine () Int)
(declare-fun System.UInt16 () Int)
(declare-fun false3434to3451_correct () Int)
(declare-fun ClassRepr (Int) Int)
(declare-fun System.Runtime.InteropServices._Type () Int)
(declare-fun boolNot (Int) Int)
(declare-fun Microsoft.Contracts.ICheckedException () Int)
(declare-fun System.Exception () Int)
(declare-fun System.Runtime.InteropServices._MemberInfo () Int)
(declare-fun boolAnd (Int Int) Int)
(declare-fun boolImplies (Int Int) Int)
(declare-fun Unbox (Int) Int)
(declare-fun intAtLeast (Int Int) Int)
(declare-fun ownerFrame_ () Int)
(declare-fun int_4294967295 () Int)
(declare-fun IsAllocated (Int Int) Int)
(declare-fun TypeName (Int) Int)
(declare-fun AsPeerField (Int) Int)
(declare-fun int_9223372036854775807 () Int)
(declare-fun AsRepField (Int Int) Int)
(declare-fun System.Reflection.MemberInfo () Int)
(declare-fun ArrayCategoryValue_ () Int)
(declare-fun is (Int Int) Int)
(declare-fun Microsoft.Contracts.GuardException () Int)
(declare-fun InRange (Int Int) Bool)
(declare-fun AsOwner (Int Int) Int)
(declare-fun System.Int64 () Int)
(declare-fun System.Runtime.InteropServices._Exception () Int)
(declare-fun or_ (Int Int) Int)
(declare-fun As_ (Int Int) Int)
(declare-fun exposeVersion_ () Int)
(declare-fun true3434to3536_correct () Int)
(declare-fun System.Type () Int)
(declare-fun intLess (Int Int) Int)
(declare-fun AsImmutable_ (Int) Int)
(declare-fun NonNullFieldsAreInitialized_ () Int)
(declare-fun block3417_correct () Int)
(declare-fun LBound_ (Int Int) Int)
(declare-fun System.Object () Int)
(declare-fun System.UInt32 () Int)
(declare-fun localinv_ () Int)
(declare-fun inv_ () Int)
(declare-fun Interval () Int)
(declare-fun stack50000o_0 () Int)
(declare-fun stack50000o_1 () Int)
(declare-fun Heap_0_ () Int)
(declare-fun entry_correct () Int)
(declare-fun FirstConsistentOwner_ () Int)
(declare-fun UnboxedType (Int) Int)
(declare-fun AsRefField (Int Int) Int)
(declare-fun System.Byte () Int)
(declare-fun this () Int)
(declare-fun stack1o_0 () Int)
(declare-fun int_2147483647 () Int)
(declare-fun ArrayCategoryRef_ () Int)
(declare-fun Interval.a () Int)
(declare-fun Interval.b () Int)
(declare-fun stack1i_0 () Int)
(declare-fun Heap_ () Int)
(declare-fun Length_ (Int) Int)
(declare-fun System.Runtime.Serialization.ISerializable () Int)
(declare-fun AsNonNullRefField (Int Int) Int)
(declare-fun IsHeap (Int) Int)
(declare-fun Heap_1_ () Int)
(declare-fun UBound_ (Int Int) Int)
(declare-fun Cell () Int)
(declare-fun System.String () Int)
(declare-fun System.String.IsInterned_System.String_notnull_ (Int) Int)
(declare-fun Rank_ (Int) Int)
(declare-fun UnknownRef_ () Int)
(declare-fun RefArraySet (Int Int Int) Int)
(declare-fun ValueArraySet (Int Int Int) Int)
(declare-fun stack50000o () Int)
(declare-fun boolOr (Int Int) Int)
(declare-fun sharingMode_ () Int)
(declare-fun subtypes (Int Int) Bool)
(declare-fun System.IComparable_1...System.String () Int)
(declare-fun System.String.Equals_System.String_System.String_ (Int Int) Int)
(declare-fun block3434_correct () Int)
(declare-fun anyNeq (Int Int) Int)
(declare-fun IsStaticField (Int) Int)
(declare-fun SS_Display.Return.Local_0 () Int)
(declare-fun IsNotNull_ (Int Int) Int)
(declare-fun typeof_ (Int) Int)
(declare-fun ArrayCategoryNonNullRef_ () Int)
(declare-fun RefArrayGet (Int Int) Int)
(declare-fun ValueArrayGet (Int Int) Int)
(declare-fun TypeObject (Int) Int)
(declare-fun and_ (Int Int) Int)
(declare-fun BoxTester (Int Int) Int)
(declare-fun Microsoft.Contracts.ObjectInvariantException () Int)
(declare-fun block3468_correct () Int)
(declare-fun IsValueType_ (Int) Int)
(declare-fun Heap_2_ () Int)
(declare-fun AsRangeField (Int Int) Int)
(declare-fun System.SByte () Int)
(declare-fun BeingConstructed_ () Int)
(declare-fun block3502_correct () Int)
(declare-fun FieldDependsOnFCO_ (Int Int Int) Int)
(declare-fun NonNullRefArray (Int Int) Int)
(declare-fun RefArray (Int Int) Int)
(declare-fun ArrayCategory_ (Int) Int)
(declare-fun stack0b () Int)
(declare-fun Cell.Value () Int)
(declare-fun AsPureObject_ (Int) Int)
(declare-fun System.String.Equals_System.String_ (Int Int) Int)
(declare-fun System.Int16 () Int)
(declare-fun block3536_correct () Int)
(declare-fun AsMutable_ (Int) Int)
(declare-fun System.Char () Int)
(declare-fun System.UInt64 () Int)
(declare-fun StructGet_ (Int Int) Int)
(declare-fun OneClassDown (Int Int) Int)
(declare-fun ArrayIndex (Int Int Int Int) Int)
(declare-fun stack0o_0 () Int)
(declare-fun Box (Int Int) Int)
(declare-fun stack0o_1 () Int)
(declare-fun int_18446744073709551615 () Int)
(declare-fun shr_ (Int Int) Int)
(declare-fun stack0i_0 () Int)
(declare-fun block3553_2_GeneratedUnifiedExit_correct () Int)
(declare-fun System.ICloneable () Int)
(declare-fun IsDirectlyModifiableField (Int) Int)
(declare-fun StringLength_ (Int) Int)
(declare-fun allocated_ () Int)
(declare-fun BaseClass_ (Int) Int)
(declare-fun ValueArray (Int Int) Int)
(declare-fun Smt.false () Int)
(declare-fun true3451to3502_correct () Int)
(declare-fun IsImmutable_ (Int) Int)
(declare-fun elements_ () Int)
(declare-fun DeclType (Int) Int)
(declare-fun System.Collections.IEnumerable () Int)
(declare-fun ReallyLastGeneratedExit_correct () Int)
(assert (forall ((?o Int) (?T Int)) (! (= (= (IsNotNull_ ?o ?T) Smt.true) (and (not (= ?o nullObject)) (= (Is_ ?o ?T) Smt.true))) :pattern ((IsNotNull_ ?o ?T)) )))
(assert (forall ((?h Int) (?o Int) (?f Int) (?T Int)) (! (=> (and (= (IsHeap ?h) Smt.true) (not (= ?o nullObject)) (or (not (= ?o BeingConstructed_)) (= (= (select2 ?h BeingConstructed_ NonNullFieldsAreInitialized_) Smt.true) true))) (not (= (select2 ?h ?o (AsNonNullRefField ?f ?T)) nullObject))) :pattern ((select2 ?h ?o (AsNonNullRefField ?f ?T))) )))
(assert (forall ((?o Int) (?T Int)) (! (=> (and (not (= ?o nullObject)) (not (= ?o BeingConstructed_)) (subtypes (typeof_ ?o) (AsImmutable_ ?T))) (forall ((?h Int)) (! (let ((?v_0 (typeof_ ?o))) (=> (= (IsHeap ?h) Smt.true) (and (= (select2 ?h ?o inv_) ?v_0) (= (select2 ?h ?o localinv_) ?v_0) (= (select2 ?h ?o ownerFrame_) PeerGroupPlaceholder_) (= (AsOwner ?o (select2 ?h ?o ownerRef_)) ?o) (forall ((?t Int)) (! (=> (= (AsOwner ?o (select2 ?h ?t ownerRef_)) ?o) (or (= ?t ?o) (not (= (select2 ?h ?t ownerFrame_) PeerGroupPlaceholder_)))) :pattern ((AsOwner ?o (select2 ?h ?t ownerRef_))) ))))) :pattern ((IsHeap ?h)) ))) :pattern ((subtypes (typeof_ ?o) (AsImmutable_ ?T))) )))
(assert (= (IsValueType_ System.SByte) Smt.true))
(assert (= (IsValueType_ System.Byte) Smt.true))
(assert (= (IsValueType_ System.Int16) Smt.true))
(assert (= (IsValueType_ System.UInt16) Smt.true))
(assert (= (IsValueType_ System.Int32) Smt.true))
(assert (= (IsValueType_ System.UInt32) Smt.true))
(assert (= (IsValueType_ System.Int64) Smt.true))
(assert (= (IsValueType_ System.UInt64) Smt.true))
(assert (= (IsValueType_ System.Char) Smt.true))
(assert (< int_m9223372036854775808 int_m2147483648))
(assert (< int_m2147483648 (- 0 100000)))
(assert (< 100000 int_2147483647))
(assert (< int_2147483647 int_4294967295))
(assert (< int_4294967295 int_9223372036854775807))
(assert (< int_9223372036854775807 int_18446744073709551615))
(assert (not (= (IsStaticField Cell.Value) Smt.true)))
(assert (= (IsDirectlyModifiableField Cell.Value) Smt.true))
(assert (= (DeclType Cell.Value) Cell))
(assert (= (AsRangeField Cell.Value System.Int32) Cell.Value))
(assert (not (= (IsStaticField Interval.a) Smt.true)))
(assert (= (IsDirectlyModifiableField Interval.a) Smt.true))
(assert (= (AsRepField Interval.a Interval) Interval.a))
(assert (= (DeclType Interval.a) Interval))
(assert (= (AsNonNullRefField Interval.a Cell) Interval.a))
(assert (not (= (IsStaticField Interval.b) Smt.true)))
(assert (= (IsDirectlyModifiableField Interval.b) Smt.true))
(assert (= (AsRepField Interval.b Interval) Interval.b))
(assert (= (DeclType Interval.b) Interval))
(assert (= (AsNonNullRefField Interval.b Cell) Interval.b))
(assert (subtypes Cell Cell))
(assert (= (BaseClass_ Cell) System.Object))
(assert (subtypes Cell (BaseClass_ Cell)))
(assert (= (AsDirectSubClass Cell (BaseClass_ Cell)) Cell))
(assert (not (= (IsImmutable_ Cell) Smt.true)))
(assert (= (AsMutable_ Cell) Cell))
(assert (subtypes System.Type System.Type))
(assert (subtypes System.Reflection.MemberInfo System.Reflection.MemberInfo))
(assert (= (BaseClass_ System.Reflection.MemberInfo) System.Object))
(assert (subtypes System.Reflection.MemberInfo (BaseClass_ System.Reflection.MemberInfo)))
(assert (= (AsDirectSubClass System.Reflection.MemberInfo (BaseClass_ System.Reflection.MemberInfo)) System.Reflection.MemberInfo))
(assert (= (IsImmutable_ System.Reflection.MemberInfo) Smt.true))
(assert (= (AsImmutable_ System.Reflection.MemberInfo) System.Reflection.MemberInfo))
(assert (subtypes System.Reflection.ICustomAttributeProvider System.Object))
(assert (= (IsMemberlessType_ System.Reflection.ICustomAttributeProvider) Smt.true))
(assert (subtypes System.Reflection.MemberInfo System.Reflection.ICustomAttributeProvider))
(assert (subtypes System.Runtime.InteropServices._MemberInfo System.Object))
(assert (= (IsMemberlessType_ System.Runtime.InteropServices._MemberInfo) Smt.true))
(assert (subtypes System.Reflection.MemberInfo System.Runtime.InteropServices._MemberInfo))
(assert (= (IsMemberlessType_ System.Reflection.MemberInfo) Smt.true))
(assert (= (BaseClass_ System.Type) System.Reflection.MemberInfo))
(assert (subtypes System.Type (BaseClass_ System.Type)))
(assert (= (AsDirectSubClass System.Type (BaseClass_ System.Type)) System.Type))
(assert (= (IsImmutable_ System.Type) Smt.true))
(assert (= (AsImmutable_ System.Type) System.Type))
(assert (subtypes System.Runtime.InteropServices._Type System.Object))
(assert (= (IsMemberlessType_ System.Runtime.InteropServices._Type) Smt.true))
(assert (subtypes System.Type System.Runtime.InteropServices._Type))
(assert (subtypes System.Reflection.IReflect System.Object))
(assert (= (IsMemberlessType_ System.Reflection.IReflect) Smt.true))
(assert (subtypes System.Type System.Reflection.IReflect))
(assert (= (IsMemberlessType_ System.Type) Smt.true))
(assert (subtypes PartOfLine PartOfLine))
(assert (= (BaseClass_ PartOfLine) System.Object))
(assert (subtypes PartOfLine (BaseClass_ PartOfLine)))
(assert (= (AsDirectSubClass PartOfLine (BaseClass_ PartOfLine)) PartOfLine))
(assert (distinct Smt.false Smt.true))
(assert (let ((?v_0 (select2 Heap_ this ownerFrame_)) (?v_1 (select2 Heap_ this ownerRef_)) (?v_2 (not (= this nullObject))) (?v_3 (not (= stack0o_0 nullObject))) (?v_4 (not (= stack1o_0 nullObject))) (?v_5 (forall ((?o_ Int)) (=> (and (not (= ?o_ nullObject)) (= (= (select2 Heap_ ?o_ allocated_) Smt.true) true)) (and (= (select2 Heap_ ?o_ ownerRef_) (select2 Heap_2_ ?o_ ownerRef_)) (= (select2 Heap_ ?o_ ownerFrame_) (select2 Heap_2_ ?o_ ownerFrame_)))))) (?v_12 (=> true true)) (?v_6 (= ReallyLastGeneratedExit_correct Smt.true)) (?v_7 (= block3553_2_GeneratedUnifiedExit_correct Smt.true)) (?v_15 (= block3553_correct Smt.true)) (?v_14 (= throwException_in Smt.true)) (?v_8 (not (= stack50000o_0 nullObject))) (?v_11 (typeof_ stack50000o_0)) (?v_9 (select2 Heap_1_ stack50000o_0 ownerFrame_)) (?v_10 (select2 Heap_1_ stack50000o_0 ownerRef_)) (?v_13 (= block3468_correct Smt.true)) (?v_19 (= false3451to3468_correct Smt.true))) (let ((?v_21 (=> true ?v_15)) (?v_16 (= block3502_2_block3553_correct Smt.true)) (?v_17 (= block3502_correct Smt.true)) (?v_18 (= true3451to3502_correct Smt.true)) (?v_20 (= block3451_correct Smt.true)) (?v_25 (= false3434to3451_correct Smt.true)) (?v_22 (= block3536_2_block3553_correct Smt.true)) (?v_23 (= block3536_correct Smt.true)) (?v_24 (= true3434to3536_correct Smt.true)) (?v_26 (= block3434_correct Smt.true)) (?v_27 (= block3417_correct Smt.true)) (?v_28 (= entry_correct Smt.true))) (not (=> (=> (=> true (=> (= (IsHeap Heap_) Smt.true) (=> true (=> (= BeingConstructed_ nullObject) (=> (and (or (= ?v_0 PeerGroupPlaceholder_) (not (subtypes (select2 Heap_ ?v_1 inv_) ?v_0)) (= (select2 Heap_ ?v_1 localinv_) (BaseClass_ ?v_0))) (forall ((?pc_ Int)) (let ((?v_29 (typeof_ ?pc_))) (=> (and (not (= ?pc_ nullObject)) (= (= (select2 Heap_ ?pc_ allocated_) Smt.true) true) (= (select2 Heap_ ?pc_ ownerRef_) ?v_1) (= (select2 Heap_ ?pc_ ownerFrame_) ?v_0)) (and (= (select2 Heap_ ?pc_ inv_) ?v_29) (= (select2 Heap_ ?pc_ localinv_) ?v_29)))))) (=> true (=> true (=> (= (IsNotNull_ this Interval) Smt.true) (=> (= (= (select2 Heap_ this allocated_) Smt.true) true) (=> true (=> (=> (=> true (=> true (=> true (=> (=> (=> true (=> true (and ?v_2 (=> ?v_2 (=> (= stack0o_0 (select2 Heap_ this Interval.a)) (and ?v_3 (=> ?v_3 (=> (= stack0i_0 (select2 Heap_ stack0o_0 Cell.Value)) (and ?v_2 (=> ?v_2 (=> (= stack1o_0 (select2 Heap_ this Interval.b)) (and ?v_4 (=> ?v_4 (=> (= stack1i_0 (select2 Heap_ stack1o_0 Cell.Value)) (=> true (=> (and (=> (=> true (=> true (=> true (=> (=> (=> true (=> (= SS_Display.Return.Local_0 local0_0) (=> (= result_0_ local0_0) (=> (= stack50000o_1 stack50000o) (=> (= stack0b_1 local0_0) (=> (= stack0o_1 stack0o_0) (=> (= local0_1 local0_0) (=> (= Heap_2_ Heap_) (=> (=> (=> true (and ?v_5 (=> ?v_5 ?v_12))) ?v_6) ?v_6))))))))) ?v_7) ?v_7)))) ?v_15) (=> (=> true (=> true (=> (> stack0i_0 stack1i_0) (=> true (=> (=> (=> true (=> true (=> true (=> (and (=> (=> true (=> true (=> ?v_14 (=> true (=> (=> (=> true (=> true (=> false (=> (and (= (= (select2 Heap_ stack50000o_0 allocated_) Smt.true) false) ?v_8 (= ?v_11 Microsoft.Contracts.ObjectInvariantException)) (=> (and (= (select2 Heap_ stack50000o_0 ownerRef_) stack50000o_0) (= (select2 Heap_ stack50000o_0 ownerFrame_) PeerGroupPlaceholder_)) (=> (= Heap_0_ (store2 Heap_ stack50000o_0 allocated_ Smt.true)) (and ?v_8 (=> ?v_8 (=> (= (IsHeap Heap_1_) Smt.true) (=> (and (or (= ?v_9 PeerGroupPlaceholder_) (not (subtypes (select2 Heap_1_ ?v_10 inv_) ?v_9)) (= (select2 Heap_1_ ?v_10 localinv_) (BaseClass_ ?v_9))) (= (select2 Heap_1_ stack50000o_0 inv_) Microsoft.Contracts.ObjectInvariantException) (= (select2 Heap_1_ stack50000o_0 localinv_) ?v_11)) (=> (and (= ?v_10 (select2 Heap_0_ stack50000o_0 ownerRef_)) (= ?v_9 (select2 Heap_0_ stack50000o_0 ownerFrame_))) (=> (= (select2 Heap_1_ stack50000o_0 sharingMode_) SharingMode_Unshared_) (=> (forall ((?o_ Int)) (let ((?v_30 (typeof_ ?o_))) (=> (and (not (= ?o_ nullObject)) (= (= (select2 Heap_0_ ?o_ allocated_) Smt.true) (not true)) (= (= (select2 Heap_1_ ?o_ allocated_) Smt.true) true)) (and (= (select2 Heap_1_ ?o_ inv_) ?v_30) (= (select2 Heap_1_ ?o_ localinv_) ?v_30))))) (=> (forall ((?o_ Int)) (! (let ((?v_31 (select2 Heap_0_ ?o_ FirstConsistentOwner_))) (=> (= (select2 Heap_0_ ?v_31 exposeVersion_) (select2 Heap_1_ ?v_31 exposeVersion_)) (= ?v_31 (select2 Heap_1_ ?o_ FirstConsistentOwner_)))) :pattern ((select2 Heap_1_ ?o_ FirstConsistentOwner_)) )) (=> (forall ((?o_ Int)) (=> (and (not (= ?o_ nullObject)) (= (= (select2 Heap_0_ ?o_ allocated_) Smt.true) true)) (and (= (select2 Heap_0_ ?o_ ownerRef_) (select2 Heap_1_ ?o_ ownerRef_)) (= (select2 Heap_0_ ?o_ ownerFrame_) (select2 Heap_1_ ?o_ ownerFrame_))))) (=> (forall ((?o_ Int) (?f_ Int)) (! (let ((?v_32 (select2 Heap_0_ ?o_ ownerFrame_)) (?v_33 (select2 Heap_0_ ?o_ ownerRef_))) (=> (and (not (= ?f_ inv_)) (not (= ?f_ localinv_)) (not (= ?f_ FirstConsistentOwner_)) (or (not (= (IsStaticField ?f_) Smt.true)) (not (= (IsDirectlyModifiableField ?f_) Smt.true))) (not (= ?o_ nullObject)) (= (= (select2 Heap_0_ ?o_ allocated_) Smt.true) true) (or (= ?v_32 PeerGroupPlaceholder_) (not (subtypes (select2 Heap_0_ ?v_33 inv_) ?v_32)) (= (select2 Heap_0_ ?v_33 localinv_) (BaseClass_ ?v_32))) (or (not (= ?o_ stack50000o_0)) (not (subtypes Microsoft.Contracts.ObjectInvariantException (DeclType ?f_)))) true) (= (select2 Heap_0_ ?o_ ?f_) (select2 Heap_1_ ?o_ ?f_)))) :pattern ((select2 Heap_1_ ?o_ ?f_)) )) (=> (forall ((?o_ Int)) (or (= ?o_ stack50000o_0) (and (= (select2 Heap_0_ ?o_ inv_) (select2 Heap_1_ ?o_ inv_)) (= (select2 Heap_0_ ?o_ localinv_) (select2 Heap_1_ ?o_ localinv_))) (= (= (select2 Heap_0_ ?o_ allocated_) Smt.true) (not true)))) (=> (and (forall ((?o_ Int)) (=> (= (= (select2 Heap_0_ ?o_ allocated_) Smt.true) true) (= (= (select2 Heap_1_ ?o_ allocated_) Smt.true) true))) (forall ((?ot_ Int)) (let ((?v_34 (select2 Heap_0_ ?ot_ ownerFrame_))) (=> (and (= (= (select2 Heap_0_ ?ot_ allocated_) Smt.true) true) (not (= ?v_34 PeerGroupPlaceholder_))) (and (= (select2 Heap_1_ ?ot_ ownerRef_) (select2 Heap_0_ ?ot_ ownerRef_)) (= (select2 Heap_1_ ?ot_ ownerFrame_) ?v_34))))) (= (= (select2 Heap_0_ BeingConstructed_ NonNullFieldsAreInitialized_) Smt.true) (= (select2 Heap_1_ BeingConstructed_ NonNullFieldsAreInitialized_) Smt.true))) (=> (forall ((?o_ Int)) (or (= ?o_ stack50000o_0) (= (select2 Heap_0_ ?o_ sharingMode_) (select2 Heap_1_ ?o_ sharingMode_)))) (and ?v_8 (=> ?v_8 (=> false (=> true ?v_12))))))))))))))))))))))) ?v_13) ?v_13))))) ?v_19) (=> (=> true (=> true (=> (not ?v_14) (=> true (=> (=> (=> true (=> true (=> true (=> (=> (=> true (=> (= stack0b_0 throwException_in) (=> (= local0_0 Smt.false) ?v_21))) ?v_16) ?v_16)))) ?v_17) ?v_17))))) ?v_18)) (and ?v_18 ?v_19))))) ?v_20) ?v_20))))) ?v_25) (=> (=> true (=> true (=> (<= stack0i_0 stack1i_0) (=> true (=> (=> (=> true (=> true (=> true (=> (=> (=> true (=> (= stack0b_0 stack0b) (=> (= local0_0 Smt.true) ?v_21))) ?v_22) ?v_22)))) ?v_23) ?v_23))))) ?v_24)) (and ?v_24 ?v_25))))))))))))))))) ?v_26) ?v_26)))) ?v_27) ?v_27))))))))))) ?v_28) ?v_28)))))
(check-sat)
(exit)
|
