Fixes for relational triggers (#2967)

1 files changed, 207 insertions, 0 deletions

diff --git a/test/regress/regress2/quantifiers/specsharp-WindowsCard.15.RTE.Terminate_System.Int32.smt2 b/test/regress/regress2/quantifiers/specsharp-WindowsCard.15.RTE.Terminate_System.Int32.smt2
new file mode 100644
index 000000000..7be432dbf
--- /dev/null
+++ b/test/regress/regress2/quantifiers/specsharp-WindowsCard.15.RTE.Terminate_System.Int32.smt2
@@ -0,0 +1,207 @@
+(set-logic UFNIA)
+(set-info :source |

+    Spec# benchmarks.  Contributed by Leonardo de Moura and Michal Moskal.

+  |)
+(set-info :smt-lib-version 2.0)
+(set-info :category "industrial")
+(set-info :status unsat)
+(declare-fun x (Int Int) Int)
+(declare-fun true_1 () Int)
+(declare-fun false_1 () Int)
+(declare-fun intGreater (Int Int) Int)
+(declare-fun intAtLeast (Int Int) Int)
+(declare-fun intAtMost (Int Int) Int)
+(declare-fun intLess (Int Int) Int)
+(declare-fun anyNeq (Int Int) Int)
+(declare-fun anyEqual (Int Int) Int)
+(declare-fun boolNot (Int) Int)
+(declare-fun boolOr (Int Int) Int)
+(declare-fun boolAnd (Int Int) Int)
+(declare-fun boolImplies (Int Int) Int)
+(declare-fun boolIff (Int Int) Int)
+(declare-fun select2 (Int Int Int) Int)
+(declare-fun store2 (Int Int Int Int) Int)
+(declare-fun select1 (Int Int) Int)
+(declare-fun store1 (Int Int Int) Int)
+(declare-fun Microsoft_Contracts_ICheckedException () Int)
+(declare-fun AsInterface (Int) Int)
+(declare-fun IsMemberlessType (Int) Int)
+(declare-fun System_Object () Int)
+(declare-fun System_String () Int)
+(declare-fun inv () Int)
+(declare-fun BaseClass (Int) Int)
+(declare-fun localinv () Int)
+(declare-fun IsHeap (Int) Int)
+(declare-fun System_IEquatable_1___System_String () Int)
+(declare-fun System_Collections_IEnumerable () Int)
+(declare-fun System_Collections_Generic_IEnumerable_1___System_Char () Int)
+(declare-fun System_IComparable_1___System_String () Int)
+(declare-fun System_IConvertible () Int)
+(declare-fun System_ICloneable () Int)
+(declare-fun System_IComparable () Int)
+(declare-fun AsImmutable (Int) Int)
+(declare-fun IsImmutable (Int) Int)
+(declare-fun AsDirectSubClass (Int Int) Int)
+(declare-fun Microsoft_Contracts_ObjectInvariantException () Int)
+(declare-fun AsMutable (Int) Int)
+(declare-fun Microsoft_Contracts_GuardException () Int)
+(declare-fun System_Exception () Int)
+(declare-fun System_Runtime_InteropServices__Exception () Int)
+(declare-fun System_Runtime_Serialization_ISerializable () Int)
+(declare-fun RTE () Int)
+(declare-fun RTE_MStackMaxSize () Int)
+(declare-fun RTE_MStackBase () Int)
+(declare-fun RTE_DPP () Int)
+(declare-fun Length (Int) Int)
+(declare-fun Memory_contents () Int)
+(declare-fun RTE_Scratch () Int)
+(declare-fun x_1 (Int Int) Int)
+(declare-fun RTE_MSP () Int)
+(declare-fun RTE_CSP () Int)
+(declare-fun RTE_CallStack () Int)
+(declare-fun RTE_Data () Int)
+(declare-fun Memory_InSandbox_System_Int32 (Int Int Int) Int)
+(declare-fun Memory_InSandbox_System_Int32_1 (Int Int) Int)
+(declare-fun exposeVersion () Int)
+(declare-fun allocated () Int)
+(declare-fun typeof (Int) Int)
+(declare-fun Memory () Int)
+(declare-fun nullObject () Int)
+(declare-fun AsPureObject (Int) Int)
+(declare-fun FirstConsistentOwner () Int)
+(declare-fun ownerRef () Int)
+(declare-fun ownerFrame () Int)
+(declare-fun PeerGroupPlaceholder () Int)
+(declare-fun IsNotNull (Int Int) Int)
+(declare-fun PurityAxiomsCanBeAssumed () Int)
+(declare-fun System_Type () Int)
+(declare-fun System_Reflection_IReflect () Int)
+(declare-fun System_Runtime_InteropServices__Type () Int)
+(declare-fun System_Reflection_MemberInfo () Int)
+(declare-fun System_Runtime_InteropServices__MemberInfo () Int)
+(declare-fun System_Reflection_ICustomAttributeProvider () Int)
+(declare-fun Memory_get_cont_System_Int32 (Int Int Int) Int)
+(declare-fun Memory_get_cont_System_Int32_1 (Int Int) Int)
+(declare-fun System_Array () Int)
+(declare-fun System_Collections_ICollection () Int)
+(declare-fun System_Collections_IList () Int)
+(declare-fun RTE_Instructions () Int)
+(declare-fun AsNonNullRefField (Int Int) Int)
+(declare-fun IntArray (Int Int) Int)
+(declare-fun System_Int32 () Int)
+(declare-fun DeclType (Int) Int)
+(declare-fun AsRepField (Int Int) Int)
+(declare-fun IncludedInModifiesStar (Int) Int)
+(declare-fun IncludeInMainFrameCondition (Int) Int)
+(declare-fun IsStaticField (Int) Int)
+(declare-fun RTE_Program () Int)
+(declare-fun RTE_RtnCode () Int)
+(declare-fun AsRangeField (Int Int) Int)
+(declare-fun RTE_CurrRTEMode () Int)
+(declare-fun RTE_PC () Int)
+(declare-fun RTE_C () Int)
+(declare-fun RTE_Z () Int)
+(declare-fun RTE_A () Int)
+(declare-fun RTE_MStackMaxSize_1 (Int) Int)
+(declare-fun RTE_MStackBase_1 (Int) Int)
+(declare-fun Memory_contents_1 (Int) Int)
+(declare-fun System_Byte () Int)
+(declare-fun System_String_Equals_System_String_System_String (Int Int Int) Int)
+(declare-fun System_String_IsInterned_System_String_notnull (Int Int) Int)
+(declare-fun StringEquals (Int Int) Int)
+(declare-fun System_String_Equals_System_String (Int Int Int) Int)
+(declare-fun max (Int Int) Int)
+(declare-fun min (Int Int) Int)
+(declare-fun shr (Int Int) Int)
+(declare-fun x_2 (Int Int) Int)
+(declare-fun shl (Int Int) Int)
+(declare-fun int_2147483647 () Int)
+(declare-fun or_1 (Int Int) Int)
+(declare-fun and_1 (Int Int) Int)
+(declare-fun IfThenElse (Int Int Int) Int)
+(declare-fun IntToInt (Int Int Int) Int)
+(declare-fun InRange (Int Int) Int)
+(declare-fun System_Char () Int)
+(declare-fun int_18446744073709551615 () Int)
+(declare-fun System_UInt64 () Int)
+(declare-fun int_9223372036854775807 () Int)
+(declare-fun int_m9223372036854775808 () Int)
+(declare-fun System_Int64 () Int)
+(declare-fun int_4294967295 () Int)
+(declare-fun System_UInt32 () Int)
+(declare-fun int_m2147483648 () Int)
+(declare-fun System_UInt16 () Int)
+(declare-fun System_Int16 () Int)
+(declare-fun System_SByte () Int)
+(declare-fun IsValueType (Int) Int)
+(declare-fun System_IntPtr () Int)
+(declare-fun System_UIntPtr () Int)
+(declare-fun BoxTester (Int Int) Int)
+(declare-fun Box (Int Int) Int)
+(declare-fun Unbox (Int) Int)
+(declare-fun UnboxedType (Int) Int)
+(declare-fun BoxFunc (Int Int Int Int) Int)
+(declare-fun FieldDependsOnFCO (Int Int Int) Int)
+(declare-fun AsElementsPeerField (Int Int) Int)
+(declare-fun ElementProxy (Int Int) Int)
+(declare-fun AsElementsRepField (Int Int Int) Int)
+(declare-fun AsPeerField (Int) Int)
+(declare-fun StringLength (Int) Int)
+(declare-fun AsOwner (Int Int) Int)
+(declare-fun BeingConstructed () Int)
+(declare-fun NonNullFieldsAreInitialized () Int)
+(declare-fun AsRefField (Int Int) Int)
+(declare-fun Is (Int Int) Int)
+(declare-fun ClassRepr (Int) Int)
+(declare-fun IsAllocated (Int Int) Int)
+(declare-fun ValueArrayGet (Int Int) Int)
+(declare-fun RefArrayGet (Int Int) Int)
+(declare-fun StructGet (Int Int) Int)
+(declare-fun As (Int Int) Int)
+(declare-fun TypeObject (Int) Int)
+(declare-fun TypeName (Int) Int)
+(declare-fun System_Boolean () Int)
+(declare-fun OneClassDown (Int Int) Int)
+(declare-fun StructSet (Int Int Int) Int)
+(declare-fun ElementProxyStruct (Int Int) Int)
+(declare-fun elements () Int)
+(declare-fun ValueArray (Int Int) Int)
+(declare-fun NonNullRefArray (Int Int) Int)
+(declare-fun ElementType (Int) Int)
+(declare-fun RefArray (Int Int) Int)
+(declare-fun NonNullRefArrayRaw (Int Int Int) Int)
+(declare-fun Rank (Int) Int)
+(declare-fun ArrayCategoryNonNullRef () Int)
+(declare-fun ArrayCategory (Int) Int)
+(declare-fun ArrayCategoryRef () Int)
+(declare-fun ArrayCategoryInt () Int)
+(declare-fun ArrayCategoryValue () Int)
+(declare-fun UBound (Int Int) Int)
+(declare-fun DimLength (Int Int) Int)
+(declare-fun LBound (Int Int) Int)
+(declare-fun IntArrayGet (Int Int) Int)
+(declare-fun ArrayIndex (Int Int Int Int) Int)
+(declare-fun ArrayIndexInvY (Int) Int)
+(declare-fun ArrayIndexInvX (Int) Int)
+(declare-fun RefArraySet (Int Int Int) Int)
+(declare-fun IntArraySet (Int Int Int) Int)
+(declare-fun ValueArraySet (Int Int Int) Int)
+(declare-fun ClassReprInv (Int) Int)
+(declare-fun SharingMode_LockProtected () Int)
+(declare-fun SharingMode_Unshared () Int)
+(declare-fun sharingMode () Int)
+(declare-fun Heap_3 () Int)
+(declare-fun Heap () Int)
+(declare-fun this () Int)
+(declare-fun code_in () Int)
+(declare-fun Heap_2 () Int)
+(declare-fun temp1_0 () Int)
+(declare-fun Heap_1 () Int)
+(declare-fun Heap_0 () Int)
+(declare-fun temp0_0 () Int)
+(declare-fun code () Int)
+(assert (not (or (not (forall ((?A Int) (?i Int) (?v Int)) (= (select1 (store1 ?A ?i ?v) ?i) ?v))) (not (forall ((?A Int) (?i Int) (?j Int) (?v Int)) (=> (not (= ?i ?j)) (= (select1 (store1 ?A ?i ?v) ?j) (select1 ?A ?j))))) (not (forall ((?A Int) (?o Int) (?f Int) (?v Int)) (= (select2 (store2 ?A ?o ?f ?v) ?o ?f) ?v))) (not (forall ((?A Int) (?o Int) (?f Int) (?p Int) (?g Int) (?v Int)) (=> (not (= ?o ?p)) (= (select2 (store2 ?A ?o ?f ?v) ?p ?g) (select2 ?A ?p ?g))))) (not (forall ((?A Int) (?o Int) (?f Int) (?p Int) (?g Int) (?v Int)) (=> (not (= ?f ?g)) (= (select2 (store2 ?A ?o ?f ?v) ?p ?g) (select2 ?A ?p ?g))))) (not (forall ((?x_3 Int) (?y Int)) (= (= (boolIff ?x_3 ?y) true_1) (= (= ?x_3 true_1) (= ?y true_1))))) (not (forall ((?x_3 Int) (?y Int)) (= (= (boolImplies ?x_3 ?y) true_1) (=> (= ?x_3 true_1) (= ?y true_1))))) (not (forall ((?x_3 Int) (?y Int)) (= (= (boolAnd ?x_3 ?y) true_1) (not (or (not (= ?x_3 true_1)) (not (= ?y true_1))))))) (not (forall ((?x_3 Int) (?y Int)) (= (= (boolOr ?x_3 ?y) true_1) (or (= ?x_3 true_1) (= ?y true_1))))) (not (forall ((?x_3 Int)) (! (= (= (boolNot ?x_3) true_1) (not (= ?x_3 true_1))) :pattern ((boolNot ?x_3)) ))) (not (forall ((?x_3 Int) (?y Int)) (= (= (anyEqual ?x_3 ?y) true_1) (= ?x_3 ?y)))) (not (forall ((?x_3 Int) (?y Int)) (! (= (= (anyNeq ?x_3 ?y) true_1) (not (= ?x_3 ?y))) :pattern ((anyNeq ?x_3 ?y)) ))) (not (forall ((?x_3 Int) (?y Int)) (= (= (intLess ?x_3 ?y) true_1) (< ?x_3 ?y)))) (not (forall ((?x_3 Int) (?y Int)) (= (= (intAtMost ?x_3 ?y) true_1) (<= ?x_3 ?y)))) (not (forall ((?x_3 Int) (?y Int)) (= (= (intAtLeast ?x_3 ?y) true_1) (>= ?x_3 ?y)))) (not (forall ((?x_3 Int) (?y Int)) (= (= (intGreater ?x_3 ?y) true_1) (> ?x_3 ?y)))) (not (distinct false_1 true_1)) (not (forall ((?t Int)) (! (= (x ?t ?t) true_1) :pattern ((x ?t ?t)) ))) (not (forall ((?t Int) (?u Int) (?v Int)) (! (=> (not (or (not (= (x ?t ?u) true_1)) (not (= (x ?u ?v) true_1)))) (= (x ?t ?v) true_1)) :pattern ((x ?t ?u) (x ?u ?v)) ))) (not (forall ((?t Int) (?u Int)) (! (=> (not (or (not (= (x ?t ?u) true_1)) (not (= (x ?u ?t) true_1)))) (= ?t ?u)) :pattern ((x ?t ?u) (x ?u ?t)) ))))))
+(assert (let ((?v_10 (BaseClass System_String)) (?v_9 (BaseClass Microsoft_Contracts_ObjectInvariantException)) (?v_8 (BaseClass Microsoft_Contracts_GuardException)) (?v_7 (BaseClass System_Exception)) (?v_6 (BaseClass RTE)) (?v_5 (= PurityAxiomsCanBeAssumed true_1)) (?v_4 (BaseClass System_Type)) (?v_3 (BaseClass System_Reflection_MemberInfo)) (?v_2 (BaseClass System_Array)) (?v_1 (BaseClass Memory)) (?v_0 (IntArray System_Int32 1))) (not (or (not (distinct allocated elements inv localinv exposeVersion sharingMode SharingMode_Unshared SharingMode_LockProtected ownerRef ownerFrame PeerGroupPlaceholder ArrayCategoryValue ArrayCategoryInt ArrayCategoryRef ArrayCategoryNonNullRef System_Array System_Boolean System_Object System_Type NonNullFieldsAreInitialized System_String FirstConsistentOwner System_SByte System_Byte System_Int16 System_UInt16 System_Int32 System_UInt32 System_Int64 System_UInt64 System_Char System_UIntPtr System_IntPtr RTE_Instructions RTE_C RTE_CallStack RTE_Z RTE_Scratch RTE_MSP RTE_CurrRTEMode RTE_DPP Memory_contents RTE_Program RTE_MStackBase RTE_A RTE_PC RTE_RtnCode RTE_CSP RTE_Data RTE_MStackMaxSize System_ICloneable System_Reflection_MemberInfo System_Runtime_InteropServices__MemberInfo System_Runtime_Serialization_ISerializable RTE System_Exception System_Runtime_InteropServices__Exception Microsoft_Contracts_ObjectInvariantException System_Runtime_InteropServices__Type System_Collections_IList System_Reflection_ICustomAttributeProvider System_Collections_ICollection System_Reflection_IReflect System_Collections_IEnumerable System_IComparable Microsoft_Contracts_ICheckedException Memory System_IComparable_1___System_String System_IConvertible System_Collections_Generic_IEnumerable_1___System_Char System_IEquatable_1___System_String Microsoft_Contracts_GuardException)) (not (= (DeclType elements) System_Object)) (not (= (DeclType exposeVersion) System_Object)) (not (forall ((?c Int)) (! (= (ClassReprInv (ClassRepr ?c)) ?c) :pattern ((ClassRepr ?c)) ))) (not (forall ((?T Int)) (not (= (x (typeof (ClassRepr ?T)) System_Object) true_1)))) (not (forall ((?T Int)) (not (= (ClassRepr ?T) nullObject)))) (not (forall ((?T Int) (?h_1 Int)) (! (=> (= (IsHeap ?h_1) true_1) (= (select2 ?h_1 (ClassRepr ?T) ownerFrame) PeerGroupPlaceholder)) :pattern ((select2 ?h_1 (ClassRepr ?T) ownerFrame)) ))) (not (= (IncludeInMainFrameCondition allocated) true_1)) (not (= (IncludeInMainFrameCondition elements) true_1)) (not (not (= (IncludeInMainFrameCondition inv) true_1))) (not (not (= (IncludeInMainFrameCondition localinv) true_1))) (not (= (IncludeInMainFrameCondition ownerRef) true_1)) (not (= (IncludeInMainFrameCondition ownerFrame) true_1)) (not (= (IncludeInMainFrameCondition exposeVersion) true_1)) (not (not (= (IncludeInMainFrameCondition FirstConsistentOwner) true_1))) (not (not (= (IsStaticField allocated) true_1))) (not (not (= (IsStaticField elements) true_1))) (not (not (= (IsStaticField inv) true_1))) (not (not (= (IsStaticField localinv) true_1))) (not (not (= (IsStaticField exposeVersion) true_1))) (not (not (= (IncludedInModifiesStar ownerRef) true_1))) (not (not (= (IncludedInModifiesStar ownerFrame) true_1))) (not (= (IncludedInModifiesStar exposeVersion) true_1)) (not (= (IncludedInModifiesStar elements) true_1)) (not (forall ((?A Int) (?i Int) (?x_3 Int)) (= (ValueArrayGet (ValueArraySet ?A ?i ?x_3) ?i) ?x_3))) (not (forall ((?A Int) (?i Int) (?j Int) (?x_3 Int)) (=> (not (= ?i ?j)) (= (ValueArrayGet (ValueArraySet ?A ?i ?x_3) ?j) (ValueArrayGet ?A ?j))))) (not (forall ((?A Int) (?i Int) (?x_3 Int)) (= (IntArrayGet (IntArraySet ?A ?i ?x_3) ?i) ?x_3))) (not (forall ((?A Int) (?i Int) (?j Int) (?x_3 Int)) (=> (not (= ?i ?j)) (= (IntArrayGet (IntArraySet ?A ?i ?x_3) ?j) (IntArrayGet ?A ?j))))) (not (forall ((?A Int) (?i Int) (?x_3 Int)) (= (RefArrayGet (RefArraySet ?A ?i ?x_3) ?i) ?x_3))) (not (forall ((?A Int) (?i Int) (?j Int) (?x_3 Int)) (=> (not (= ?i ?j)) (= (RefArrayGet (RefArraySet ?A ?i ?x_3) ?j) (RefArrayGet ?A ?j))))) (not (forall ((?a Int) (?d Int) (?x_3 Int) (?y Int)) (! (= (ArrayIndexInvX (ArrayIndex ?a ?d ?x_3 ?y)) ?x_3) :pattern ((ArrayIndex ?a ?d ?x_3 ?y)) ))) (not (forall ((?a Int) (?d Int) (?x_3 Int) (?y Int)) (! (= (ArrayIndexInvY (ArrayIndex ?a ?d ?x_3 ?y)) ?y) :pattern ((ArrayIndex ?a ?d ?x_3 ?y)) ))) (not (forall ((?a Int) (?i Int) (?heap_1 Int)) (! (=> (= (IsHeap ?heap_1) true_1) (= (InRange (IntArrayGet (select2 ?heap_1 ?a elements) ?i) (ElementType (typeof ?a))) true_1)) :pattern ((IntArrayGet (select2 ?heap_1 ?a elements) ?i)) ))) (not (forall ((?a Int) (?i Int) (?heap_1 Int)) (! (let ((?v_11 (RefArrayGet (select2 ?heap_1 ?a elements) ?i))) (=> (not (or (not (= (IsHeap ?heap_1) true_1)) (not (not (= ?v_11 nullObject))))) (= (x (typeof ?v_11) (ElementType (typeof ?a))) true_1))) :pattern ((typeof (RefArrayGet (select2 ?heap_1 ?a elements) ?i))) ))) (not (forall ((?a Int) (?T Int) (?i Int) (?r_1 Int) (?heap_1 Int)) (! (=> (not (or (not (= (IsHeap ?heap_1) true_1)) (not (= (x (typeof ?a) (NonNullRefArray ?T ?r_1)) true_1)))) (not (= (RefArrayGet (select2 ?heap_1 ?a elements) ?i) nullObject))) :pattern ((x (typeof ?a) (NonNullRefArray ?T ?r_1)) (RefArrayGet (select2 ?heap_1 ?a elements) ?i)) ))) (not (forall ((?a Int)) (<= 1 (Rank ?a)))) (not (forall ((?a Int) (?T Int) (?r_1 Int)) (! (=> (not (or (not (not (= ?a nullObject))) (not (= (x (typeof ?a) (RefArray ?T ?r_1)) true_1)))) (= (Rank ?a) ?r_1)) :pattern ((x (typeof ?a) (RefArray ?T ?r_1))) ))) (not (forall ((?a Int) (?T Int) (?r_1 Int)) (! (=> (not (or (not (not (= ?a nullObject))) (not (= (x (typeof ?a) (NonNullRefArray ?T ?r_1)) true_1)))) (= (Rank ?a) ?r_1)) :pattern ((x (typeof ?a) (NonNullRefArray ?T ?r_1))) ))) (not (forall ((?a Int) (?T Int) (?r_1 Int)) (! (=> (not (or (not (not (= ?a nullObject))) (not (= (x (typeof ?a) (ValueArray ?T ?r_1)) true_1)))) (= (Rank ?a) ?r_1)) :pattern ((x (typeof ?a) (ValueArray ?T ?r_1))) ))) (not (forall ((?a Int) (?T Int) (?r_1 Int)) (! (=> (not (or (not (not (= ?a nullObject))) (not (= (x (typeof ?a) (IntArray ?T ?r_1)) true_1)))) (= (Rank ?a) ?r_1)) :pattern ((x (typeof ?a) (IntArray ?T ?r_1))) ))) (not (forall ((?a Int)) (! (let ((?v_12 (Length ?a))) (not (or (not (<= 0 ?v_12)) (not (<= ?v_12 int_2147483647))))) :pattern ((Length ?a)) ))) (not (forall ((?a Int) (?i Int)) (<= 0 (DimLength ?a ?i)))) (not (forall ((?a Int)) (! (=> (= (Rank ?a) 1) (= (DimLength ?a 0) (Length ?a))) :pattern ((DimLength ?a 0)) ))) (not (forall ((?a Int) (?i Int)) (! (= (LBound ?a ?i) 0) :pattern ((LBound ?a ?i)) ))) (not (forall ((?a Int) (?i Int)) (! (= (UBound ?a ?i) (- (DimLength ?a ?i) 1)) :pattern ((UBound ?a ?i)) ))) (not (forall ((?T Int) (?ET Int) (?r_1 Int)) (! (=> (= (x ?T (ValueArray ?ET ?r_1)) true_1) (= (ArrayCategory ?T) ArrayCategoryValue)) :pattern ((x ?T (ValueArray ?ET ?r_1))) ))) (not (forall ((?T Int) (?ET Int) (?r_1 Int)) (! (=> (= (x ?T (IntArray ?ET ?r_1)) true_1) (= (ArrayCategory ?T) ArrayCategoryInt)) :pattern ((x ?T (IntArray ?ET ?r_1))) ))) (not (forall ((?T Int) (?ET Int) (?r_1 Int)) (! (=> (= (x ?T (RefArray ?ET ?r_1)) true_1) (= (ArrayCategory ?T) ArrayCategoryRef)) :pattern ((x ?T (RefArray ?ET ?r_1))) ))) (not (forall ((?T Int) (?ET Int) (?r_1 Int)) (! (=> (= (x ?T (NonNullRefArray ?ET ?r_1)) true_1) (= (ArrayCategory ?T) ArrayCategoryNonNullRef)) :pattern ((x ?T (NonNullRefArray ?ET ?r_1))) ))) (not (= (x System_Array System_Object) true_1)) (not (forall ((?T Int) (?r_1 Int)) (! (let ((?v_13 (ValueArray ?T ?r_1))) (not (or (not (= (x ?v_13 ?v_13) true_1)) (not (= (x ?v_13 System_Array) true_1))))) :pattern ((ValueArray ?T ?r_1)) ))) (not (forall ((?T Int) (?r_1 Int)) (! (let ((?v_14 (IntArray ?T ?r_1))) (not (or (not (= (x ?v_14 ?v_14) true_1)) (not (= (x ?v_14 System_Array) true_1))))) :pattern ((IntArray ?T ?r_1)) ))) (not (forall ((?T Int) (?r_1 Int)) (! (let ((?v_15 (RefArray ?T ?r_1))) (not (or (not (= (x ?v_15 ?v_15) true_1)) (not (= (x ?v_15 System_Array) true_1))))) :pattern ((RefArray ?T ?r_1)) ))) (not (forall ((?T Int) (?r_1 Int)) (! (let ((?v_16 (NonNullRefArray ?T ?r_1))) (not (or (not (= (x ?v_16 ?v_16) true_1)) (not (= (x ?v_16 System_Array) true_1))))) :pattern ((NonNullRefArray ?T ?r_1)) ))) (not (forall ((?array Int) (?elementType Int) (?rank Int)) (! (let ((?v_17 (typeof ?array))) (=> (= (NonNullRefArrayRaw ?array ?elementType ?rank) true_1) (not (or (not (= (x ?v_17 System_Array) true_1)) (not (= (Rank ?array) ?rank)) (not (= (x ?elementType (ElementType ?v_17)) true_1)))))) :pattern ((NonNullRefArrayRaw ?array ?elementType ?rank)) ))) (not (forall ((?T Int) (?U_1 Int) (?r_1 Int)) (=> (= (x ?U_1 ?T) true_1) (= (x (RefArray ?U_1 ?r_1) (RefArray ?T ?r_1)) true_1)))) (not (forall ((?T Int) (?U_1 Int) (?r_1 Int)) (=> (= (x ?U_1 ?T) true_1) (= (x (NonNullRefArray ?U_1 ?r_1) (NonNullRefArray ?T ?r_1)) true_1)))) (not (forall ((?A Int) (?r_1 Int)) (= (ElementType (ValueArray ?A ?r_1)) ?A))) (not (forall ((?A Int) (?r_1 Int)) (= (ElementType (IntArray ?A ?r_1)) ?A))) (not (forall ((?A Int) (?r_1 Int)) (= (ElementType (RefArray ?A ?r_1)) ?A))) (not (forall ((?A Int) (?r_1 Int)) (= (ElementType (NonNullRefArray ?A ?r_1)) ?A))) (not (forall ((?A Int) (?r_1 Int) (?T Int)) (! (let ((?v_18 (ElementType ?T))) (=> (= (x ?T (RefArray ?A ?r_1)) true_1) (not (or (not (not (= ?T ?A))) (not (= ?T (RefArray ?v_18 ?r_1))) (not (= (x ?v_18 ?A) true_1)))))) :pattern ((x ?T (RefArray ?A ?r_1))) ))) (not (forall ((?A Int) (?r_1 Int) (?T Int)) (! (let ((?v_19 (ElementType ?T))) (=> (= (x ?T (NonNullRefArray ?A ?r_1)) true_1) (not (or (not (not (= ?T ?A))) (not (= ?T (NonNullRefArray ?v_19 ?r_1))) (not (= (x ?v_19 ?A) true_1)))))) :pattern ((x ?T (NonNullRefArray ?A ?r_1))) ))) (not (forall ((?A Int) (?r_1 Int) (?T Int)) (! (let ((?v_20 (ValueArray ?A ?r_1))) (=> (= (x ?T ?v_20) true_1) (= ?T ?v_20))) :pattern ((x ?T (ValueArray ?A ?r_1))) ))) (not (forall ((?A Int) (?r_1 Int) (?T Int)) (! (let ((?v_21 (IntArray ?A ?r_1))) (=> (= (x ?T ?v_21) true_1) (= ?T ?v_21))) :pattern ((x ?T (IntArray ?A ?r_1))) ))) (not (forall ((?A Int) (?r_1 Int) (?T Int)) (! (let ((?v_22 (ElementType ?T))) (=> (= (x (RefArray ?A ?r_1) ?T) true_1) (or (= (x System_Array ?T) true_1) (not (or (not (= ?T (RefArray ?v_22 ?r_1))) (not (= (x ?A ?v_22) true_1))))))) :pattern ((x (RefArray ?A ?r_1) ?T)) ))) (not (forall ((?A Int) (?r_1 Int) (?T Int)) (! (let ((?v_23 (ElementType ?T))) (=> (= (x (NonNullRefArray ?A ?r_1) ?T) true_1) (or (= (x System_Array ?T) true_1) (not (or (not (= ?T (NonNullRefArray ?v_23 ?r_1))) (not (= (x ?A ?v_23) true_1))))))) :pattern ((x (NonNullRefArray ?A ?r_1) ?T)) ))) (not (forall ((?A Int) (?r_1 Int) (?T Int)) (! (let ((?v_24 (ValueArray ?A ?r_1))) (=> (= (x ?v_24 ?T) true_1) (or (= (x System_Array ?T) true_1) (= ?T ?v_24)))) :pattern ((x (ValueArray ?A ?r_1) ?T)) ))) (not (forall ((?A Int) (?r_1 Int) (?T Int)) (! (let ((?v_25 (IntArray ?A ?r_1))) (=> (= (x ?v_25 ?T) true_1) (or (= (x System_Array ?T) true_1) (= ?T ?v_25)))) :pattern ((x (IntArray ?A ?r_1) ?T)) ))) (not (forall ((?a Int) (?i Int) (?heap_1 Int)) (! (let ((?v_27 (ElementProxy ?a (- 0 1))) (?v_26 (RefArrayGet (select2 ?heap_1 ?a elements) ?i))) (=> (not (or (not (= (IsHeap ?heap_1) true_1)) (not (= (x (typeof ?a) System_Array) true_1)))) (or (= ?v_26 nullObject) (= (IsImmutable (typeof ?v_26)) true_1) (not (or (not (= (select2 ?heap_1 ?v_26 ownerRef) (select2 ?heap_1 ?v_27 ownerRef))) (not (= (select2 ?heap_1 ?v_26 ownerFrame) (select2 ?heap_1 ?v_27 ownerFrame)))))))) :pattern ((select2 ?heap_1 (RefArrayGet (select2 ?heap_1 ?a elements) ?i) ownerRef))  :pattern ((select2 ?heap_1 (RefArrayGet (select2 ?heap_1 ?a elements) ?i) ownerFrame)) ))) (not (forall ((?a Int) (?heap_1 Int)) (! (=> (not (or (not (= (IsHeap ?heap_1) true_1)) (not (= (IsAllocated ?heap_1 ?a) true_1)) (not (= (x (typeof ?a) System_Array) true_1)))) (= (IsAllocated ?heap_1 (ElementProxy ?a (- 0 1))) true_1)) :pattern ((IsAllocated ?heap_1 ?a)) ))) (not (forall ((?o Int) (?pos Int)) (! (= (typeof (ElementProxy ?o ?pos)) System_Object) :pattern ((typeof (ElementProxy ?o ?pos))) ))) (not (forall ((?o Int) (?pos Int)) (! (= (typeof (ElementProxyStruct ?o ?pos)) System_Object) :pattern ((typeof (ElementProxyStruct ?o ?pos))) ))) (not (forall ((?s Int) (?f Int) (?x_3 Int)) (= (StructGet (StructSet ?s ?f ?x_3) ?f) ?x_3))) (not (forall ((?s Int) (?f Int) (|?f'| Int) (?x_3 Int)) (=> (not (= ?f |?f'|)) (= (StructGet (StructSet ?s ?f ?x_3) |?f'|) (StructGet ?s |?f'|))))) (not (forall ((?T Int)) (! (let ((?v_28 (BaseClass ?T))) (not (or (not (= (x ?T ?v_28) true_1)) (not (=> (not (= ?T System_Object)) (not (= ?T ?v_28))))))) :pattern ((BaseClass ?T)) ))) (not (forall ((?A Int) (?B Int) (?C Int)) (! (=> (= (x ?C (AsDirectSubClass ?B ?A)) true_1) (= (OneClassDown ?C ?A) ?B)) :pattern ((x ?C (AsDirectSubClass ?B ?A))) ))) (not (forall ((?T Int)) (=> (= (IsValueType ?T) true_1) (not (or (not (forall ((?U_1 Int)) (=> (= (x ?T ?U_1) true_1) (= ?T ?U_1)))) (not (forall ((?U_1 Int)) (=> (= (x ?U_1 ?T) true_1) (= ?T ?U_1))))))))) (not (= (IsValueType System_Boolean) true_1)) (not (= (x System_Type System_Object) true_1)) (not (forall ((?T Int)) (! (= (IsNotNull (TypeObject ?T) System_Type) true_1) :pattern ((TypeObject ?T)) ))) (not (forall ((?T Int)) (! (= (TypeName (TypeObject ?T)) ?T) :pattern ((TypeObject ?T)) ))) (not (forall ((?o Int) (?T Int)) (! (= (= (Is ?o ?T) true_1) (or (= ?o nullObject) (= (x (typeof ?o) ?T) true_1))) :pattern ((Is ?o ?T)) ))) (not (forall ((?o Int) (?T Int)) (! (= (= (IsNotNull ?o ?T) true_1) (not (or (not (not (= ?o nullObject))) (not (= (Is ?o ?T) true_1))))) :pattern ((IsNotNull ?o ?T)) ))) (not (forall ((?o Int) (?T Int)) (=> (= (Is ?o ?T) true_1) (= (As ?o ?T) ?o)))) (not (forall ((?o Int) (?T Int)) (=> (not (= (Is ?o ?T) true_1)) (= (As ?o ?T) nullObject)))) (not (forall ((?h_1 Int) (?o Int)) (! (let ((?v_29 (typeof ?o))) (=> (not (or (not (= (IsHeap ?h_1) true_1)) (not (not (= ?o nullObject))) (not (= (x ?v_29 System_Array) true_1)))) (not (or (not (= (select2 ?h_1 ?o inv) ?v_29)) (not (= (select2 ?h_1 ?o localinv) ?v_29)))))) :pattern ((x (typeof ?o) System_Array) (select2 ?h_1 ?o inv)) ))) (not (forall ((?h_1 Int) (?o Int) (?f Int)) (! (=> (not (or (not (= (IsHeap ?h_1) true_1)) (not (= (select2 ?h_1 ?o allocated) true_1)))) (= (IsAllocated ?h_1 (select2 ?h_1 ?o ?f)) true_1)) :pattern ((IsAllocated ?h_1 (select2 ?h_1 ?o ?f))) ))) (not (forall ((?h_1 Int) (?o Int) (?f Int)) (! (=> (not (or (not (= (IsHeap ?h_1) true_1)) (not (= (select2 ?h_1 ?o allocated) true_1)))) (= (select2 ?h_1 (select2 ?h_1 ?o ?f) allocated) true_1)) :pattern ((select2 ?h_1 (select2 ?h_1 ?o ?f) allocated)) ))) (not (forall ((?h_1 Int) (?s Int) (?f Int)) (! (=> (= (IsAllocated ?h_1 ?s) true_1) (= (IsAllocated ?h_1 (StructGet ?s ?f)) true_1)) :pattern ((IsAllocated ?h_1 (StructGet ?s ?f))) ))) (not (forall ((?h_1 Int) (?e Int) (?i Int)) (! (=> (= (IsAllocated ?h_1 ?e) true_1) (= (IsAllocated ?h_1 (RefArrayGet ?e ?i)) true_1)) :pattern ((IsAllocated ?h_1 (RefArrayGet ?e ?i))) ))) (not (forall ((?h_1 Int) (?e Int) (?i Int)) (! (=> (= (IsAllocated ?h_1 ?e) true_1) (= (IsAllocated ?h_1 (ValueArrayGet ?e ?i)) true_1)) :pattern ((IsAllocated ?h_1 (ValueArrayGet ?e ?i))) ))) (not (forall ((?h_1 Int) (?o Int)) (! (=> (= (IsAllocated ?h_1 ?o) true_1) (= (select2 ?h_1 ?o allocated) true_1)) :pattern ((select2 ?h_1 ?o allocated)) ))) (not (forall ((?h_1 Int) (?c Int)) (! (=> (= (IsHeap ?h_1) true_1) (= (select2 ?h_1 (ClassRepr ?c) allocated) true_1)) :pattern ((select2 ?h_1 (ClassRepr ?c) allocated)) ))) (not (= (DeclType NonNullFieldsAreInitialized) System_Object)) (not (forall ((?f Int) (?T Int)) (! (=> (= (AsNonNullRefField ?f ?T) ?f) (= (AsRefField ?f ?T) ?f)) :pattern ((AsNonNullRefField ?f ?T)) ))) (not (forall ((?h_1 Int) (?o Int) (?f Int) (?T Int)) (! (=> (= (IsHeap ?h_1) true_1) (= (Is (select2 ?h_1 ?o (AsRefField ?f ?T)) ?T) true_1)) :pattern ((select2 ?h_1 ?o (AsRefField ?f ?T))) ))) (not (forall ((?h_1 Int) (?o Int) (?f Int) (?T Int)) (! (=> (not (or (not (= (IsHeap ?h_1) true_1)) (not (not (= ?o nullObject))) (not (or (not (= ?o BeingConstructed)) (= (= (select2 ?h_1 BeingConstructed NonNullFieldsAreInitialized) true_1) true))))) (not (= (select2 ?h_1 ?o (AsNonNullRefField ?f ?T)) nullObject))) :pattern ((select2 ?h_1 ?o (AsNonNullRefField ?f ?T))) ))) (not (forall ((?h_1 Int) (?o Int) (?f Int) (?T Int)) (! (=> (= (IsHeap ?h_1) true_1) (= (InRange (select2 ?h_1 ?o (AsRangeField ?f ?T)) ?T) true_1)) :pattern ((select2 ?h_1 ?o (AsRangeField ?f ?T))) ))) (not (forall ((?o Int)) (! (not (= (IsMemberlessType (typeof ?o)) true_1)) :pattern ((IsMemberlessType (typeof ?o))) ))) (not (forall ((?J Int) (?s Int) (?b Int)) (! (let ((?v_31 (AsInterface ?J)) (?v_30 (Box ?s ?b))) (=> (not (or (not (= ?v_31 ?J)) (not (= ?v_30 ?b)) (not (= (x (UnboxedType ?v_30) ?v_31) true_1)))) (= (x (typeof ?b) ?J) true_1))) :pattern ((x (UnboxedType (Box ?s ?b)) (AsInterface ?J))) ))) (not (not (= (IsImmutable System_Object) true_1))) (not (forall ((?T Int) (?U_1 Int)) (! (=> (= (x ?U_1 (AsImmutable ?T)) true_1) (not (or (not (= (IsImmutable ?U_1) true_1)) (not (= (AsImmutable ?U_1) ?U_1))))) :pattern ((x ?U_1 (AsImmutable ?T))) ))) (not (forall ((?T Int) (?U_1 Int)) (! (=> (= (x ?U_1 (AsMutable ?T)) true_1) (not (or (not (not (= (IsImmutable ?U_1) true_1))) (not (= (AsMutable ?U_1) ?U_1))))) :pattern ((x ?U_1 (AsMutable ?T))) ))) (not (forall ((?o Int) (?T Int)) (! (=> (not (or (not (not (= ?o nullObject))) (not (not (= ?o BeingConstructed))) (not (= (x (typeof ?o) (AsImmutable ?T)) true_1)))) (forall ((?h_1 Int)) (! (let ((?v_32 (typeof ?o))) (=> (= (IsHeap ?h_1) true_1) (not (or (not (= (select2 ?h_1 ?o inv) ?v_32)) (not (= (select2 ?h_1 ?o localinv) ?v_32)) (not (= (select2 ?h_1 ?o ownerFrame) PeerGroupPlaceholder)) (not (= (AsOwner ?o (select2 ?h_1 ?o ownerRef)) ?o)) (not (forall ((?t Int)) (! (=> (= (AsOwner ?o (select2 ?h_1 ?t ownerRef)) ?o) (or (= ?t ?o) (not (= (select2 ?h_1 ?t ownerFrame) PeerGroupPlaceholder)))) :pattern ((AsOwner ?o (select2 ?h_1 ?t ownerRef))) ))))))) :pattern ((IsHeap ?h_1)) ))) :pattern ((x (typeof ?o) (AsImmutable ?T))) ))) (not (forall ((?s Int)) (! (<= 0 (StringLength ?s)) :pattern ((StringLength ?s)) ))) (not (forall ((?h_1 Int) (?o Int) (?f Int) (?T Int)) (! (let ((?v_33 (select2 ?h_1 ?o (AsRepField ?f ?T)))) (=> (not (or (not (= (IsHeap ?h_1) true_1)) (not (not (= ?v_33 nullObject))))) (not (or (not (= (select2 ?h_1 ?v_33 ownerRef) ?o)) (not (= (select2 ?h_1 ?v_33 ownerFrame) ?T)))))) :pattern ((select2 ?h_1 ?o (AsRepField ?f ?T))) ))) (not (forall ((?h_1 Int) (?o Int) (?f Int)) (! (let ((?v_34 (select2 ?h_1 ?o (AsPeerField ?f)))) (=> (not (or (not (= (IsHeap ?h_1) true_1)) (not (not (= ?v_34 nullObject))))) (not (or (not (= (select2 ?h_1 ?v_34 ownerRef) (select2 ?h_1 ?o ownerRef))) (not (= (select2 ?h_1 ?v_34 ownerFrame) (select2 ?h_1 ?o ownerFrame))))))) :pattern ((select2 ?h_1 ?o (AsPeerField ?f))) ))) (not (forall ((?h_1 Int) (?o Int) (?f Int) (?T Int) (?i Int)) (! (let ((?v_35 (select2 ?h_1 ?o (AsElementsRepField ?f ?T ?i)))) (let ((?v_36 (ElementProxy ?v_35 ?i))) (=> (not (or (not (= (IsHeap ?h_1) true_1)) (not (not (= ?v_35 nullObject))))) (not (or (not (= (select2 ?h_1 ?v_36 ownerRef) ?o)) (not (= (select2 ?h_1 ?v_36 ownerFrame) ?T))))))) :pattern ((select2 ?h_1 ?o (AsElementsRepField ?f ?T ?i))) ))) (not (forall ((?h_1 Int) (?o Int) (?f Int) (?i Int)) (! (let ((?v_37 (select2 ?h_1 ?o (AsElementsPeerField ?f ?i)))) (let ((?v_38 (ElementProxy ?v_37 ?i))) (=> (not (or (not (= (IsHeap ?h_1) true_1)) (not (not (= ?v_37 nullObject))))) (not (or (not (= (select2 ?h_1 ?v_38 ownerRef) (select2 ?h_1 ?o ownerRef))) (not (= (select2 ?h_1 ?v_38 ownerFrame) (select2 ?h_1 ?o ownerFrame)))))))) :pattern ((select2 ?h_1 ?o (AsElementsPeerField ?f ?i))) ))) (not (forall ((?h_1 Int) (?o Int)) (! (let ((?v_41 (typeof ?o)) (?v_39 (select2 ?h_1 ?o ownerFrame)) (?v_40 (select2 ?h_1 ?o ownerRef))) (=> (not (or (not (= (IsHeap ?h_1) true_1)) (not (not (= ?v_39 PeerGroupPlaceholder))) (not (= (x (select2 ?h_1 ?v_40 inv) ?v_39) true_1)) (not (not (= (select2 ?h_1 ?v_40 localinv) (BaseClass ?v_39)))))) (not (or (not (= (select2 ?h_1 ?o inv) ?v_41)) (not (= (select2 ?h_1 ?o localinv) ?v_41)))))) :pattern ((x (select2 ?h_1 (select2 ?h_1 ?o ownerRef) inv) (select2 ?h_1 ?o ownerFrame))) ))) (not (forall ((?o Int) (?f Int) (?h_1 Int)) (! (let ((?v_42 (select2 ?h_1 ?o ownerFrame)) (?v_43 (select2 ?h_1 ?o ownerRef))) (=> (not (or (not (= (IsHeap ?h_1) true_1)) (not (not (= ?o nullObject))) (not (= (= (select2 ?h_1 ?o allocated) true_1) true)) (not (= (AsPureObject ?o) ?o)) (not (not (= ?v_42 PeerGroupPlaceholder))) (not (= (x (select2 ?h_1 ?v_43 inv) ?v_42) true_1)) (not (not (= (select2 ?h_1 ?v_43 localinv) (BaseClass ?v_42)))))) (= (select2 ?h_1 ?o ?f) (FieldDependsOnFCO ?o ?f (select2 ?h_1 (select2 ?h_1 ?o FirstConsistentOwner) exposeVersion))))) :pattern ((select2 ?h_1 (AsPureObject ?o) ?f)) ))) (not (forall ((?o Int) (?h_1 Int)) (! (let ((?v_46 (select2 ?h_1 ?o FirstConsistentOwner))) (let ((?v_47 (select2 ?h_1 ?v_46 ownerFrame)) (?v_48 (select2 ?h_1 ?v_46 ownerRef)) (?v_44 (select2 ?h_1 ?o ownerFrame)) (?v_45 (select2 ?h_1 ?o ownerRef))) (=> (not (or (not (= (IsHeap ?h_1) true_1)) (not (not (= ?o nullObject))) (not (= (= (select2 ?h_1 ?o allocated) true_1) true)) (not (not (= ?v_44 PeerGroupPlaceholder))) (not (= (x (select2 ?h_1 ?v_45 inv) ?v_44) true_1)) (not (not (= (select2 ?h_1 ?v_45 localinv) (BaseClass ?v_44)))))) (not (or (not (not (= ?v_46 nullObject))) (not (= (= (select2 ?h_1 ?v_46 allocated) true_1) true)) (not (or (= ?v_47 PeerGroupPlaceholder) (not (= (x (select2 ?h_1 ?v_48 inv) ?v_47) true_1)) (= (select2 ?h_1 ?v_48 localinv) (BaseClass ?v_47))))))))) :pattern ((select2 ?h_1 ?o FirstConsistentOwner)) ))) (not (forall ((?value Int) (?typ Int) (?occurrence Int) (?activity Int)) (! (let ((?v_49 (BoxFunc ?value ?typ ?occurrence ?activity))) (not (or (not (= (Box ?value ?v_49) ?v_49)) (not (= (UnboxedType ?v_49) ?typ))))) :pattern ((BoxFunc ?value ?typ ?occurrence ?activity)) ))) (not (forall ((?x_3 Int) (?typ Int) (?occurrence Int) (?activity Int)) (=> (not (= (IsValueType (UnboxedType ?x_3)) true_1)) (= (BoxFunc ?x_3 ?typ ?occurrence ?activity) ?x_3)))) (not (forall ((?x_3 Int) (?p Int)) (! (= (Unbox (Box ?x_3 ?p)) ?x_3) :pattern ((Unbox (Box ?x_3 ?p))) ))) (not (forall ((?p Int)) (! (=> (= (IsValueType (UnboxedType ?p)) true_1) (forall ((?heap_1 Int) (?x_3 Int)) (! (let ((?v_50 (Box ?x_3 ?p))) (let ((?v_51 (typeof ?v_50))) (=> (= (IsHeap ?heap_1) true_1) (not (or (not (= (select2 ?heap_1 ?v_50 inv) ?v_51)) (not (= (select2 ?heap_1 ?v_50 localinv) ?v_51))))))) :pattern ((select2 ?heap_1 (Box ?x_3 ?p) inv)) ))) :pattern ((IsValueType (UnboxedType ?p))) ))) (not (forall ((?x_3 Int) (?p Int)) (! (let ((?v_52 (Box ?x_3 ?p))) (=> (not (or (not (= (x (UnboxedType ?v_52) System_Object) true_1)) (not (= ?v_52 ?p)))) (= ?x_3 ?p))) :pattern ((x (UnboxedType (Box ?x_3 ?p)) System_Object)) ))) (not (forall ((?p Int) (?typ Int)) (! (= (= (UnboxedType ?p) ?typ) (not (= (BoxTester ?p ?typ) nullObject))) :pattern ((BoxTester ?p ?typ)) ))) (not (forall ((?p Int) (?typ Int)) (! (=> (not (= (BoxTester ?p ?typ) nullObject)) (= (Box (Unbox ?p) ?p) ?p)) :pattern ((BoxTester ?p ?typ)) ))) (not (= (IsValueType System_SByte) true_1)) (not (= (IsValueType System_Byte) true_1)) (not (= (IsValueType System_Int16) true_1)) (not (= (IsValueType System_UInt16) true_1)) (not (= (IsValueType System_Int32) true_1)) (not (= (IsValueType System_UInt32) true_1)) (not (= (IsValueType System_Int64) true_1)) (not (= (IsValueType System_UInt64) true_1)) (not (= (IsValueType System_Char) true_1)) (not (= (IsValueType System_UIntPtr) true_1)) (not (= (IsValueType System_IntPtr) true_1)) (not (< int_m9223372036854775808 int_m2147483648)) (not (< int_m2147483648 (- 0 100000))) (not (< 100000 int_2147483647)) (not (< int_2147483647 int_4294967295)) (not (< int_4294967295 int_9223372036854775807)) (not (< int_9223372036854775807 int_18446744073709551615)) (not (= (+ int_m9223372036854775808 1) (- 0 int_9223372036854775807))) (not (= (+ int_m2147483648 1) (- 0 int_2147483647))) (not (forall ((?i Int)) (= (= (InRange ?i System_SByte) true_1) (not (or (not (<= (- 0 128) ?i)) (not (< ?i 128))))))) (not (forall ((?i Int)) (= (= (InRange ?i System_Byte) true_1) (not (or (not (<= 0 ?i)) (not (< ?i 256))))))) (not (forall ((?i Int)) (= (= (InRange ?i System_Int16) true_1) (not (or (not (<= (- 0 32768) ?i)) (not (< ?i 32768))))))) (not (forall ((?i Int)) (= (= (InRange ?i System_UInt16) true_1) (not (or (not (<= 0 ?i)) (not (< ?i 65536))))))) (not (forall ((?i Int)) (= (= (InRange ?i System_Int32) true_1) (not (or (not (<= int_m2147483648 ?i)) (not (<= ?i int_2147483647))))))) (not (forall ((?i Int)) (= (= (InRange ?i System_UInt32) true_1) (not (or (not (<= 0 ?i)) (not (<= ?i int_4294967295))))))) (not (forall ((?i Int)) (= (= (InRange ?i System_Int64) true_1) (not (or (not (<= int_m9223372036854775808 ?i)) (not (<= ?i int_9223372036854775807))))))) (not (forall ((?i Int)) (= (= (InRange ?i System_UInt64) true_1) (not (or (not (<= 0 ?i)) (not (<= ?i int_18446744073709551615))))))) (not (forall ((?i Int)) (= (= (InRange ?i System_Char) true_1) (not (or (not (<= 0 ?i)) (not (< ?i 65536))))))) (not (forall ((?z Int) (?B Int) (?C Int)) (=> (= (InRange ?z ?C) true_1) (= (IntToInt ?z ?B ?C) ?z)))) (not (forall ((?b Int) (?x_3 Int) (?y Int)) (! (=> (= ?b true_1) (= (IfThenElse ?b ?x_3 ?y) ?x_3)) :pattern ((IfThenElse ?b ?x_3 ?y)) ))) (not (forall ((?b Int) (?x_3 Int) (?y Int)) (! (=> (not (= ?b true_1)) (= (IfThenElse ?b ?x_3 ?y) ?y)) :pattern ((IfThenElse ?b ?x_3 ?y)) ))) (not (forall ((?x_3 Int) (?y Int)) (! (= (x_1 ?x_3 ?y) (- ?x_3 (* (x_2 ?x_3 ?y) ?y))) :pattern ((x_1 ?x_3 ?y))  :pattern ((x_2 ?x_3 ?y)) ))) (not (forall ((?x_3 Int) (?y Int)) (! (let ((?v_53 (x_1 ?x_3 ?y))) (=> (not (or (not (<= 0 ?x_3)) (not (< 0 ?y)))) (not (or (not (<= 0 ?v_53)) (not (< ?v_53 ?y)))))) :pattern ((x_1 ?x_3 ?y)) ))) (not (forall ((?x_3 Int) (?y Int)) (! (let ((?v_54 (x_1 ?x_3 ?y))) (=> (not (or (not (<= 0 ?x_3)) (not (< ?y 0)))) (not (or (not (<= 0 ?v_54)) (not (< ?v_54 (- 0 ?y))))))) :pattern ((x_1 ?x_3 ?y)) ))) (not (forall ((?x_3 Int) (?y Int)) (! (let ((?v_55 (x_1 ?x_3 ?y))) (=> (not (or (not (<= ?x_3 0)) (not (< 0 ?y)))) (not (or (not (< (- 0 ?y) ?v_55)) (not (<= ?v_55 0)))))) :pattern ((x_1 ?x_3 ?y)) ))) (not (forall ((?x_3 Int) (?y Int)) (! (let ((?v_56 (x_1 ?x_3 ?y))) (=> (not (or (not (<= ?x_3 0)) (not (< ?y 0)))) (not (or (not (< ?y ?v_56)) (not (<= ?v_56 0)))))) :pattern ((x_1 ?x_3 ?y)) ))) (not (forall ((?x_3 Int) (?y Int)) (! (=> (not (or (not (<= 0 ?x_3)) (not (<= 0 ?y)))) (= (x_1 (+ ?x_3 ?y) ?y) (x_1 ?x_3 ?y))) :pattern ((x_1 (+ ?x_3 ?y) ?y)) ))) (not (forall ((?x_3 Int) (?y Int)) (! (=> (not (or (not (<= 0 ?x_3)) (not (<= 0 ?y)))) (= (x_1 (+ ?y ?x_3) ?y) (x_1 ?x_3 ?y))) :pattern ((x_1 (+ ?y ?x_3) ?y)) ))) (not (forall ((?x_3 Int) (?y Int)) (! (let ((?v_57 (- ?x_3 ?y))) (=> (not (or (not (<= 0 ?v_57)) (not (<= 0 ?y)))) (= (x_1 ?v_57 ?y) (x_1 ?x_3 ?y)))) :pattern ((x_1 (- ?x_3 ?y) ?y)) ))) (not (forall ((?a Int) (?b Int) (?d Int)) (! (=> (not (or (not (<= 2 ?d)) (not (= (x_1 ?a ?d) (x_1 ?b ?d))) (not (< ?a ?b)))) (<= (+ ?a ?d) ?b)) :pattern ((x_1 ?a ?d) (x_1 ?b ?d)) ))) (not (forall ((?x_3 Int) (?y Int)) (! (=> (or (<= 0 ?x_3) (<= 0 ?y)) (<= 0 (and_1 ?x_3 ?y))) :pattern ((and_1 ?x_3 ?y)) ))) (not (forall ((?x_3 Int) (?y Int)) (! (let ((?v_58 (or_1 ?x_3 ?y))) (=> (not (or (not (<= 0 ?x_3)) (not (<= 0 ?y)))) (not (or (not (<= 0 ?v_58)) (not (<= ?v_58 (+ ?x_3 ?y))))))) :pattern ((or_1 ?x_3 ?y)) ))) (not (forall ((?i Int)) (! (= (shl ?i 0) ?i) :pattern ((shl ?i 0)) ))) (not (forall ((?i Int) (?j Int)) (! (=> (<= 1 ?j) (= (shl ?i ?j) (* (shl ?i (- ?j 1)) 2))) :pattern ((shl ?i ?j)) ))) (not (forall ((?i Int) (?j Int)) (! (let ((?v_59 (shl ?i ?j))) (=> (not (or (not (<= 0 ?i)) (not (< ?i 32768)) (not (<= 0 ?j)) (not (<= ?j 16)))) (not (or (not (<= 0 ?v_59)) (not (<= ?v_59 int_2147483647)))))) :pattern ((shl ?i ?j)) ))) (not (forall ((?i Int)) (! (= (shr ?i 0) ?i) :pattern ((shr ?i 0)) ))) (not (forall ((?i Int) (?j Int)) (! (=> (<= 1 ?j) (= (shr ?i ?j) (x_2 (shr ?i (- ?j 1)) 2))) :pattern ((shr ?i ?j)) ))) (not (forall ((?x_3 Int) (?y Int)) (! (let ((?v_60 (min ?x_3 ?y))) (not (or (not (or (= ?v_60 ?x_3) (= ?v_60 ?y))) (not (<= ?v_60 ?x_3)) (not (<= ?v_60 ?y))))) :pattern ((min ?x_3 ?y)) ))) (not (forall ((?x_3 Int) (?y Int)) (! (let ((?v_61 (max ?x_3 ?y))) (not (or (not (or (= ?v_61 ?x_3) (= ?v_61 ?y))) (not (<= ?x_3 ?v_61)) (not (<= ?y ?v_61))))) :pattern ((max ?x_3 ?y)) ))) (not (forall ((?h_1 Int) (?a Int) (?b Int)) (! (= (= (System_String_Equals_System_String ?h_1 ?a ?b) true_1) (= (System_String_Equals_System_String_System_String ?h_1 ?a ?b) true_1)) :pattern ((System_String_Equals_System_String ?h_1 ?a ?b)) ))) (not (forall ((?h_1 Int) (?a Int) (?b Int)) (! (let ((?v_63 (= (StringEquals ?a ?b) true_1)) (?v_62 (= (System_String_Equals_System_String_System_String ?h_1 ?a ?b) true_1))) (not (or (not (= ?v_62 ?v_63)) (not (= ?v_62 (= (StringEquals ?b ?a) true_1))) (not (=> (= ?a ?b) ?v_63))))) :pattern ((System_String_Equals_System_String_System_String ?h_1 ?a ?b)) ))) (not (forall ((?a Int) (?b Int) (?c Int)) (=> (not (or (not (= (StringEquals ?a ?b) true_1)) (not (= (StringEquals ?b ?c) true_1)))) (= (StringEquals ?a ?c) true_1)))) (not (forall ((?h_1 Int) (?a Int) (?b Int)) (! (=> (not (or (not (not (= ?a nullObject))) (not (not (= ?b nullObject))) (not (= (System_String_Equals_System_String_System_String ?h_1 ?a ?b) true_1)))) (= (System_String_IsInterned_System_String_notnull ?h_1 ?a) (System_String_IsInterned_System_String_notnull ?h_1 ?b))) :pattern ((System_String_Equals_System_String_System_String ?h_1 ?a ?b)) ))) (not (not (= (IsStaticField Memory_contents) true_1))) (not (= (IncludeInMainFrameCondition Memory_contents) true_1)) (not (= (IncludedInModifiesStar Memory_contents) true_1)) (not (= (AsRepField Memory_contents Memory) Memory_contents)) (not (= (DeclType Memory_contents) Memory)) (not (= (AsNonNullRefField Memory_contents (IntArray System_Byte 1)) Memory_contents)) (not (forall ((?heap Int) (?r Int)) (! (=> (= (IsHeap ?heap) true_1) (= (select2 ?heap ?r Memory_contents) (Memory_contents_1 ?r))) :pattern ((select2 ?heap ?r Memory_contents)) ))) (not (not (= (IsStaticField RTE_Data) true_1))) (not (= (IncludeInMainFrameCondition RTE_Data) true_1)) (not (= (IncludedInModifiesStar RTE_Data) true_1)) (not (= (AsRepField RTE_Data RTE) RTE_Data)) (not (= (DeclType RTE_Data) RTE)) (not (= (AsNonNullRefField RTE_Data Memory) RTE_Data)) (not (not (= (IsStaticField RTE_CallStack) true_1))) (not (= (IncludeInMainFrameCondition RTE_CallStack) true_1)) (not (= (IncludedInModifiesStar RTE_CallStack) true_1)) (not (= (AsRepField RTE_CallStack RTE) RTE_CallStack)) (not (= (DeclType RTE_CallStack) RTE)) (not (= (AsNonNullRefField RTE_CallStack ?v_0) RTE_CallStack)) (not (not (= (IsStaticField RTE_CSP) true_1))) (not (= (IncludeInMainFrameCondition RTE_CSP) true_1)) (not (= (IncludedInModifiesStar RTE_CSP) true_1)) (not (= (DeclType RTE_CSP) RTE)) (not (= (AsRangeField RTE_CSP System_Int32) RTE_CSP)) (not (not (= (IsStaticField RTE_MStackBase) true_1))) (not (= (IncludeInMainFrameCondition RTE_MStackBase) true_1)) (not (= (IncludedInModifiesStar RTE_MStackBase) true_1)) (not (= (DeclType RTE_MStackBase) RTE)) (not (= (AsRangeField RTE_MStackBase System_Int32) RTE_MStackBase)) (not (forall ((?heap Int) (?r Int)) (! (=> (= (IsHeap ?heap) true_1) (= (select2 ?heap ?r RTE_MStackBase) (RTE_MStackBase_1 ?r))) :pattern ((select2 ?heap ?r RTE_MStackBase)) ))) (not (not (= (IsStaticField RTE_MSP) true_1))) (not (= (IncludeInMainFrameCondition RTE_MSP) true_1)) (not (= (IncludedInModifiesStar RTE_MSP) true_1)) (not (= (DeclType RTE_MSP) RTE)) (not (= (AsRangeField RTE_MSP System_Int32) RTE_MSP)) (not (not (= (IsStaticField RTE_MStackMaxSize) true_1))) (not (= (IncludeInMainFrameCondition RTE_MStackMaxSize) true_1)) (not (= (IncludedInModifiesStar RTE_MStackMaxSize) true_1)) (not (= (DeclType RTE_MStackMaxSize) RTE)) (not (= (AsRangeField RTE_MStackMaxSize System_Int32) RTE_MStackMaxSize)) (not (forall ((?heap Int) (?r Int)) (! (=> (= (IsHeap ?heap) true_1) (= (select2 ?heap ?r RTE_MStackMaxSize) (RTE_MStackMaxSize_1 ?r))) :pattern ((select2 ?heap ?r RTE_MStackMaxSize)) ))) (not (not (= (IsStaticField RTE_Scratch) true_1))) (not (= (IncludeInMainFrameCondition RTE_Scratch) true_1)) (not (= (IncludedInModifiesStar RTE_Scratch) true_1)) (not (= (AsRepField RTE_Scratch RTE) RTE_Scratch)) (not (= (DeclType RTE_Scratch) RTE)) (not (= (AsNonNullRefField RTE_Scratch Memory) RTE_Scratch)) (not (not (= (IsStaticField RTE_DPP) true_1))) (not (= (IncludeInMainFrameCondition RTE_DPP) true_1)) (not (= (IncludedInModifiesStar RTE_DPP) true_1)) (not (= (DeclType RTE_DPP) RTE)) (not (= (AsRangeField RTE_DPP System_Int32) RTE_DPP)) (not (not (= (IsStaticField RTE_A) true_1))) (not (= (IncludeInMainFrameCondition RTE_A) true_1)) (not (= (IncludedInModifiesStar RTE_A) true_1)) (not (= (DeclType RTE_A) RTE)) (not (= (AsRangeField RTE_A System_Int32) RTE_A)) (not (not (= (IsStaticField RTE_Z) true_1))) (not (= (IncludeInMainFrameCondition RTE_Z) true_1)) (not (= (IncludedInModifiesStar RTE_Z) true_1)) (not (= (DeclType RTE_Z) RTE)) (not (not (= (IsStaticField RTE_C) true_1))) (not (= (IncludeInMainFrameCondition RTE_C) true_1)) (not (= (IncludedInModifiesStar RTE_C) true_1)) (not (= (DeclType RTE_C) RTE)) (not (not (= (IsStaticField RTE_PC) true_1))) (not (= (IncludeInMainFrameCondition RTE_PC) true_1)) (not (= (IncludedInModifiesStar RTE_PC) true_1)) (not (= (DeclType RTE_PC) RTE)) (not (= (AsRangeField RTE_PC System_Int32) RTE_PC)) (not (not (= (IsStaticField RTE_CurrRTEMode) true_1))) (not (= (IncludeInMainFrameCondition RTE_CurrRTEMode) true_1)) (not (= (IncludedInModifiesStar RTE_CurrRTEMode) true_1)) (not (= (DeclType RTE_CurrRTEMode) RTE)) (not (= (AsRangeField RTE_CurrRTEMode System_Int32) RTE_CurrRTEMode)) (not (not (= (IsStaticField RTE_RtnCode) true_1))) (not (= (IncludeInMainFrameCondition RTE_RtnCode) true_1)) (not (= (IncludedInModifiesStar RTE_RtnCode) true_1)) (not (= (DeclType RTE_RtnCode) RTE)) (not (= (AsRangeField RTE_RtnCode System_Int32) RTE_RtnCode)) (not (not (= (IsStaticField RTE_Program) true_1))) (not (= (IncludeInMainFrameCondition RTE_Program) true_1)) (not (= (IncludedInModifiesStar RTE_Program) true_1)) (not (= (AsRepField RTE_Program RTE) RTE_Program)) (not (= (DeclType RTE_Program) RTE)) (not (= (AsNonNullRefField RTE_Program Memory) RTE_Program)) (not (not (= (IsStaticField RTE_Instructions) true_1))) (not (= (IncludeInMainFrameCondition RTE_Instructions) true_1)) (not (= (IncludedInModifiesStar RTE_Instructions) true_1)) (not (= (AsRepField RTE_Instructions RTE) RTE_Instructions)) (not (= (DeclType RTE_Instructions) RTE)) (not (= (AsNonNullRefField RTE_Instructions ?v_0) RTE_Instructions)) (not (= (x Memory Memory) true_1)) (not (= ?v_1 System_Object)) (not (= (AsDirectSubClass Memory ?v_1) Memory)) (not (not (= (IsImmutable Memory) true_1))) (not (= (AsMutable Memory) Memory)) (not (forall ((?oi Int) (?h Int)) (! (=> (not (or (not (= (IsHeap ?h) true_1)) (not (= (x (select2 ?h ?oi inv) Memory) true_1)) (not (not (= (select2 ?h ?oi localinv) ?v_1))))) true) :pattern ((x (select2 ?h ?oi inv) Memory)) ))) (not (= (x System_Array System_Array) true_1)) (not (= ?v_2 System_Object)) (not (= (AsDirectSubClass System_Array ?v_2) System_Array)) (not (not (= (IsImmutable System_Array) true_1))) (not (= (AsMutable System_Array) System_Array)) (not (= (x System_ICloneable System_ICloneable) true_1)) (not (= (x System_ICloneable System_Object) true_1)) (not (= (IsMemberlessType System_ICloneable) true_1)) (not (= (AsInterface System_ICloneable) System_ICloneable)) (not (= (x System_Array System_ICloneable) true_1)) (not (= (x System_Collections_IList System_Collections_IList) true_1)) (not (= (x System_Collections_IList System_Object) true_1)) (not (= (x System_Collections_ICollection System_Collections_ICollection) true_1)) (not (= (x System_Collections_ICollection System_Object) true_1)) (not (= (x System_Collections_IEnumerable System_Collections_IEnumerable) true_1)) (not (= (x System_Collections_IEnumerable System_Object) true_1)) (not (= (IsMemberlessType System_Collections_IEnumerable) true_1)) (not (= (AsInterface System_Collections_IEnumerable) System_Collections_IEnumerable)) (not (= (x System_Collections_ICollection System_Collections_IEnumerable) true_1)) (not (= (IsMemberlessType System_Collections_ICollection) true_1)) (not (= (AsInterface System_Collections_ICollection) System_Collections_ICollection)) (not (= (x System_Collections_IList System_Collections_ICollection) true_1)) (not (= (x System_Collections_IList System_Collections_IEnumerable) true_1)) (not (= (IsMemberlessType System_Collections_IList) true_1)) (not (= (AsInterface System_Collections_IList) System_Collections_IList)) (not (= (x System_Array System_Collections_IList) true_1)) (not (= (x System_Array System_Collections_ICollection) true_1)) (not (= (x System_Array System_Collections_IEnumerable) true_1)) (not (= (IsMemberlessType System_Array) true_1)) (not (forall ((?oi Int) (?h Int)) (! (=> (not (or (not (= (IsHeap ?h) true_1)) (not (= (x (select2 ?h ?oi inv) System_Array) true_1)) (not (not (= (select2 ?h ?oi localinv) ?v_2))))) true) :pattern ((x (select2 ?h ?oi inv) System_Array)) ))) (not (=> ?v_5 (forall ((?Heap Int) (?this Int) (?addr_in Int)) (! (let ((?v_65 (select2 ?Heap ?this ownerRef)) (?v_67 (select2 ?Heap ?this FirstConsistentOwner)) (?v_64 (select2 ?Heap ?this ownerFrame))) (let ((?v_66 (not (or (not (= (x (select2 ?Heap ?v_65 inv) ?v_64) true_1)) (not (not (= (select2 ?Heap ?v_65 localinv) (BaseClass ?v_64)))))))) (=> (not (or (not (= (IsHeap ?Heap) true_1)) (not (= (IsNotNull ?this Memory) true_1)) (not (= (select2 ?Heap ?this allocated) true_1)) (not (<= 0 ?addr_in)) (not (< ?addr_in (Length (select2 ?Heap ?this Memory_contents)))) (not (forall ((?pc Int)) (! (let ((?v_68 (typeof ?pc))) (=> (not (or (not (not (= ?pc nullObject))) (not (= (select2 ?Heap ?pc allocated) true_1)) (not (= (select2 ?Heap ?pc ownerRef) ?v_65)) (not (= (select2 ?Heap ?pc ownerFrame) ?v_64)))) (not (or (not (= (select2 ?Heap ?pc inv) ?v_68)) (not (= (select2 ?Heap ?pc localinv) ?v_68)))))) :pattern ((typeof ?pc))  :pattern ((select2 ?Heap ?pc localinv))  :pattern ((select2 ?Heap ?pc inv))  :pattern ((select2 ?Heap ?pc ownerFrame))  :pattern ((select2 ?Heap ?pc ownerRef)) ))))) (not (or (not (=> (not (= ?v_64 PeerGroupPlaceholder)) (not (or (not (=> ?v_66 (= ?v_67 ?v_65))) (not (=> (not ?v_66) (= ?v_67 (select2 ?Heap ?v_65 FirstConsistentOwner)))))))) (not (= (AsPureObject ?this) ?this))))))) :pattern ((Memory_get_cont_System_Int32 ?Heap ?this ?addr_in)) )))) (not (forall ((?Heap Int) (?this Int) (?addr_in Int)) (! (let ((?v_69 (typeof ?this))) (=> (not (or (not (not (= ?this nullObject))) (not (= (x ?v_69 Memory) true_1)) (not (= (select2 ?Heap ?this inv) ?v_69)) (not (= (select2 ?Heap ?this localinv) ?v_69)) (not (= (IsHeap ?Heap) true_1)) (not (= (select2 ?Heap ?this allocated) true_1)))) (= (Memory_get_cont_System_Int32 ?Heap ?this ?addr_in) (Memory_get_cont_System_Int32_1 (select2 ?Heap ?this exposeVersion) ?addr_in)))) :pattern ((Memory_get_cont_System_Int32 ?Heap ?this ?addr_in)) ))) (not (= (x System_Type System_Type) true_1)) (not (= (x System_Reflection_MemberInfo System_Reflection_MemberInfo) true_1)) (not (= ?v_3 System_Object)) (not (= (AsDirectSubClass System_Reflection_MemberInfo ?v_3) System_Reflection_MemberInfo)) (not (= (IsImmutable System_Reflection_MemberInfo) true_1)) (not (= (AsImmutable System_Reflection_MemberInfo) System_Reflection_MemberInfo)) (not (= (x System_Reflection_ICustomAttributeProvider System_Reflection_ICustomAttributeProvider) true_1)) (not (= (x System_Reflection_ICustomAttributeProvider System_Object) true_1)) (not (= (IsMemberlessType System_Reflection_ICustomAttributeProvider) true_1)) (not (= (AsInterface System_Reflection_ICustomAttributeProvider) System_Reflection_ICustomAttributeProvider)) (not (= (x System_Reflection_MemberInfo System_Reflection_ICustomAttributeProvider) true_1)) (not (= (x System_Runtime_InteropServices__MemberInfo System_Runtime_InteropServices__MemberInfo) true_1)) (not (= (x System_Runtime_InteropServices__MemberInfo System_Object) true_1)) (not (= (IsMemberlessType System_Runtime_InteropServices__MemberInfo) true_1)) (not (= (AsInterface System_Runtime_InteropServices__MemberInfo) System_Runtime_InteropServices__MemberInfo)) (not (= (x System_Reflection_MemberInfo System_Runtime_InteropServices__MemberInfo) true_1)) (not (= (IsMemberlessType System_Reflection_MemberInfo) true_1)) (not (forall ((?oi Int) (?h Int)) (! (=> (not (or (not (= (IsHeap ?h) true_1)) (not (= (x (select2 ?h ?oi inv) System_Reflection_MemberInfo) true_1)) (not (not (= (select2 ?h ?oi localinv) ?v_3))))) true) :pattern ((x (select2 ?h ?oi inv) System_Reflection_MemberInfo)) ))) (not (= ?v_4 System_Reflection_MemberInfo)) (not (= (AsDirectSubClass System_Type ?v_4) System_Type)) (not (= (IsImmutable System_Type) true_1)) (not (= (AsImmutable System_Type) System_Type)) (not (= (x System_Runtime_InteropServices__Type System_Runtime_InteropServices__Type) true_1)) (not (= (x System_Runtime_InteropServices__Type System_Object) true_1)) (not (= (IsMemberlessType System_Runtime_InteropServices__Type) true_1)) (not (= (AsInterface System_Runtime_InteropServices__Type) System_Runtime_InteropServices__Type)) (not (= (x System_Type System_Runtime_InteropServices__Type) true_1)) (not (= (x System_Reflection_IReflect System_Reflection_IReflect) true_1)) (not (= (x System_Reflection_IReflect System_Object) true_1)) (not (= (IsMemberlessType System_Reflection_IReflect) true_1)) (not (= (AsInterface System_Reflection_IReflect) System_Reflection_IReflect)) (not (= (x System_Type System_Reflection_IReflect) true_1)) (not (= (IsMemberlessType System_Type) true_1)) (not (forall ((?oi Int) (?h Int)) (! (=> (not (or (not (= (IsHeap ?h) true_1)) (not (= (x (select2 ?h ?oi inv) System_Type) true_1)) (not (not (= (select2 ?h ?oi localinv) ?v_4))))) true) :pattern ((x (select2 ?h ?oi inv) System_Type)) ))) (not (=> ?v_5 (forall ((?Heap Int) (?this Int) (?addr_in Int)) (! (let ((?v_71 (select2 ?Heap ?this ownerRef)) (?v_73 (select2 ?Heap ?this FirstConsistentOwner)) (?v_70 (select2 ?Heap ?this ownerFrame))) (let ((?v_72 (not (or (not (= (x (select2 ?Heap ?v_71 inv) ?v_70) true_1)) (not (not (= (select2 ?Heap ?v_71 localinv) (BaseClass ?v_70)))))))) (=> (not (or (not (= (IsHeap ?Heap) true_1)) (not (= (IsNotNull ?this Memory) true_1)) (not (= (select2 ?Heap ?this allocated) true_1)) (not (forall ((?pc Int)) (! (let ((?v_74 (typeof ?pc))) (=> (not (or (not (not (= ?pc nullObject))) (not (= (select2 ?Heap ?pc allocated) true_1)) (not (= (select2 ?Heap ?pc ownerRef) ?v_71)) (not (= (select2 ?Heap ?pc ownerFrame) ?v_70)))) (not (or (not (= (select2 ?Heap ?pc inv) ?v_74)) (not (= (select2 ?Heap ?pc localinv) ?v_74)))))) :pattern ((typeof ?pc))  :pattern ((select2 ?Heap ?pc localinv))  :pattern ((select2 ?Heap ?pc inv))  :pattern ((select2 ?Heap ?pc ownerFrame))  :pattern ((select2 ?Heap ?pc ownerRef)) ))))) (not (or (not (=> (= (Memory_InSandbox_System_Int32 ?Heap ?this ?addr_in) true_1) (not (or (not (<= 0 ?addr_in)) (not (< ?addr_in (Length (select2 ?Heap ?this Memory_contents)))))))) (not (=> (not (= ?v_70 PeerGroupPlaceholder)) (not (or (not (=> ?v_72 (= ?v_73 ?v_71))) (not (=> (not ?v_72) (= ?v_73 (select2 ?Heap ?v_71 FirstConsistentOwner)))))))) (not (= (AsPureObject ?this) ?this))))))) :pattern ((Memory_InSandbox_System_Int32 ?Heap ?this ?addr_in)) )))) (not (forall ((?Heap Int) (?this Int) (?addr_in Int)) (! (let ((?v_75 (typeof ?this))) (=> (not (or (not (not (= ?this nullObject))) (not (= (x ?v_75 Memory) true_1)) (not (= (select2 ?Heap ?this inv) ?v_75)) (not (= (select2 ?Heap ?this localinv) ?v_75)) (not (= (IsHeap ?Heap) true_1)) (not (= (select2 ?Heap ?this allocated) true_1)))) (= (= (Memory_InSandbox_System_Int32 ?Heap ?this ?addr_in) true_1) (= (Memory_InSandbox_System_Int32_1 (select2 ?Heap ?this exposeVersion) ?addr_in) true_1)))) :pattern ((Memory_InSandbox_System_Int32 ?Heap ?this ?addr_in)) ))) (not (= (x RTE RTE) true_1)) (not (= ?v_6 System_Object)) (not (= (AsDirectSubClass RTE ?v_6) RTE)) (not (not (= (IsImmutable RTE) true_1))) (not (= (AsMutable RTE) RTE)) (not (forall ((?U Int)) (! (=> (= (x ?U RTE) true_1) (= ?U RTE)) :pattern ((x ?U RTE)) ))) (not (forall ((?oi Int) (?h Int)) (! (let ((?v_79 (select2 ?h ?oi RTE_MStackMaxSize)) (?v_78 (select2 ?h ?oi RTE_MStackBase))) (let ((?v_80 (+ ?v_78 ?v_79)) (?v_77 (select2 ?h ?oi RTE_MSP)) (?v_76 (select2 ?h ?oi RTE_CSP))) (=> (not (or (not (= (IsHeap ?h) true_1)) (not (= (x (select2 ?h ?oi inv) RTE) true_1)) (not (not (= (select2 ?h ?oi localinv) ?v_6))))) (not (or (not (= 65536 (Length (select2 ?h (select2 ?h ?oi RTE_Data) Memory_contents)))) (not (= (Length (select2 ?h ?oi RTE_CallStack)) 10)) (not (<= 0 ?v_76)) (not (<= ?v_76 10)) (not (<= ?v_78 ?v_77)) (not (<= ?v_77 ?v_80)) (not (= (x_1 ?v_77 4) 0)) (not (= (x_1 ?v_78 4) 0)) (not (= (x_1 ?v_79 4) 0)) (not (<= ?v_80 (Length (select2 ?h (select2 ?h ?oi RTE_Scratch) Memory_contents)))) (not (<= 0 ?v_78)) (not (<= 0 ?v_79)) (not (= (select2 ?h ?oi RTE_DPP) ?v_80))))))) :pattern ((x (select2 ?h ?oi inv) RTE)) ))) (not (= (x Microsoft_Contracts_ObjectInvariantException Microsoft_Contracts_ObjectInvariantException) true_1)) (not (= (x Microsoft_Contracts_GuardException Microsoft_Contracts_GuardException) true_1)) (not (= (x System_Exception System_Exception) true_1)) (not (= ?v_7 System_Object)) (not (= (AsDirectSubClass System_Exception ?v_7) System_Exception)) (not (not (= (IsImmutable System_Exception) true_1))) (not (= (AsMutable System_Exception) System_Exception)) (not (= (x System_Runtime_Serialization_ISerializable System_Runtime_Serialization_ISerializable) true_1)) (not (= (x System_Runtime_Serialization_ISerializable System_Object) true_1)) (not (= (IsMemberlessType System_Runtime_Serialization_ISerializable) true_1)) (not (= (AsInterface System_Runtime_Serialization_ISerializable) System_Runtime_Serialization_ISerializable)) (not (= (x System_Exception System_Runtime_Serialization_ISerializable) true_1)) (not (= (x System_Runtime_InteropServices__Exception System_Runtime_InteropServices__Exception) true_1)) (not (= (x System_Runtime_InteropServices__Exception System_Object) true_1)) (not (= (IsMemberlessType System_Runtime_InteropServices__Exception) true_1)) (not (= (AsInterface System_Runtime_InteropServices__Exception) System_Runtime_InteropServices__Exception)) (not (= (x System_Exception System_Runtime_InteropServices__Exception) true_1)) (not (forall ((?oi Int) (?h Int)) (! (=> (not (or (not (= (IsHeap ?h) true_1)) (not (= (x (select2 ?h ?oi inv) System_Exception) true_1)) (not (not (= (select2 ?h ?oi localinv) ?v_7))))) true) :pattern ((x (select2 ?h ?oi inv) System_Exception)) ))) (not (= ?v_8 System_Exception)) (not (= (AsDirectSubClass Microsoft_Contracts_GuardException ?v_8) Microsoft_Contracts_GuardException)) (not (not (= (IsImmutable Microsoft_Contracts_GuardException) true_1))) (not (= (AsMutable Microsoft_Contracts_GuardException) Microsoft_Contracts_GuardException)) (not (forall ((?oi Int) (?h Int)) (! (=> (not (or (not (= (IsHeap ?h) true_1)) (not (= (x (select2 ?h ?oi inv) Microsoft_Contracts_GuardException) true_1)) (not (not (= (select2 ?h ?oi localinv) ?v_8))))) true) :pattern ((x (select2 ?h ?oi inv) Microsoft_Contracts_GuardException)) ))) (not (= ?v_9 Microsoft_Contracts_GuardException)) (not (= (AsDirectSubClass Microsoft_Contracts_ObjectInvariantException ?v_9) Microsoft_Contracts_ObjectInvariantException)) (not (not (= (IsImmutable Microsoft_Contracts_ObjectInvariantException) true_1))) (not (= (AsMutable Microsoft_Contracts_ObjectInvariantException) Microsoft_Contracts_ObjectInvariantException)) (not (forall ((?oi Int) (?h Int)) (! (=> (not (or (not (= (IsHeap ?h) true_1)) (not (= (x (select2 ?h ?oi inv) Microsoft_Contracts_ObjectInvariantException) true_1)) (not (not (= (select2 ?h ?oi localinv) ?v_9))))) true) :pattern ((x (select2 ?h ?oi inv) Microsoft_Contracts_ObjectInvariantException)) ))) (not (= (x System_String System_String) true_1)) (not (= ?v_10 System_Object)) (not (= (AsDirectSubClass System_String ?v_10) System_String)) (not (= (IsImmutable System_String) true_1)) (not (= (AsImmutable System_String) System_String)) (not (= (x System_IComparable System_IComparable) true_1)) (not (= (x System_IComparable System_Object) true_1)) (not (= (IsMemberlessType System_IComparable) true_1)) (not (= (AsInterface System_IComparable) System_IComparable)) (not (= (x System_String System_IComparable) true_1)) (not (= (x System_String System_ICloneable) true_1)) (not (= (x System_IConvertible System_IConvertible) true_1)) (not (= (x System_IConvertible System_Object) true_1)) (not (= (IsMemberlessType System_IConvertible) true_1)) (not (= (AsInterface System_IConvertible) System_IConvertible)) (not (= (x System_String System_IConvertible) true_1)) (not (= (x System_IComparable_1___System_String System_IComparable_1___System_String) true_1)) (not (= (x System_IComparable_1___System_String System_Object) true_1)) (not (= (IsMemberlessType System_IComparable_1___System_String) true_1)) (not (= (AsInterface System_IComparable_1___System_String) System_IComparable_1___System_String)) (not (= (x System_String System_IComparable_1___System_String) true_1)) (not (= (x System_Collections_Generic_IEnumerable_1___System_Char System_Collections_Generic_IEnumerable_1___System_Char) true_1)) (not (= (x System_Collections_Generic_IEnumerable_1___System_Char System_Object) true_1)) (not (= (x System_Collections_Generic_IEnumerable_1___System_Char System_Collections_IEnumerable) true_1)) (not (= (IsMemberlessType System_Collections_Generic_IEnumerable_1___System_Char) true_1)) (not (= (AsInterface System_Collections_Generic_IEnumerable_1___System_Char) System_Collections_Generic_IEnumerable_1___System_Char)) (not (= (x System_String System_Collections_Generic_IEnumerable_1___System_Char) true_1)) (not (= (x System_String System_Collections_IEnumerable) true_1)) (not (= (x System_IEquatable_1___System_String System_IEquatable_1___System_String) true_1)) (not (= (x System_IEquatable_1___System_String System_Object) true_1)) (not (= (IsMemberlessType System_IEquatable_1___System_String) true_1)) (not (= (AsInterface System_IEquatable_1___System_String) System_IEquatable_1___System_String)) (not (= (x System_String System_IEquatable_1___System_String) true_1)) (not (forall ((?U Int)) (! (=> (= (x ?U System_String) true_1) (= ?U System_String)) :pattern ((x ?U System_String)) ))) (not (forall ((?oi Int) (?h Int)) (! (=> (not (or (not (= (IsHeap ?h) true_1)) (not (= (x (select2 ?h ?oi inv) System_String) true_1)) (not (not (= (select2 ?h ?oi localinv) ?v_10))))) true) :pattern ((x (select2 ?h ?oi inv) System_String)) ))) (not (= (x Microsoft_Contracts_ICheckedException Microsoft_Contracts_ICheckedException) true_1)) (not (= (x Microsoft_Contracts_ICheckedException System_Object) true_1)) (not (= (IsMemberlessType Microsoft_Contracts_ICheckedException) true_1)) (not (= (AsInterface Microsoft_Contracts_ICheckedException) Microsoft_Contracts_ICheckedException))))))
+(assert (let ((?v_27 (BaseClass RTE)) (?v_48 (forall ((?o_1 Int) (?f_1 Int)) (! (let ((?v_51 (not (= ?o_1 this))) (?v_49 (select2 Heap ?o_1 ownerFrame)) (?v_50 (select2 Heap ?o_1 ownerRef))) (=> (not (or (not (= (IncludeInMainFrameCondition ?f_1) true_1)) (not (not (= ?o_1 nullObject))) (not (= (select2 Heap ?o_1 allocated) true_1)) (not (or (= ?v_49 PeerGroupPlaceholder) (not (= (x (select2 Heap ?v_50 inv) ?v_49) true_1)) (= (select2 Heap ?v_50 localinv) (BaseClass ?v_49)))) (not (or ?v_51 (not (= ?f_1 RTE_CurrRTEMode)))) (not (or ?v_51 (not (= ?f_1 RTE_RtnCode)))) (not (or ?v_51 (not (= ?f_1 exposeVersion)))))) (= (select2 Heap ?o_1 ?f_1) (select2 Heap_3 ?o_1 ?f_1)))) :pattern ((select2 Heap_3 ?o_1 ?f_1)) ))) (?v_47 (not (<= 0 0))) (?v_40 (select2 Heap_3 this RTE_MStackMaxSize)) (?v_36 (select2 Heap_3 this RTE_MStackBase))) (let ((?v_42 (+ ?v_36 ?v_40)) (?v_29 (not (not (or (not (= (x (select2 Heap_3 this inv) RTE) true_1)) (not (not (= (select2 Heap_3 this localinv) ?v_27)))))))) (let ((?v_46 (or ?v_29 (= (select2 Heap_3 this RTE_DPP) ?v_42))) (?v_45 (or ?v_29 (<= 0 ?v_40))) (?v_44 (or ?v_29 (<= 0 ?v_36))) (?v_43 (or ?v_29 (<= ?v_42 (Length (select2 Heap_3 (select2 Heap_3 this RTE_Scratch) Memory_contents))))) (?v_41 (or ?v_29 (= (x_1 ?v_40 4) 0))) (?v_39 (or ?v_29 (= (x_1 ?v_36 4) 0))) (?v_35 (select2 Heap_3 this RTE_MSP))) (let ((?v_38 (or ?v_29 (= (x_1 ?v_35 4) 0))) (?v_37 (or ?v_29 (<= ?v_35 ?v_42))) (?v_34 (or ?v_29 (<= ?v_36 ?v_35))) (?v_32 (select2 Heap_3 this RTE_CSP))) (let ((?v_33 (or ?v_29 (<= ?v_32 10))) (?v_31 (or ?v_29 (<= 0 ?v_32))) (?v_30 (or ?v_29 (= (Length (select2 Heap_3 this RTE_CallStack)) 10))) (?v_28 (or ?v_29 (= 65536 (Length (select2 Heap_3 (select2 Heap_3 this RTE_Data) Memory_contents))))) (?v_24 (select2 Heap_1 this ownerFrame)) (?v_25 (select2 Heap_1 this ownerRef))) (let ((?v_26 (or (= ?v_24 PeerGroupPlaceholder) (not (= (x (select2 Heap_1 ?v_25 inv) ?v_24) true_1)) (= (select2 Heap_1 ?v_25 localinv) (BaseClass ?v_24)))) (?v_0 (not (= this nullObject)))) (let ((?v_23 (not ?v_0)) (?v_16 (select2 Heap_1 this RTE_MStackMaxSize)) (?v_12 (select2 Heap_1 this RTE_MStackBase))) (let ((?v_18 (+ ?v_12 ?v_16)) (?v_5 (not (not (or (not (= (x (select2 Heap_1 this inv) RTE) true_1)) (not (not (= (select2 Heap_1 this localinv) ?v_27)))))))) (let ((?v_22 (or ?v_5 (= (select2 Heap_1 this RTE_DPP) ?v_18))) (?v_21 (or ?v_5 (<= 0 ?v_16))) (?v_20 (or ?v_5 (<= 0 ?v_12))) (?v_19 (or ?v_5 (<= ?v_18 (Length (select2 Heap_1 (select2 Heap_1 this RTE_Scratch) Memory_contents))))) (?v_17 (or ?v_5 (= (x_1 ?v_16 4) 0))) (?v_15 (or ?v_5 (= (x_1 ?v_12 4) 0))) (?v_11 (select2 Heap_1 this RTE_MSP))) (let ((?v_14 (or ?v_5 (= (x_1 ?v_11 4) 0))) (?v_13 (or ?v_5 (<= ?v_11 ?v_18))) (?v_10 (or ?v_5 (<= ?v_12 ?v_11))) (?v_8 (select2 Heap_1 this RTE_CSP))) (let ((?v_9 (or ?v_5 (<= ?v_8 10))) (?v_7 (or ?v_5 (<= 0 ?v_8))) (?v_6 (or ?v_5 (= (Length (select2 Heap_1 this RTE_CallStack)) 10))) (?v_4 (or ?v_5 (= 65536 (Length (select2 Heap_1 (select2 Heap_1 this RTE_Data) Memory_contents))))) (?v_1 (select2 Heap this ownerFrame)) (?v_2 (select2 Heap this ownerRef))) (let ((?v_3 (or (= ?v_1 PeerGroupPlaceholder) (not (= (x (select2 Heap ?v_2 inv) ?v_1) true_1)) (= (select2 Heap ?v_2 localinv) (BaseClass ?v_1))))) (not (=> true (=> (= (IsHeap Heap) true_1) (=> (not (or (not (= (IsNotNull this RTE) true_1)) (not (= (select2 Heap this allocated) true_1)))) (=> (= (InRange code_in System_Int32) true_1) (=> (= (InRange code System_Int32) true_1) (=> (= PurityAxiomsCanBeAssumed true_1) (=> (= BeingConstructed nullObject) (=> (or (not (= (x (select2 Heap this inv) RTE) true_1)) (= (select2 Heap this localinv) System_Object)) (=> true (=> true (=> true (=> true (=> true (=> true (=> true (not (or ?v_23 (not (=> ?v_0 (not (or (not ?v_3) (not (=> ?v_3 (=> (= Heap_0 (store2 Heap this exposeVersion temp0_0)) (=> (= Heap_1 (store2 Heap_0 this RTE_CurrRTEMode 0)) (not (or (not ?v_4) (not (=> ?v_4 (not (or (not ?v_6) (not (=> ?v_6 (not (or (not ?v_7) (not (=> ?v_7 (not (or (not ?v_9) (not (=> ?v_9 (not (or (not ?v_10) (not (=> ?v_10 (not (or (not ?v_13) (not (=> ?v_13 (not (or (not ?v_14) (not (=> ?v_14 (not (or (not ?v_15) (not (=> ?v_15 (not (or (not ?v_17) (not (=> ?v_17 (not (or (not ?v_19) (not (=> ?v_19 (not (or (not ?v_20) (not (=> ?v_20 (not (or (not ?v_21) (not (=> ?v_21 (not (or (not ?v_22) (not (=> ?v_22 (=> (= (IsHeap Heap_1) true_1) (not (or ?v_23 (not (=> ?v_0 (not (or (not ?v_26) (not (=> ?v_26 (=> (= Heap_2 (store2 Heap_1 this exposeVersion temp1_0)) (=> (= Heap_3 (store2 Heap_2 this RTE_RtnCode code_in)) (not (or (not ?v_28) (not (=> ?v_28 (not (or (not ?v_30) (not (=> ?v_30 (not (or (not ?v_31) (not (=> ?v_31 (not (or (not ?v_33) (not (=> ?v_33 (not (or (not ?v_34) (not (=> ?v_34 (not (or (not ?v_37) (not (=> ?v_37 (not (or (not ?v_38) (not (=> ?v_38 (not (or (not ?v_39) (not (=> ?v_39 (not (or (not ?v_41) (not (=> ?v_41 (not (or (not ?v_43) (not (=> ?v_43 (not (or (not ?v_44) (not (=> ?v_44 (not (or (not ?v_45) (not (=> ?v_45 (not (or (not ?v_46) (not (=> ?v_46 (=> (= (IsHeap Heap_3) true_1) (=> (not (or ?v_47 ?v_47)) (=> true (not (or (not ?v_48) (not (=> ?v_48 true)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+(check-sat)
+(exit)