diff options
Diffstat (limited to 'test/regress/regress0/quantifiers/rew-to-0211-dd.smt2')
| -rw-r--r-- | test/regress/regress0/quantifiers/rew-to-0211-dd.smt2 | 259 |
1 files changed, 259 insertions, 0 deletions
diff --git a/test/regress/regress0/quantifiers/rew-to-0211-dd.smt2 b/test/regress/regress0/quantifiers/rew-to-0211-dd.smt2 new file mode 100644 index 000000000..ec49231e3 --- /dev/null +++ b/test/regress/regress0/quantifiers/rew-to-0211-dd.smt2 @@ -0,0 +1,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) |