(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)