| Bound_P-infer_p.smt2 |
| StaticField_Test.Foo.smt2 |
| DynamicTypes_Sub0..ctor.smt2 |
| VisibilityBasedInvariants_Friend.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| ExposeVersion_X..ctor-level_2.smt2 |
| PeerFields_Parent..ctor.smt2 |
| PeerFields_PeerFields.Assign2_PeerFields.smt2 |
| Bag1_Bag.Add_System.Int32.smt2 |
| PureAxioms_UnsoundSpec..ctor-level_2.smt2 |
| PeerModifiesClauses_Homeboy.Q-level_2.smt2 |
| MustOverride_Ex4.B.foo.smt2 |
| Pack_Bad2.Cell..cctor.smt2 |
| Chunker_Chunker..ctor_System.String_notnull_System.Int32.smt2 |
| InitialValuesGood_Cell..ctor.smt2 |
| AdvancedTypes_AdvancedTypes.Advanced4_P_notnull-orderStrength_1.smt2 |
| Spouse_Person.MM.smt2 |
| Arrays_Q4-noinfer.smt2 |
| PureAxioms_UnsoundSpec.Unsound-level_2.smt2 |
| Lock_LockingExample.smt2 |
| AndNumbers_T..ctor-level_0.smt2 |
| Search_Search.Inc_System.Int32-noinfer.smt2 |
| IntToString_Test..ctor.smt2 |
| WhileTrueLoop_Test.M.smt2 |
| MustOverride_Ex3.B.foo.smt2 |
| DynamicTypes_Sub0.M.smt2 |
| ManualRange1_Tools.Range_Enumerator.get_Current.smt2 |
| Arrays_P0-noinfer.smt2 |
| PeerConsistentLoop_C.M0_System.Int32.smt2 |
| Literals_Test.Bar.smt2 |
| loopinv1_LoopInv1..ctor-infer_eh.smt2 |
| Finally_ReturnFinally.TryFinally0-modifiesOnLoop.smt2 |
| DoWhileGood_Test.Copy_System.Int32.smt2 |
| Spouse_Person..cctor.smt2 |
| StrictReadOnly_C1.P.smt2 |
| Change769_Test5.Foo_System.Int32.ptr.smt2 |
| Change769_Test8.TriggerMe_System.Int32.smt2 |
| Ensures_Q-noinfer_3.smt2 |
| AdditiveMethods_OwnedResults.Mm_System.Boolean.smt2 |
| Boxes_Boxes_2.P1_Boxes_2..type.parameter.U.smt2 |
| VarMapFixPoint_main.smt2 |
| Alloc_T.get_Next.smt2 |
| Unsigned_test.Conversions_System.UInt32_System.Double.smt2 |
| PeerFields_Parent.M.smt2 |
| Array_test3.MyClass.Allocate1_System.Int32.smt2 |
| Recursion0_Recursion0..ctor-infer_i.smt2 |
| AdditiveMethods_AdditiveMethods.X0.smt2 |
| DynamicTypes_SealedSub.M.smt2 |
| ExposeVersion_A..ctor-level_2.smt2 |
| Assumptions_Assumptions..ctor.HARD.smt2 |
| Bag7_Bag..cctor.smt2 |
| FieldUpdateLoop_Test..ctor.smt2 |
| Literals_Test.Quux_System.Int64.smt2 |
| AssignToNonInvariantField_AnotherClient.UpdateTheRep_Good.smt2 |
| SimpleWhile1_SimpleWhile1..ctor-infer_i.smt2 |
| Interval_Interval.Shift_System.Int32.smt2 |
| equivpoly0_M-infer_ep-vc_local.smt2 |
| ExplicitExposeVersionHavoc_A..ctor-level_2.smt2 |
| Global_MyNamespace.Global..ctor.smt2 |
| Chunker9_Chunker.NextChunk.smt2 |
| Immutable_test3.C..ctor_test3.B_notnull.smt2 |
| ExposeVersion_S..ctor-level_2.smt2 |
| Call_Call.Main.smt2 |
| AdditiveMethods_AdditiveMethods.M.smt2 |
| Arrays_Q2-noinfer.smt2 |
| PureCall_Test.FieldLikeTest.smt2 |
| loopinv0_LoopInv0.N-infer_eh.smt2 |
| SimpleAssignments2_SimpleAssignments2..ctor-infer_i.smt2 |
| ModifiesClauses_C.Method0.smt2 |
| Quantifiers_W-noinfer.smt2 |
| StrictReadOnly_C1.W3.smt2 |
| BoxedInt_BoxedInt.Main.smt2 |
| loopinv0_Node..ctor-infer_eh.smt2 |
| Types_Types.P4_System.Object.array_notnull_System.Int32.array_notnull_A.array_notnull_J.array_notnull_B.array_notnull-orderStrength_1.smt2 |
| Change769_Test1..ctor_System.Int32.smt2 |
| Finally_ReturnFinally.TryFinally3-modifiesOnLoop.smt2 |
| Bag1_Bag..ctor_System.Int32.array.smt2 |
| QuantifierVisibilityInvariant_A.N.smt2 |
| ExactTypes_X..ctor.smt2 |
| BasicMethodology_Component..ctor_System.Int32.smt2 |
| AdditiveMethods_OwnedResults.Static1.smt2 |
| PeerFields_PeerFields.Assign4.smt2 |
| Typeof_Typeof.N.smt2 |
| QuantifierVisibilityInvariant_AnotherInvariantNameIssue..ctor.smt2 |
| B_Q1-noinfer.smt2 |
| Arrays_Q3-noinfer.smt2 |
| VisibilityBasedInvariants_Thing.S.smt2 |
| Passification_Array0-noinfer.smt2 |
| Passification_good0-noinfer.smt2 |
| CommittedOblivious_W.PureOp.smt2 |
| LocalExpose_C.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| equivpoly1_M-infer_ep-vc_local.smt2 |
| Chunker5_Chunker..cctor.smt2 |
| PeerModifiesClauses_Homeboy.E-level_2.smt2 |
| BClient_Client..ctor.smt2 |
| MustOverride_Ex4.B..ctor.smt2 |
| AssumeEnsures_BarBad-noinfer.smt2 |
| BasicMethodology_Component.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| Literals_Test..ctor.smt2 |
| Unsigned_test.Caller1.smt2 |
| Immutable_test3.C.M1.smt2 |
| Boxes_Boxes_2.A.smt2 |
| Types_Types.P1_K_notnull-orderStrength_1.smt2 |
| PeerFields_PeerFields.Assign3.smt2 |
| Chunker6_Chunker..ctor_System.String_notnull_System.Int32.smt2 |
| AdvancedTypes_AdvancedTypes.Advanced4_X_notnull-orderStrength_1.smt2 |
| BasicMethodology_CS.foo.smt2 |
| ExposeVersion_A.FieldUpdateWithGetterQuery_A_notnull-level_2.smt2 |
| Types_Types..ctor-orderStrength_1.smt2 |
| ExplicitExposeVersionHavoc_A.Unsound-level_2.smt2 |
| AssignToRepField_AssignToRepField..ctor_System.Boolean.smt2 |
| Strings_test3.XY.M4_System.Object.smt2 |
| WhereMotivation_Types.MCall-modifiesOnLoop_1.smt2 |
| Strings_test3.XY.N1_test3.XY_notnull_System.Object_notnull.smt2 |
| PureAxioms_A..ctor-level_2.smt2 |
| AdvancedTypes_InternalClass..ctor-orderStrength_1.smt2 |
| BasicMethodology_Component..ctor_System.Int32_System.Boolean.smt2 |
| Alloc_Alloc.Main.smt2 |
| Chunker6_Chunker..cctor.smt2 |
| ExactTypes_P..ctor.smt2 |
| DynamicTypes_DynamicTypes.P1.smt2 |
| ExposeVersion_A.MethodCallWithMethodQuery-level_2.smt2 |
| LocalExpose_T.V0.smt2 |
| Array_test3.MyClass.DimLengthRank1_System.String.array_notnull.smt2 |
| Types_T.M-orderStrength_1.smt2 |
| ModifiesClauses_D..ctor.smt2 |
| Immutable_test3.E.Mfalse.smt2 |
| Boxes_Boxes_2.N_System.Int32.smt2 |
| loopinv1_F.M-infer_eh.smt2 |
| Bag3_Bag..cctor.smt2 |
| AddMethod_Bag.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| CommittedOblivious_CO..ctor.smt2 |
| ParamOut_Test.foo_MyInterface_2...System.String___System.String_notnull.smt2 |
| StrictReadOnly_C1.W2.smt2 |
| AndNumbers_T.M_System.Collections.Generic.IEnumerable_1...type.parameter.T_2550_System.Int32_System.Boolean-level_0.smt2 |
| Types_Types.P2_K_notnull-orderStrength_1.smt2 |
| BClient_Client.P_MyClass_notnull.smt2 |
| StructTests_St..ctor_System.Int32-level_2.smt2 |
| DefaultLoopInv0_Test..ctor-modifiesOnLoop-noinfer.smt2 |
| QuantifierVisibilityInvariant_A.P.smt2 |
| Strings_test3.XY.M3_System.Object_notnull.smt2 |
| PureAxioms_A.SumXYAxiomFromBody-level_2.smt2 |
| AdditiveMethods_OwnedResults..ctor.smt2 |
| Pack_Good1.Cell..cctor.smt2 |
| ExposeVersion_C.foo-level_2.smt2 |
| Bag8_Bag.Add_System.Int32.smt2 |
| CommittedOblivious_W.ConfinedOp.smt2 |
| Operators_Operators.P_System.Boolean_System.Boolean.smt2 |
| ExactTypes_F.M_X.array_notnull.smt2 |
| Strengthen_U..ctor.smt2 |
| SimpleAssignments2_SimpleAssignments2.DivisionByZero-infer_i.smt2 |
| BClient_Client.Main.HARD.smt2 |
| BasicMethodology_CS.test0.smt2 |
| Delegate_Delegate.P_MyDelegate.smt2 |
| AssertFalse_AssertFalseTest.Test1.smt2 |
| Boxes_Boxes_2..ctor.smt2 |
| Factory_Test.N.smt2 |
| Types_Types.N0_C_D-orderStrength_1.smt2 |
| Quantifiers_S-noinfer.smt2 |
| PeerFields_Parent.P.smt2 |
| Change769_Test8.Foo2_System.Int32.array_notnull.smt2 |
| Passification_Q-noinfer.smt2 |
| AssignToNonInvariantField_InternalClass..ctor.smt2 |
| StaticFields_StaticFields.M.smt2 |
| Change773_Test2.Foo.smt2 |
| StrictReadOnly_C0..ctor.smt2 |
| LocalExpose_U.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| SiblingConstructors_SiblingConstructors..ctor_System.Int32.smt2 |
| AssumeEnsures_Foo-noinfer.smt2 |
| Types_T..ctor_D_notnull-orderStrength_1.smt2 |
| ExposeVersion_QClient.bar-level_2.smt2 |
| Quantifiers_V2-noinfer.smt2 |
| Quantifiers_R-noinfer.smt2 |
| Bag1_Bag..cctor.smt2 |
| BClient_Client.Q_MyClass_notnull_System.Boolean_System.Boolean.smt2 |
| ManualRange1_Tools.Range_Enumerator.MoveNext.smt2 |
| Chunker11c_Chunker.NextChunk.smt2 |
| AssertFalse_AssertFalseTest..ctor.smt2 |
| Spouse_Person.B1.smt2 |
| ValidAndPrevalid_Interval.Foo5.smt2 |
| Types_Types.N1_C_D-orderStrength_1.smt2 |
| ModifiesClauses_C.Method2.smt2 |
| Pack_Good2.Cell.GetX.smt2 |
| StructTests_St..ctor_System.Boolean-level_2.smt2 |
| Modifies_Arraytests.P0_System.String.array-level_2.smt2 |
| Search_Search.ContainsZero_WithExplicitInvariant_System.Int32.array_notnull-noinfer.smt2 |
| Spouse_Person.MarryAssignTheOtherWayAround_Person_notnull.smt2 |
| ExposeVersion_A.getValue_System.Int32-level_2.smt2 |
| AssignToNonInvariantField_AssignToNonInvariantField..cctor.smt2 |
| PureCall_Cell.set_FieldLikeProperty_System.Int32.smt2 |
| ExposeVersion_D..ctor-level_2.smt2 |
| LocalExpose_U.N0.smt2 |
| Strengthen_T.M.smt2 |
| StrictReadOnly_C2.X0.smt2 |
| Spouse_Person.Marry_CaptureThis_Person_notnull.smt2 |
| SimpleWhile5_SimpleWhile5..ctor-infer_i.smt2 |
| Old_Swap-noinfer.smt2 |
| ParamInAssert_Test.Foo_System.Int32.smt2 |
| AssignToRepField_AssignToRepField..ctor_T.smt2 |
| StrictReadOnly_C2.W2.smt2 |
| AdvancedTypes_AdvancedTypes.Main-orderStrength_1.smt2 |
| ValidAndPrevalid_PartOfLine..ctor.smt2 |
| PeerModifiesClauses_Homeboy.A-level_2.smt2 |
| QuantifierVisibilityInvariant_C..cctor.smt2 |
| QuantifierVisibilityInvariant_A.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| Array_test3.MyClass..ctor.smt2 |
| StrictReadOnly_C2.Y0.smt2 |
| ExposeVersion_QClient..ctor-level_2.smt2 |
| Bag0_Bag.Add_System.Int32.smt2 |
| WhereMotivation_Types.MLoop1.smt2 |
| ExactTypes_F..ctor_W_notnull.smt2 |
| ExposeVersion_X.FieldUpdateByObjectCreationWithMethodQueryFails_X_notnull-level_2.smt2 |
| AdvancedTypes_W..ctor-orderStrength_1.smt2 |
| PeerModifiesClauses_Homeboy.F-level_2.smt2 |
| CommittedOblivious_W..ctor.smt2 |
| LocalExpose_T.M1.smt2 |
| Change773_Test2..ctor.smt2 |
| Chunker4_Chunker.NextChunk.smt2 |
| VisibilityBasedInvariants_Thing.R.smt2 |
| FormulaTerm2_QX-noinfer.smt2 |
| PeerModifiesClauses_Homeboy.T-level_2.smt2 |
| equiv4_M-infer_e-vc_local.smt2 |
| AssignToNonInvariantField_ClientClass..ctor.smt2 |
| B_P0-noinfer.smt2 |
| Arrays_P2-noinfer.smt2 |
| VisibilityBasedInvariants_Friend..cctor.smt2 |
| AdvancedTypes_X..ctor-orderStrength_1.smt2 |
| Spouse_Person.NN.smt2 |
| StrictReadOnly_C1..ctor.smt2 |
| BasicMethodology_SubClass.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| WhereClause_C..ctor.smt2 |
| BasicMethodology_SubClass..cctor.smt2 |
| AssumeEnsures_BarGood-noinfer.smt2 |
| AssertFalse_AssertFalseTest.Test0.smt2 |
| equiv6_M-infer_e-vc_local.smt2 |
| loopinv0_LoopInv0..ctor-infer_eh.smt2 |
| Unsigned_test.KitchenSink1_System.SByte_System.Byte_System.Int16_System.UInt16_System.Int32_System.UInt32_System.Int64_System.UInt64_System.Char.smt2 |
| heapsucc2_M-infer_eh-vc_local.smt2 |
| Alloc_T.M.smt2 |
| Chunker11b_Chunker.NextChunk.smt2 |
| StaticFields_StaticFields..ctor.smt2 |
| Types_Types.Main-orderStrength_1.smt2 |
| StrictReadOnly_D..ctor.smt2 |
| AssignToNonInvariantField_AnotherClient.P_Good.smt2 |
| Spouse_Possession..ctor.smt2 |
| DoWhileBad_Test.Copy_System.Int32.smt2 |
| Alloc_Alloc.M0_T.smt2 |
| ValidAndPrevalid_Cell..ctor.smt2 |
| Switch_Switch.M2_System.String_notnull_System.String_notnull.smt2 |
| AdvancedTypes_InternalSubClass..ctor-orderStrength_1.smt2 |
| BoxedInt_BoxedInt.P_System.Double.smt2 |
| WhereMotivation_Types.M-modifiesOnLoop_1.smt2 |
| PureReceiverMightBeCommitted_T.Q.smt2 |
| BasicMethodology_CS..ctor.smt2 |
| Strings_test3.MyStrings.StringCoolness3.smt2 |
| Array_test3.MyClass.Allocate0_System.Int32.smt2 |
| EnsuresFalse_C.foo.smt2 |
| Finally_ReturnFinally..cctor-modifiesOnLoop.smt2 |
| Immutable_test3.E.M.smt2 |
| Strings_test3.MyStrings.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| Passification_bad0-noinfer.smt2 |
| Search_Search..ctor-noinfer.smt2 |
| Spouse_Person.Marry_Person_notnull.smt2 |
| Array_test3.MyClass.M2_test3.MyClass.array2_notnull.smt2 |
| BoxedInt_BoxedInt.T_System.Int32.smt2 |
| Passification_Array2-noinfer.smt2 |
| Global_MyNamespace.Old.IncGBad.smt2 |
| BClient_Client.R_MyClass_notnull_System.Boolean.smt2 |
| Ensures_Q-noinfer_1.smt2 |
| FieldUpdateLoop_Test.Method.smt2 |
| Boxes_Boxes_2.Q_System.Int32.smt2 |
| Assumptions_Sub.Q.smt2 |
| ExposeVersion_A.FieldUpdateOnOtherWithMethodQuery_A_notnull_A_notnull-level_2.smt2 |
| Strings_test3.XY.M2.smt2 |
| Alloc_T.OtherTypes_Struct_Stru.smt2 |
| WhereMotivation_Types.MLoop0.smt2 |
| Spouse_Person..ctor.smt2 |
| StrictReadOnly_C1.Y0.smt2 |
| Immutable_test3.Typeof..ctor.smt2 |
| WhereMotivation_Types..ctor-modifiesOnLoop_1.smt2 |
| Types_Types.P6_System.Object.array_notnull_System.Int32.array_notnull_A.array_notnull_J.array_notnull_B.array_notnull-orderStrength_1.smt2 |
| Spouse_Person.MarryAssignTheOtherWayAround_GoodnessRestored_Person_notnull_System.Boolean.smt2 |
| StrictReadOnly_C2..ctor.smt2 |
| ManualRange1_Tools.Range_System.Int32_System.Int32.smt2 |
| ExposeVersion_A.MethodCallWithGetterQuery-level_2.smt2 |
| ManualRange1_Tools.Range_Enumerator..ctor_System.Int32_System.Int32.smt2 |
| CommittedOblivious_CO.P.smt2 |
| WhereMotivation_Types.MLoop3.smt2 |
| ExactTypes_F.CoVariance_W_notnull_System.Object.array_notnull.smt2 |
| PureReceiverMightBeCommitted_T..ctor.smt2 |
| heapaware0_M-infer_ep-vc_local.smt2 |
| ExplicitExposeVersionHavoc_D.SpecSharp.CheckInvariant_System.Boolean-level_2.smt2 |
| Types_Types.Px0_System.Object-orderStrength_1.smt2 |
| Bag0_Bag..cctor.smt2 |
| Axioms_Q-noinfer.smt2 |
| Bag2_Bag..cctor.smt2 |
| MultipleErrors_P-showErrorTrace-vc_local_1.smt2 |
| AndNumbers_T.OrRange_System.Boolean_System.Boolean-level_0.smt2 |
| WhereMotivation_Types.SLoop0-modifiesOnLoop_1.smt2 |
| Global_MyNamespace.Old..ctor.smt2 |
| Chunker1_Chunker..ctor_System.String_System.Int32.smt2 |
| StructTests_St.P-level_2.smt2 |
| Change769_Test7..ctor.smt2 |
| QuantifierVisibilityInvariant_A.M.smt2 |
| LocalExpose_D..ctor.smt2 |
| DefaultLoopInv0_A.N0_System.Int32-modifiesOnLoop-noinfer.smt2 |
| ModifiesClauses_ModifiesClauses.Test1_C_notnull.smt2 |
| ForLoop0_ForLoop0..ctor-infer_i.smt2 |
| Types_Types.Q_T_T-orderStrength_1.smt2 |
| PureCall_Cell.get_Natural.smt2 |
| AddMethod_Bag..cctor.smt2 |
| B_P1-noinfer.smt2 |
| IndexerInExpr_Test..ctor.smt2 |
| Chunker9_Chunker.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| SimpleWhile0_SimpleWhile0.CC77-infer_i.smt2 |
| Types_Types.P3_K_notnull-orderStrength_1.smt2 |
| StrictReadOnly_C0.foo0.smt2 |
| LocalExpose_C..cctor.smt2 |
| ValidAndPrevalid_Interval.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| PeerModifiesClauses_Homeboy.D-level_2.smt2 |
| IntToString_Test.Main.smt2 |
| PureCall_Cell.get_Value.smt2 |
| QuantifierVisibilityInvariant_B.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| Chunker11c_Chunker.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| SiblingConstructors_SiblingConstructors..cctor.smt2 |
| ExactTypes_F..ctor_System.Object.smt2 |
| Bag2_Bag.RemoveMin.smt2 |
| AdvancedTypes_AdvancedTypes.Advanced2_SubLessType_notnull-orderStrength_1.smt2 |
| AdvancedTypes_AdvancedTypes.Advanced0_InternalSubClass_notnull_K_notnull_InternalClass_notnull-orderStrength_1.smt2 |
| AssumeEnsures_Proc-noinfer_1.smt2 |
| Finally_ReturnFinally.Expose3_System.Boolean_System.Int32-modifiesOnLoop.smt2 |
| AdditiveMethods_OwnedResults.F2_System.Boolean.smt2 |
| Interval_Interval..cctor.smt2 |
| StaticField_Test.Bar.smt2 |
| Change769_MyException..ctor.smt2 |
| AssignToRepField_AssignToRepField..ctor.HARD.smt2 |
| Unsigned_test..ctor.smt2 |
| WhileBad_Test..ctor.smt2 |
| FormulaTerm_plus-noinfer.smt2 |
| ExposeVersion_Q..ctor-level_2.smt2 |
| Finally_ReturnFinally.Expose4_System.Boolean_System.Int32-modifiesOnLoop.smt2 |
| Pack_Bad1.Cell..ctor_System.Int32.smt2 |
| AssignToNonInvariantField_AnotherClient..cctor.smt2 |
| Bag9_Bag.RemoveMin.smt2 |
| DoWhileGood_Test..ctor.smt2 |
| AssumeEnsures_Proc-noinfer.smt2 |
| Alloc_Alloc.M5.smt2 |
| LocalExpose_C.M0.smt2 |
| loopinv0-nonnull_F.M-modifiesOnLoop.smt2 |
| Spouse_Person.A1_Possession_notnull.smt2 |
| Immutable_test3.C.M0.smt2 |
| Types_MoreTypes.P_System.Object-orderStrength_1.smt2 |
| StrictReadOnly_AlsoImpossible..ctor.smt2 |
| Assumptions_Assumptions..ctor_System.Boolean.HARD.smt2 |
| Strings_test3.MyStrings.StringCoolness0.smt2 |
| Unsigned_test.P_System.UInt32.smt2 |
| equiv0_M-infer_e-vc_local.smt2 |
| LocalExpose_T.V2.smt2 |
| BoxedInt_BoxedInt.R_System.Int32.smt2 |
| AssignToNonInvariantField_RepClass..ctor.smt2 |
| Assumptions_Sub.P.smt2 |
| AdvancedTypes_Q..ctor-orderStrength_1.smt2 |
| Types_Types.P7_System.Object.array_notnull_System.Int32.array_notnull_A.array_notnull_J.array_notnull_B.array_notnull-orderStrength_1.smt2 |
| AssignToNonInvariantField_T.Mc0.smt2 |
| Alloc_Alloc.GimmieOne.smt2 |
| Search_Search.ContainsZero_IncMethod_System.Int32.array_notnull-noinfer.smt2 |
| QuantifierVisibilityInvariant_AnotherInvariantNameIssue..cctor.smt2 |
| QuantifierVisibilityInvariant_AbstractCity0..ctor.smt2 |
| MultipleErrors_P-showErrorTrace-vc_block.smt2 |
| DefinedExpressions_DefinedExpressions.Division_System.Int32.smt2 |
| WhereMotivation_Types.SLoop0.smt2 |
| Interval_Cell..ctor_System.Int32.smt2 |
| Interval_Interval.BadShift2_System.Int32.smt2 |
| equiv6_M0-infer_e-vc_local.smt2 |
| LocalExpose_T.V3.smt2 |
| Strings_test3.MyStrings.StringCoolness1.smt2 |
| Good_Cell.Main.smt2 |
| CommittedOblivious_W.MutatingOp.smt2 |
| AdvancedTypes_Z0..ctor-orderStrength_1.smt2 |
| AdditiveMethods_Sub.StartHere2_AdditiveMethods_notnull.smt2 |
| quant0_Test.Foo.smt2 |
| PureAxioms_UnsoundSpec.Dummy1-level_2.smt2 |
| Quantifiers_T-noinfer.smt2 |
| Boxes_XYZ.Main.smt2 |
| StrictReadOnly_D.foo1_ImpossibleSub_notnull.smt2 |
| Axioms_P-noinfer.smt2 |
| Types_Types.M4_System.Object-orderStrength_1.smt2 |
| AssignToNonInvariantField_AnotherClient.P_AlsoBad.smt2 |
| Branching_T.P_System.Int32.smt2 |
| Subclass_Sub..ctor.smt2 |
| LocalExpose_U..cctor.smt2 |
| ExposeVersion_T..ctor-level_2.smt2 |
| SimpleWhile5_SimpleWhile5.NegativeWrong_System.Int32_System.Int32_System.Int32-infer_i.smt2 |
| Recursion0_Recursion0.fact_System.Int32-infer_i.smt2 |
| Factory_Test.M.smt2 |
| Types_Types.Px1_System.Object-orderStrength_1.smt2 |
| Change769_A..ctor.smt2 |
| AssignToRepField_AssignToRepField..ctor_System.Int32.array.smt2 |
| ExplicitExposeVersionHavoc_C..ctor-level_2.smt2 |
| AdditiveMethods_OwnedResults.Static2.smt2 |
| WhileGood_Test..ctor.smt2 |
| Immutable_test3.Imtbl..ctor.smt2 |
| Search_Search.ContainsZero_WithoutExplicitInvariant_System.Int32.array_notnull-noinfer.smt2 |
| LocalExpose_S.V1.smt2 |
| Chunker8_Chunker..ctor_System.String_notnull_System.Int32.smt2 |
| AssignToRepField_AssignToRepField.M.smt2 |
| Iff_Iff.R_System.Boolean_System.Boolean.smt2 |
| ManualRange1_Tools.Range_Enumerable..ctor_System.Int32_System.Int32.smt2 |
| Array2_test3.MyClass2..ctor.smt2 |
| PeerModifiesClauses_Homeboy.R-level_2.smt2 |
| SimpleWhile3_SimpleWhile3..ctor-infer_i.smt2 |
| MultipleErrors_P-showErrorTrace-vc_dag_2.smt2 |
| SimpleAssignments1_SimpleAssignments1..ctor-infer_i.smt2 |
| PeerFields_PeerFields.M_System.Int32.smt2 |
| Boxes_XYZ..ctor.smt2 |
| loopInvOnDemand_M.smt2 |
| Change769_Test4.Foo_A.smt2 |
| ValidAndPrevalid_Interval.Foo3.smt2 |
| LocalExpose_C.M1.smt2 |
| Unsigned_test.KitchenSink0_System.SByte_System.Byte_System.Int16_System.UInt16_System.Int32_System.UInt32_System.Int64_System.UInt64_System.Int32.smt2 |
| Immutable_test3.XY.M0_test3.Imtbl.smt2 |
| AdditiveMethods_OwnedResults.F3.smt2 |
| DoWhileBad_Test..ctor.smt2 |
| LocalExpose_T..cctor.smt2 |
| Bad_Cell.Main.smt2 |
| Bag0_Bag..ctor_System.Int32.array.smt2 |
| VisibilityBasedInvariants_Thing..cctor.smt2 |
| ValidAndPrevalid_Interval.Foo2.smt2 |
| Change769_Test8..ctor.smt2 |
| StaticFields_StaticFields.P.smt2 |
| Branching_T.N_System.Boolean.smt2 |
| ModifiesClauses_F..ctor.smt2 |
| PureAxioms_Getter.get_Value-level_2.smt2 |
| quant0_Test.Blah_System.Int32.smt2 |
| Bag5_Bag..cctor.smt2 |
| Quantifiers_X0-noinfer.smt2 |
| ParamOut_Test..ctor.smt2 |
| PeerFields_Parent.N.smt2 |
| PureCall_Test.TestGood.smt2 |
| Bag3_Bag.RemoveMin.smt2 |
| LocalExpose_C.M6.smt2 |
| AssignToNonInvariantField_AnotherClient.P_ViolatesInvariant.smt2 |
| PureReceiverMightBeCommitted_C.N.smt2 |
| Chunker11-AdditiveExpose_Chunker.NextChunk_NonVirtual.smt2 |
| Chunker6_Chunker.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| Bag5_Bag.Add_System.Int32.smt2 |
| Delegate_Delegate.CallIt_System.Int32_System.String_notnull.smt2 |
| Factory_Test..ctor.smt2 |
| Chunker0_Chunker.NextChunk.smt2 |
| Finally_ReturnFinally.TryFinally1-modifiesOnLoop.smt2 |
| Change769_S..ctor_System.Int32.smt2 |
| Change769_Test8.Foo3_System.Collections.Generic.IEnumerable_1...System.Int32.smt2 |
| WC-EI1_RTE.ExecuteInstruction-vc_nested.smt2 |
| Bag7_Bag.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| Capture_Capture.Caller0.smt2 |
| Finally_ReturnFinally.P1_System.Int32-modifiesOnLoop.smt2 |
| Bag8_Bag..cctor.smt2 |
| Literals_Test.Quiz_System.Double_System.Double.smt2 |
| ModifiesClauses_C..ctor.smt2 |
| equiv5_MPrime-infer_e-vc_local.smt2 |
| Boxes_Boxes_2.M_System.Int32.smt2 |
| CommittedOblivious_W.StateIndependentOp.smt2 |
| StructTests_St.M_System.Int32.array_notnull-level_2.smt2 |
| Chunker11-AdditiveExpose_Chunker.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| List_List.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| strings-no-where_Microsoft.Singularity.Applications.ThreadTest..ctor-noinfer.smt2 |
| DefinedExpressions_DefinedExpressions.Modulo_System.Boolean_System.Int32.array_notnull.smt2 |
| AdditiveMethods_Sub.Q.smt2 |
| AssignToNonInvariantField_InternalClass.M.smt2 |
| WhereMotivation_Types.SomeValue-modifiesOnLoop_1.smt2 |
| VisibilityBasedInvariants_Thing.Q.smt2 |
| DynamicTypes_DynamicTypes.P2.smt2 |
| LocalExpose_D.M1.smt2 |
| StrictReadOnly_C1.X0.smt2 |
| WhereMotivation_Types.SLoop1-modifiesOnLoop_1.smt2 |
| Switch_Switch.M_System.String_notnull.smt2 |
| SimpleWhile2_SimpleWhile2.AMethod-infer_i.smt2 |
| Chunker7_Chunker.NextChunk.smt2 |
| SimpleAssignments4_SimpleAssignment4..ctor-infer_i-vc_local-level_0.smt2 |
| Chunker11-AdditiveExpose_Chunker.NextChunk_Virtual.smt2 |
| Change769_Test6.Bar.smt2 |
| StrictReadOnly_Impossible..ctor.smt2 |
| AdvancedTypes_Y0..ctor-orderStrength_1.smt2 |
| Boxes_Boxes_2.P0_Boxes_2..type.parameter.T.smt2 |
| Bug163_S2.Foo_S2.smt2 |
| Bag4_Bag..ctor_System.Int32.array_notnull_System.Int32_System.Int32.smt2 |
| Global_MyNamespace.Global.N_System.Int32_System.Int32_System.Int32.smt2 |
| StrictReadOnly_AlsoImpossibleSub..ctor_System.Int32.smt2 |
| ExposeVersion_X.getValue_System.Int32-level_2.smt2 |
| AssertFalse_AssertFalseTest.Test2.smt2 |
| Bag8_Bag..ctor_System.Int32.array_notnull.smt2 |
| Unsigned_test.N.smt2 |
| Quantifiers_Q-noinfer.smt2 |
| Pack_Bad1.Cell..cctor.smt2 |
| Immutable_test3.Typeof.M_test3.Typeof_notnull.smt2 |
| AdvancedTypes_SubLessType..ctor-orderStrength_1.smt2 |
| Bag0_Bag.RemoveMin.smt2 |
| ExactTypes_F.Assign_X.array_X_System.Int32.smt2 |
| LocalExpose_S.V2.smt2 |
| PeerModifiesClauses_Homeboy.S-level_2.smt2 |
| Switch_Switch..ctor.smt2 |
| BasicMethodology_SubClass.P.smt2 |
| AndNumbers_T.OrRangeBad_System.Boolean_System.Boolean-level_0.smt2 |
| DefaultLoopInv0_B..ctor-modifiesOnLoop-noinfer.smt2 |
| PeerFields_PeerFields.Q_System.Int32.smt2 |
| Pack_Bad2.Cell.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| BasicMethodology_CS..cctor.smt2 |
| Unsigned_test.Q_System.Boolean.smt2 |
| Iff_Iff.Q_System.Boolean_System.Boolean.smt2 |
| Finally_ReturnFinally.M-modifiesOnLoop.smt2 |
| Finally_ReturnFinally.Expose2_System.Boolean_System.Int32-modifiesOnLoop.smt2 |
| AssignToNonInvariantField_AnotherClient.M.smt2 |
| Immutable_test3.C..ctor.smt2 |
| AssignToNonInvariantField_AnotherClient..ctor_System.Int32.smt2 |
| Chunker11a_Chunker..cctor.smt2 |
| Chunker11b_Chunker.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| Subclass_Sub.Ty.smt2 |
| StrictReadOnly_C2.P.smt2 |
| equiv1_M-infer_e-vc_local.smt2 |
| QuantifierVisibilityInvariant_A..cctor.smt2 |
| Alloc_Alloc.M1_T_notnull.smt2 |
| AdditiveMethods_AdditiveMethods.X1.smt2 |
| ExposeVersion_A.setValue_System.Int32-level_2.smt2 |
| SimpleWhile0_SimpleWhile0..ctor-infer_i.smt2 |
| strings-where_Microsoft.Singularity.Applications.ThreadTest.SecondThreadMethod-noinfer.smt2 |
| Chunker6_Chunker.NextChunk.smt2 |
| DynamicTypes_Sub1.M.smt2 |
| ModifiesClauses_ModifiesClauses.Test0_C_notnull.smt2 |
| Call_Call..ctor.smt2 |
| Spouse_Person.A3_Possession_notnull.smt2 |
| Interval_Interval..ctor_System.Int32_System.Int32.HARD.smt2 |
| Switch_Switch.FooString_System.String_notnull.smt2 |
| LocalExpose_S..ctor.smt2 |
| VisibilityBasedInvariants_Thing.P.smt2 |
| DynamicTypes_MyTestSpace.A.M_System.Object_notnull.smt2 |
| loopinv3_Foreach.M_System.Int32.array_notnull-infer_eh.smt2 |
| QuantifierVisibilityInvariant_A..ctor.smt2 |
| Alloc_Alloc.M2_T_notnull.smt2 |
| EnsuresFalse_C..ctor.smt2 |
| PureCall_Cell.Increment.smt2 |
| PureAxioms_A.SumXYNoAxiom1-level_2.smt2 |
| Modifies_Arraytests.Main-level_2.smt2 |
| PeerFields_PeerFields.Assign0.smt2 |
| Old_OutParam0-noinfer.smt2 |
| noopcall_NoOpCall.NoOp-infer_eh.smt2 |
| StrictReadOnly_C1.W1.smt2 |
| DefinedExpressions_DefinedExpressions.Modulo_System.Int32.smt2 |
| ExposeVersion_Q.blah_QClient-level_2.smt2 |
| AdvancedTypes_Y2..ctor-orderStrength_1.smt2 |
| B_Q0-noinfer.smt2 |
| equiv7_M-infer_e-vc_local.smt2 |
| Modifies_T..ctor-level_2.smt2 |
| Spouse_Person.Marry_CaptureEither_Person_notnull.smt2 |
| MustOverride_Ex4.C..ctor.smt2 |
| MustOverride_Ex1.B.foo.smt2 |
| Change773_Test1..ctor.smt2 |
| loopinv3_Foreach.M_System.Int32.array_notnull-infer_ehp_1.smt2 |
| SimpleWhile4_SimpleWhile4.AMethod-infer_i.smt2 |
| InitialValuesGood_Test.Main.smt2 |
| StrictReadOnly_C1.X1.smt2 |
| Literals_Test.Foo_System.String_notnull.smt2 |
| Generic_Test.Main.smt2 |
| Finally_ReturnFinally.N-modifiesOnLoop.smt2 |
| AdvancedTypes_Y1..ctor-orderStrength_1.smt2 |
| Chunker7_Chunker..cctor.smt2 |
| List_Node.InsertBad_System.Int32_System.Boolean.smt2 |
| ManualRange1_Tools.Range_Enumerator.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| Passification_good1-noinfer.smt2 |
| Bag0_Bag..ctor_System.Int32.array_notnull_System.Int32_System.Int32.smt2 |
| Immutable_test3.XY.M2_test3.Imtbl.smt2 |
| AssignToNonInvariantField_ClientClass.GoodUpdateOfY.smt2 |
| ExposeVersion_A.FieldUpdateOnOtherFieldWithMethodQuery-level_2.smt2 |
| ConstructorVisibility_Visitor.VisitLiteral_Literal_notnull.smt2 |
| PeerFields_Parent.Assign1.smt2 |
| Strings_test3.MyStrings.MyStringConcat_System.String_System.String.smt2 |
| Unsigned_test.KitchenSink2_System.SByte_System.Byte_System.Int16_System.UInt16_System.Int32_System.UInt32_System.Int64_System.UInt64_System.Char.smt2 |
| Change769_Test2.Foo.smt2 |
| Change769_Test3.Foo.smt2 |
| Pack_Bad2.Cell.GetX.smt2 |
| Pack_Good1.Cell.GetX.smt2 |
| Assumptions_Assumptions.Swap_System.Boolean.smt2 |
| Chunker10_Chunker.NextChunk.smt2 |
| ConstructorVisibility_UnaryExpr..ctor_System.Int32_Expr_notnull.smt2 |
| ExactTypes_Y2..ctor.smt2 |
| noopcall_NoOpCall.Method-infer_eh.smt2 |
| Pack_Good1.Cell.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| StrictReadOnly_C2.X1.smt2 |
| WhileBad_Test.Copy_System.Int32.smt2 |
| loopinv0_LoopInv0.Method2_Node_notnull-infer_eh.smt2 |
| BasicMethodology_BasicMethodology.P.smt2 |
| Types_MoreTypes..ctor-orderStrength_1.smt2 |
| Bag7_Bag.Add_System.Int32.smt2 |
| Bag1_Bag.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| Unsigned_test.O.smt2 |
| ModifyOther_Test..ctor.smt2 |
| Capture_Capture..ctor.smt2 |
| PeerModifiesClauses_Wallet..ctor-level_2.smt2 |
| PureAxioms_A.SumXYAxiomFromPost-level_2.smt2 |
| AssignToNonInvariantField_AnotherClient.UpdateTheRep_Bad.smt2 |
| Array2_test3.MyClass2.M0_System.Int32.array_notnull.smt2 |
| Array2_test3.MyClass2.M1_System.Int32.array.array_notnull.smt2 |
| Immutable_test3.XY.M3_test3.Imtbl.smt2 |
| ExposeVersion_T.m-level_2.smt2 |
| List_List..cctor.smt2 |
| Immutable_test3.Typeof.Foo_test3.Typeof_notnull.smt2 |
| Spouse_Person.B0_System.Object_notnull.smt2 |
| SimpleAssignments0_SimpleAssignments0.M_System.Int32-infer_i.smt2 |
| MustOverride_Ex1.B..ctor.smt2 |
| Factory_C..ctor.smt2 |
| BasicMethodology_C.foo.smt2 |
| VisibilityBasedInvariants_Thing.T.smt2 |
| BasicMethodology_Component..cctor.smt2 |
| Arrays_Q0-noinfer.smt2 |
| CallLoop_Test.Other-modifiesOnLoop-noinfer.smt2 |
| loopinv1_F.NoOp-infer_eh.smt2 |
| MustOverride_Ex2.B.foo.smt2 |
| PureCall_Cell.get_Id.smt2 |
| ValidAndPrevalid_Interval..cctor.smt2 |
| ExposeVersion_A.FieldUpdateOnOtherWithGetterQuery_A_notnull_A_notnull-level_2.smt2 |
| ExposeVersion_A.FieldUpdateWithMethodQuery_A_notnull-level_2.smt2 |
| ExposeVersion_C..ctor-level_2.smt2 |
| ExposeVersion_D.bar-level_2.smt2 |
| Strengthen_MainClass..ctor.smt2 |
| Types_A..ctor-orderStrength_1.smt2 |
| AssignToRepField_AssignToRepField.N.smt2 |
| Operators_Operators..ctor.smt2 |
| Array_test3.MyClass.M1_test3.MyClass.array.array_notnull.smt2 |
| AssertFalse_F..ctor.smt2 |
| Bag0_Bag.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| ManualRange1_Tools.Range_Enumerable.GetEnumerator.smt2 |
| Chunker0_Chunker..ctor_System.String_System.Int32.smt2 |
| loopinv0_LoopInv0.Method0-infer_eh.smt2 |
| PeerModifiesClauses_Homeboy.P-level_2.smt2 |
| QuantifierVisibilityInvariant_C.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| quant0_Test.Main_System.String.array.smt2 |
| AdditiveMethods_OwnedResults.F5.smt2 |
| WhereClause_D..ctor.smt2 |
| ConstructorVisibility_Literal..ctor_System.Int32.smt2 |
| LocalExpose_T.M2.smt2 |
| AssignToNonInvariantField_T..ctor.smt2 |
| Bag3_Bag..ctor_System.Int32.array_notnull.smt2 |
| StrictReadOnly_C1.W0.smt2 |
| StrictReadOnly_C2.M.smt2 |
| BasicMethodology_SubClass..ctor.smt2 |
| Ensures_Test..ctor.smt2 |
| PureReceiverMightBeCommitted_C.M.smt2 |
| List_Node.M.smt2 |
| DynamicTypes_Sub1..ctor.smt2 |
| ExposeVersion_A.FieldUpdateOnOtherFieldWithGetterQuery-level_2.smt2 |
| Ensures_Q-noinfer_7.smt2 |
| PureAxioms_Getter..ctor-level_2.smt2 |
| Cast_Cast..ctor.smt2 |
| VisibilityBasedInvariants_Thing.U.smt2 |
| ExposeVersion_X.ObjectCreationWithMethodQuery_X_notnull-level_2.smt2 |
| ExposeVersion_A.MethodCallOnOtherWithMethodQuery_A_notnull-level_2.smt2 |
| loopinv1_F..ctor-infer_eh.smt2 |
| Old_OldInCode0-noinfer.smt2 |
| Array2_test3.MyClass2.M2_System.Int32.array2_notnull.smt2 |
| Spouse_Person.A2_Possession_notnull.smt2 |
| ModifyOther_Test.Modify.smt2 |
| Pack_Bad1.Cell.GetX.smt2 |
| Bad_Cell..ctor.smt2 |
| Types_Types.Px2_System.Object-orderStrength_1.smt2 |
| ManualRange1_Test.Main.smt2 |
| MustOverride_Ex3.B..ctor.smt2 |
| Array_test3.MyClass.DimLengthRank1_System.String.array2_notnull.smt2 |
| AdditiveMethods_OwnedResults.F1.smt2 |
| Delegate_Delegate.M_MyDelegate.smt2 |
| Types_Types.M1_B-orderStrength_1.smt2 |
| AdvancedTypes_AdvancedTypes.Advanced5_P_notnull-orderStrength_1.smt2 |
| loopinv1_LoopInv1.Test0a_F_notnull-infer_eh.smt2 |
| LocalExpose_C.M2.smt2 |
| Types_MoreTypes.N_System.Object-orderStrength_1.smt2 |
| List_Node.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| Subclass_Sub..ctor_System.Boolean.smt2 |
| Types_B..ctor-orderStrength_1.smt2 |
| BasicMethodology_BasicMethodology.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| StrictReadOnly_C0.foo1.smt2 |
| PeerConsistentLoop_C.M_Coll_System.Int32.smt2 |
| ExactTypes_Q..ctor.smt2 |
| Global_MyNamespace.Global.M_System.Int32.smt2 |
| Bag2_Bag..ctor_System.Int32.array_notnull.smt2 |
| Immutable_test3.C.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| List_Node.Insert_System.Int32_System.Boolean.smt2 |
| ConstructorVisibility_Expr..ctor.smt2 |
| Unsigned_test.M.smt2 |
| InitialValuesBad_Cell..ctor.smt2 |
| Search_Search.Reverse_Div_System.Int32.array_notnull-noinfer.smt2 |
| IndexerInExpr_Test.Foo_System.Int32.array_notnull.smt2 |
| Boxes_Boxes_2.P2_Boxes_2..type.parameter.U.smt2 |
| ResultNotNewlyAllocated_C.O.smt2 |
| Bag1_Bag.RemoveMin.smt2 |
| AddMethod_Bag.Add_System.Int32.smt2 |
| AssignToNonInvariantField_T.Ma.smt2 |
| Global_MyNamespace.Old.IncG.smt2 |
| ForLoop0_ForLoop0.AForLoop_System.Int32-infer_i.smt2 |
| Strings_test3.MyStrings..cctor.smt2 |
| PeerModifiesClauses_Homeboy..ctor-level_2.smt2 |
| ExposeVersion_T.set_Value_System.Int32-level_2.smt2 |
| DynamicTypes_DynamicTypes.M.smt2 |
| MustOverride_Ex3.C.foo.smt2 |
| QuantifierVisibilityInvariant_B..cctor.smt2 |
| strings-no-where_Microsoft.Singularity.Applications.ThreadTest.Main_System.String.array-noinfer.smt2 |
| Immutable_test3.E..ctor.smt2 |
| Strengthen_U.M.smt2 |
| StrictReadOnly_AlsoImpossibleSub..ctor_System.Boolean.smt2 |
| Change769_Test5..ctor.smt2 |
| AdditiveMethods_Sub.X0.smt2 |
| Delegate_Delegate.InstanceDelegateTarget_System.Int32_System.Object_notnull.smt2 |
| Delegate_Delegate.N_MyDelegate_notnull.smt2 |
| ParamInAssert_Test..ctor.smt2 |
| Finally_ReturnFinally.P0_System.Int32-modifiesOnLoop.smt2 |
| Operators_Operators.M_System.Int32_System.Int32_System.Boolean_System.Object.array_notnull.smt2 |
| Factory_Test.O.smt2 |
| ExposeVersion_T.n-level_2.smt2 |
| AssignToNonInvariantField_AssignToNonInvariantField.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| AdvancedTypes_AdvancedTypes.Advanced3_W_notnull-orderStrength_1.smt2 |
| PeerFields_Parent.Q.smt2 |
| PureReceiverMightBeCommitted_C..ctor.smt2 |
| strings-where_Microsoft.Singularity.Applications.ThreadTest..ctor-noinfer.smt2 |
| loopinv0-nonnull_TestEnumerable..ctor-modifiesOnLoop.smt2 |
| Pack_Bad2.Cell..ctor_System.Int32.smt2 |
| VisibilityBasedInvariants_Thing.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| AssignToNonInvariantField_RepClass.M.smt2 |
| Bad_Cell.DoStuff_Cell.smt2 |
| Cast_Cast.Q_System.Object.smt2 |
| ValidAndPrevalid_Interval.Foo7.smt2 |
| Strengthen_MainClass.BoogieTest0_U_notnull.smt2 |
| DynamicTypes_MyTestSpace.AIType..ctor.smt2 |
| WhereClause_D.foo_System.String_System.String.ptr_System.String.ptr.smt2 |
| Chunker11-AdditiveExpose_Chunker..ctor_System.String_notnull_System.Int32.smt2 |
| Change769_Test6.Foo.smt2 |
| StrictReadOnly_ImpossibleSub..ctor.smt2 |
| Spouse_Person.B2.smt2 |
| PureCall_Test.TestBad.smt2 |
| Types_Types.P5_System.Object.array_notnull_System.Int32.array_notnull_A.array_notnull_J.array_notnull_B.array_notnull-orderStrength_1.smt2 |
| Chunker5_Chunker.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| SimpleWhile2_SimpleWhile2..ctor-infer_i.smt2 |
| AdditiveMethods_Sub.Z.smt2 |
| BClient_Client.DD.smt2 |
| AssignToNonInvariantField_AnotherClient.BadForAnotherReason.smt2 |
| Change769_Test6..ctor.smt2 |
| equiv6_M1-infer_e-vc_local.smt2 |
| ExactTypes_Y0..ctor.smt2 |
| ValidAndPrevalid_Interval.Foo1.smt2 |
| PureAxioms_Getter.set_Value_System.Int32-level_2.smt2 |
| equiv6_M3-infer_e-vc_local.smt2 |
| Assumptions_Sub.N.smt2 |
| WhereMotivation_Types.MLoop0-modifiesOnLoop_1.smt2 |
| PureAxioms_B.Dummy2-level_2.smt2 |
| equiv6_M2-infer_e-vc_local.smt2 |
| Boxes_Boxes_2.S1_Boxes_2..type.parameter.T.smt2 |
| SimpleWhile5_SimpleWhile5.Positive_System.Int32_System.Int32_System.Int32-infer_i.smt2 |
| Ensures_Q-noinfer_8.smt2 |
| Strings_test3.MyStrings.MyStringInsert_System.String_notnull_System.Int32_System.String_notnull.smt2 |
| MustOverride_Ex4.C.foo.smt2 |
| quant0_Test..ctor.smt2 |
| Alloc_T..ctor.smt2 |
| Bag2_Bag.Add_System.Int32.smt2 |
| Alloc_Alloc.M4_T_notnull.smt2 |
| QuantifierVisibilityInvariant_C..ctor_System.Int32.smt2 |
| Change769_S.Foo.smt2 |
| Alloc_T.OtherTypes_ArrayOfStructs_Stru.array_notnull_System.Int32.smt2 |
| VisibilityBasedInvariants_Friend..ctor_Thing_notnull_System.Boolean.smt2 |
| Change774_Test1..ctor.smt2 |
| ModifyOther_A..ctor.smt2 |
| AssertFalse_AssertFalseTest.Test3.smt2 |
| Chunker8_Chunker.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| loopinv1_LoopInv1.Test1b_F_notnull-infer_eh.smt2 |
| Typeof_Typeof.M.smt2 |
| Unsigned_test.OrRange_System.Boolean.smt2 |
| ExposeVersion_T.get_Value-level_2.smt2 |
| BClient_Client.R0_MyClass_notnull.smt2 |
| ConstructorVisibility_BinaryExpr..ctor_System.Int32_Expr_notnull_Expr_notnull.smt2 |
| Pack_Good1.Cell..ctor_System.Int32.smt2 |
| BasicMethodology_CS.test2.smt2 |
| Strengthen_T..ctor.smt2 |
| Ensures_Test.FooGood.smt2 |
| StrictReadOnly_C2.Y2.smt2 |
| Chunker10_Chunker..cctor.smt2 |
| Chunker2_Chunker.NextChunk.smt2 |
| AssignToNonInvariantField_ClientClass.M.smt2 |
| AssignToNonInvariantField_T.Mc1.smt2 |
| ExactTypes_F.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| Chunker4_Chunker..ctor_System.String_notnull_System.Int32.smt2 |
| ValidAndPrevalid_Interval.Foo4.smt2 |
| Capture_Capture.Caller2_System.Object_notnull.smt2 |
| StrictReadOnly_C2.Y3.smt2 |
| Unsigned_test.Caller0_System.UInt32.smt2 |
| PureAxioms_B.Dummy1-level_2.smt2 |
| Chunker8_Chunker.NextChunk.smt2 |
| AssignToNonInvariantField_RepClass.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| WC-EI0_RTE.ExecuteInstruction-vc_nested.smt2 |
| Strings_test3.MyStrings..ctor.smt2 |
| BoxedInt_BoxedInt.S_System.Int32.smt2 |
| equiv5_M-infer_e-vc_local.smt2 |
| Immutable_test3.XY.M5_System.Object.smt2 |
| Pack_Good2.Cell..ctor_System.Int32.smt2 |
| AdditiveMethods_Sub.StartHere0_AdditiveMethods_notnull.smt2 |
| Strings_test3.XY.M1_System.String.smt2 |
| LocalExpose_T.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| Cast_Cast.M_System.String_System.String_notnull.smt2 |
| AdditiveMethods_OwnedResults.Mz.smt2 |
| Ensures_Q-noinfer_5.smt2 |
| Types_F..ctor-orderStrength_1.smt2 |
| ResultNotNewlyAllocated_C..ctor.smt2 |
| Types_Types.P10_J.array_notnull_B.array_notnull_F.array_notnull-orderStrength_1.smt2 |
| AdditiveMethods_Sub.StartHere1_AdditiveMethods_notnull.smt2 |
| Bag8_Bag.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| ExactTypes_Y1..ctor.smt2 |
| AssignToRepField_AssignToRepField.Sqrt.smt2 |
| SiblingConstructors_SiblingConstructors..ctor_System.Int32_System.Boolean.smt2 |
| Change769_Test4..ctor.smt2 |
| strings-where_Microsoft.Singularity.Applications.ThreadTest.Main_System.String.array-noinfer.smt2 |
| StrictReadOnly_C2.Z0.smt2 |
| Immutable_test3.XY.M4_test3.Imtbl.smt2 |
| List_List..ctor.smt2 |
| Quantifiers_V1-noinfer.smt2 |
| Bag7_Bag..ctor_System.Int32.array_notnull.smt2 |
| Strings_test3.XY.N2_System.Object_notnull_test3.XY_notnull.smt2 |
| quant0_Test.MainX_System.optional...NonNullType.String.array_notnull.smt2 |
| loopinv3_Foreach..ctor-infer_eh.smt2 |
| BasicMethodology_CS.test3.smt2 |
| Pack_Good2.Cell..cctor.smt2 |
| InitialValuesBad_Test..ctor.smt2 |
| Immutable_test3.XY..ctor.smt2 |
| BasicMethodology_BasicMethodology.PeekBelow.smt2 |
| PeerModifiesClauses_Homeboy.C-level_2.smt2 |
| DynamicTypes_DynamicTypes.N0.smt2 |
| Immutable_test3.B.M.smt2 |
| Cast_Cast.R_System.Object_System.Int32.smt2 |
| StrictReadOnly_C2.X2.smt2 |
| Chunker10_Chunker.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| Delegate_Delegate.CheckTypes_MyDelegate.smt2 |
| Types_D..ctor-orderStrength_1.smt2 |
| WhereMotivation_Types.SLoop1.smt2 |
| Pack_Bad1.Cell.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| Bag7_Bag.RemoveMin.smt2 |
| Delegate_Delegate..ctor_System.Boolean.smt2 |
| Chunker11a_Chunker..ctor_System.String_notnull_System.Int32.smt2 |
| AdditiveMethods_OwnedResults.Static0.smt2 |
| PureCall_Test.AnotherTestGood.smt2 |
| Ensures_Q-noinfer_2.smt2 |
| SimpleWhile5_SimpleWhile5.Fact_System.Int32-infer_i.smt2 |
| Quantifiers_U1-noinfer.smt2 |
| CommittedOblivious_CO.Q.smt2 |
| BoxedInt_BoxedInt.N_System.Int32.smt2 |
| PureAxioms_B..ctor-level_2.smt2 |
| Change769_B..ctor.smt2 |
| ResultNotNewlyAllocated_C.P.smt2 |
| SiblingConstructors_SiblingConstructors.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| PureAxioms_A.SumXYNoAxiom2-level_2.smt2 |
| AdditiveMethods_T..ctor.smt2 |
| PureReceiverMightBeCommitted_C.O.smt2 |
| PeerFields_Parent.Assign0.smt2 |
| PureReceiverMightBeCommitted_T.P.smt2 |
| Types_Types.P0_K_notnull-orderStrength_1.smt2 |
| Iff_Iff.M_System.Boolean_System.Boolean.smt2 |
| LocalExpose_D.M0.smt2 |
| Iff_Iff.P_System.Boolean_System.Boolean.smt2 |
| ExplicitExposeVersionHavoc_D..cctor-level_2.smt2 |
| Spouse_Person.A0_System.Object_notnull.smt2 |
| DefaultLoopInv0_A.N1_System.Int32-modifiesOnLoop-noinfer.smt2 |
| Chunker_Chunker.NextChunk.smt2 |
| AddMethod_Bag..ctor_System.Int32.array_notnull.smt2 |
| AdditiveMethods_Sub.Y.smt2 |
| ExactTypes_Z0..ctor.smt2 |
| Chunker11b_Chunker..ctor_System.String_notnull_System.Int32.smt2 |
| Passification_P-noinfer.smt2 |
| Array_test3.MyClass.M0_test3.MyClass.array_notnull.smt2 |
| AssignToNonInvariantField_T.Mb.smt2 |
| PeerConsistentLoop_Coll.P.smt2 |
| ManualRange2_Test.Main.smt2 |
| SimpleAssignments4_SimpleAssignment4.Rigoletto_System.Int32-infer_i-vc_local-level_0.smt2 |
| SimpleAssignments3_SimpleAssignments3..ctor-infer_i.smt2 |
| PeerFields_PeerFields.Assign5.smt2 |
| ConstructorVisibility_Visitor.VisitUnaryExpr_UnaryExpr_notnull.smt2 |
| Change775_Test7.Bar_S.smt2 |
| ExplicitExposeVersionHavoc_D.Foo-level_2.smt2 |
| Finally_ReturnFinally.SpecSharp.CheckInvariant_System.Boolean-modifiesOnLoop.smt2 |
| Cast_Cast.N1_System.String.smt2 |
| ConstructorVisibility_Visitor..ctor.smt2 |
| Change769_Test3..ctor.smt2 |
| Chunker5_Chunker..ctor_System.String_notnull_System.Int32.smt2 |
| Bag9_Bag.Add_System.Int32.smt2 |
| Types_Types.P8_System.Object.array_notnull_System.Int32.array_notnull_A.array_notnull_J.array_notnull_B.array_notnull-orderStrength_1.smt2 |
| Types_Types.P9_System.Object.array_notnull_System.Int32.array_notnull_A.array_notnull_J.array_notnull_B.array_notnull-orderStrength_1.smt2 |
| Bag5_Bag.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| StrictReadOnly_D.foo3_AlsoImpossibleSub_notnull.smt2 |
| LocalExpose_T.V1.smt2 |
| LocalExpose_C.M3.smt2 |
| Ensures_Q-noinfer.smt2 |
| Factory_C.Create.smt2 |
| Finally_ReturnFinally.Expose0_System.Boolean-modifiesOnLoop.smt2 |
| Bag3_Bag..ctor_System.Int32.array_notnull_System.Int32_System.Int32.smt2 |
| LocalExpose_T..ctor.smt2 |
| Strings_test3.MyStrings.UnpackString_System.String_notnull.smt2 |
| Bag5_Bag..ctor_System.Int32.array_notnull.smt2 |
| AddMethod_Bag.Main.smt2 |
| Bag5_Bag..ctor_System.Int32.array_notnull_System.Int32_System.Int32.smt2 |
| Change769_A.Blah.smt2 |
| AssignToNonInvariantField_AnotherClient.P_AlsoGood.smt2 |
| Finally_ReturnFinally.TryFinally2-modifiesOnLoop.smt2 |
| AssignToRepField_T..ctor.smt2 |
| AdvancedTypes_AdvancedTypes.Advanced6_JKL_notnull-orderStrength_1.smt2 |
| Quantifiers_V0-noinfer.smt2 |
| Change769_Test7.Bar.smt2 |
| PeerModifiesClauses_Homeboy.B-level_2.smt2 |
| Types_Types.M0_B_notnull_System.Boolean-orderStrength_1.smt2 |
| DefinedExpressions_DefinedExpressions..ctor.smt2 |
| Immutable_test3.C..cctor.smt2 |
| Strengthen_MainClass.BoogieTest0_T_notnull.smt2 |
| Alloc_T.Nx.smt2 |
| Immutable_test3.XY.M1_test3.Imtbl.smt2 |
| Quantifiers_X1-noinfer.smt2 |
| List_Node..cctor.smt2 |
| BasicMethodology_C..ctor.smt2 |
| Immutable_test3.B..ctor.smt2 |
| strings-no-where_Microsoft.Singularity.Applications.ThreadTest.FirstThreadMethod-noinfer.smt2 |
| WhereMotivation_Types.MLoop3-modifiesOnLoop_1.smt2 |
| Chunker12_Chunker.NextChunk.smt2 |
| ExactTypes_Z1..ctor.smt2 |
| BasicMethodology_BasicMethodology..cctor.smt2 |
| Alloc_T.OtherTypes_Array_T.array_notnull_System.Int32.smt2 |
| SimpleAssignments3_SimpleAssignments3.AnotherMethod_System.Int32-infer_i.smt2 |
| SimpleAssignments1_SimpleAssignments1.M_System.Int32-infer_i.smt2 |
| ManualRange2_Tools.Range_Body_System.Int32_System.Int32.smt2 |
| AssignToNonInvariantField_ClientClass.AnotherBadUpdateOfY.smt2 |
| ConstructorVisibility_Visitor.M.smt2 |
| BoxedInt_BoxedInt.M_System.Int32.smt2 |
| Modifies_Arraytests.P1_System.String.array-level_2.smt2 |
| Generic_Test..ctor.smt2 |
| Modifies_Arraytests.Bad_System.Int32.array_notnull-level_2.smt2 |
| DefaultLoopInv0_A.M-modifiesOnLoop-noinfer.smt2 |
| Chunker9_Chunker..cctor.smt2 |
| FormulaTerm2_P-noinfer.smt2 |
| Chunker8_Chunker..cctor.smt2 |
| BasicMethodology_ExtensibleComponent..ctor.smt2 |
| StructTests_St.N-level_2.smt2 |
| Array_test3.MyClass.M3_System.Array_notnull.smt2 |
| DefaultLoopInv0_Test.Method-modifiesOnLoop-noinfer.smt2 |
| StaticFields_StaticFields.N.smt2 |
| LocalExpose_C..ctor.smt2 |
| loopinv0_LoopInv0.Method1-infer_eh.smt2 |
| noopcall_NoOpCall..ctor-infer_eh.smt2 |
| Modifies_C..ctor-level_2.smt2 |
| ResultNotNewlyAllocated_C.M.smt2 |
| LocalExpose_S.V0.smt2 |
| ExactTypes_F.N_P.array.smt2 |
| ExposeVersion_X.FieldUpdateByObjectCreationWithMethodQuery_X_notnull-level_2.smt2 |
| StructTests_St.SpecSharp.CheckInvariant_System.Boolean-level_2.smt2 |
| Factory_Test.R.smt2 |
| PeerFields_PeerFields.S_System.Int32.smt2 |
| PeerConsistentLoop_T..ctor.smt2 |
| AssignToNonInvariantField_AssignToNonInvariantField..ctor.smt2 |
| AssignToNonInvariantField_RepClass..cctor.smt2 |
| Subclass_Super..ctor.smt2 |
| AdditiveMethods_AdditiveMethods.Z.smt2 |
| ExplicitExposeVersionHavoc_C.Foo-level_2.smt2 |
| strings-where_Microsoft.Singularity.Applications.ThreadTest.FirstThreadMethod-noinfer.smt2 |
| Factory_Test.Q.smt2 |
| Chunker2_Chunker..ctor_System.String_notnull_System.Int32.smt2 |
| Change769_Test2..ctor.smt2 |
| AssignToNonInvariantField_AnotherClient..ctor.smt2 |
| Change775_S.Foo.smt2 |
| loopinv0-nonnull_F..ctor-modifiesOnLoop.smt2 |
| strings-no-where_Microsoft.Singularity.Applications.ThreadTest.SecondThreadMethod-noinfer.smt2 |
| PeerConsistentLoop_C.M1_System.Int32.smt2 |
| Strings_test3.XY..ctor.smt2 |
| AdditiveMethods_OwnedResults.Pz.smt2 |
| Interval_Cell.Shift_System.Int32.smt2 |
| ExposeVersion_A.FieldUpdateOnOtherWithMethodQueryWithDifferentParam_A_notnull_A_notnull-level_2.smt2 |
| DynamicTypes_SealedSub..ctor.smt2 |
| Good_Cell..ctor.smt2 |
| PureCall_Cell.get_FieldLikeProperty.smt2 |
| LocalExpose_S..cctor.smt2 |
| ParamInAssert_Test.Bar_System.Int32.smt2 |
| LocalExpose_D.M2.smt2 |
| Chunker7_Chunker..ctor_System.String_notnull_System.Int32.smt2 |
| StrictReadOnly_C1.M.smt2 |
| ExplicitExposeVersionHavoc_C.Unsound-level_2.smt2 |
| AssignToNonInvariantField_AnotherClient.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| AssignToNonInvariantField_AssignToNonInvariantField.M.smt2 |
| Bug163_S1.Foo.smt2 |
| Bag8_Bag..ctor_System.Int32.array_notnull_System.Int32_System.Int32.smt2 |
| LocalExpose_C.M7.smt2 |
| WhereClause_C.foo.smt2 |
| StrictReadOnly_C1.Y1.smt2 |
| AdditiveMethods_Sub..ctor.smt2 |
| AndNumbers_T.EnumerableCount_System.Collections.Generic.IEnumerable_1...type.parameter.T-level_0.smt2 |
| Passification_Loop0-noinfer.smt2 |
| loopinv3_Foreach..ctor-infer_ehp_1.smt2 |
| AssignToNonInvariantField_RepClass.P.smt2 |
| Cast_Cast.N0_System.String_System.Char.array.smt2 |
| PeerFields_PeerFields.R_System.Int32.smt2 |
| Modifies_Arraytests.M1_System.Int32.array_notnull-level_2.smt2 |
| AdvancedTypes_AdvancedTypes.Advanced1_SubLessType-orderStrength_1.smt2 |
| ModifiesClauses_ModifiesClauses..ctor.smt2 |
| Spouse_Person.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| PeerConsistentLoop_Coll..ctor.smt2 |
| PeerFields_PeerFields.P_System.Int32.smt2 |
| Bag2_Bag.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| loopinv0-nonnull_TestEnumerable.Test1_F_notnull-modifiesOnLoop.smt2 |
| StrictReadOnly_D.foo0_Impossible_notnull.smt2 |
| DynamicTypes_DynamicTypes.P0.smt2 |
| Ensures_Test.FooBad.smt2 |
| FormulaTerm_plus2-noinfer.smt2 |
| Interval_Interval.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| SiblingConstructors_SiblingConstructors..ctor_System.Int32_System.Int32.smt2 |
| LocalExpose_U..ctor.smt2 |
| ConstructorVisibility_Visitor.VisitExpr_Expr_notnull.smt2 |
| Types_Types.M2_B-orderStrength_1.smt2 |
| LocalExpose_S.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| Alloc_Alloc.M3_T_notnull.smt2 |
| Strings_test3.MyStrings.MyStringIndexOf_System.String_notnull_System.String_notnull.smt2 |
| PeerFields_PeerFields.Assign1_PeerFields.smt2 |
| PeerFields_PeerFields.Ouch.smt2 |
| AdvancedTypes_Z1..ctor-orderStrength_1.smt2 |
| AdditiveMethods_Sub.P.smt2 |
| CallLoop_Test.Method-modifiesOnLoop-noinfer.smt2 |
| ExposeVersion_A.set_Value_System.Int32-level_2.smt2 |
| AdvancedTypes_P..ctor-orderStrength_1.smt2 |
| Unsigned_test.R_System.Int32.smt2 |
| ModifiesClauses_ModifiesClauses.Test4_D_notnull.smt2 |
| ValidAndPrevalid_Cell.Increment.smt2 |
| AdditiveMethods_AdditiveMethods..ctor.smt2 |
| AssignToNonInvariantField_T.Md.smt2 |
| Branching_T..ctor.smt2 |
| WhileTrueLoop_Test..ctor.smt2 |
| LocalExpose_T.M0.smt2 |
| AssignToNonInvariantField_AnotherClient.P_Bad.smt2 |
| CutBackEdge_Test-noinfer.smt2 |
| LoopInvAssume_Test-noinfer.smt2 |
| ValidAndPrevalid_Interval.Foo8.smt2 |
| PeerConsistentLoop_C..ctor.smt2 |
| Bag2_Bag..ctor_System.Int32.array_notnull_System.Int32_System.Int32.smt2 |
| QuantifierVisibilityInvariant_AbstractCity1..ctor.smt2 |
| PureAxioms_GetterClient..ctor-level_2.smt2 |
| ExplicitExposeVersionHavoc_D..ctor-level_2.smt2 |
| Finally_ReturnFinally..ctor-modifiesOnLoop.smt2 |
| BClient_Client.S_MyClass_notnull_Client_notnull.smt2 |
| StrictReadOnly_C2.X3.smt2 |
| ConstructorVisibility_Visitor.VisitBinaryExpr_BinaryExpr_notnull.smt2 |
| ValidAndPrevalid_Interval.Foo6.smt2 |
| BoxedInt_BoxedInt..ctor.smt2 |
| AdditiveMethods_OwnedResults.F4.smt2 |
| Global_MyNamespace.Old.IncX.smt2 |
| SimpleWhile5_SimpleWhile5.NonNegative_System.Int32_System.Int32_System.Int32-infer_i.smt2 |
| WhereMotivation_Types.MLoop2.smt2 |
| Capture_Capture.Caller1_System.Object_notnull.smt2 |
| loopinv1_LoopInv1.Test1a_F_notnull-infer_eh.smt2 |
| Strings_test3.XY.N0_System.Object_notnull_System.Object_notnull.smt2 |
| StrictReadOnly_C1.Z1.smt2 |
| LockIncorrect_LockingExample.smt2 |
| DynamicTypes_DynamicTypes.N1.smt2 |
| Factory_Test.P.smt2 |
| Types_Types.M3_B-orderStrength_1.smt2 |
| Finally_ReturnFinally.Expose1_System.Boolean-modifiesOnLoop.smt2 |
| Delegate_Delegate..ctor.smt2 |
| ExposeVersion_A.get_Value-level_2.smt2 |
| FormulaTerm2_Q-noinfer.smt2 |
| Modifies_C.Correct_T_notnull-level_2.smt2 |
| Change773_Test1.Foo_System.Int32.array_notnull_System.Object_notnull.smt2 |
| Change769_Test7.Baz.smt2 |
| Modifies_C.Incorrect_T_notnull-level_2.smt2 |
| StrictReadOnly_C2.W0.smt2 |
| Assumptions_Sub..ctor.smt2 |
| AdvancedTypes_AnotherSubClass..ctor-orderStrength_1.smt2 |
| ExposeVersion_A.MethodCallOnOtherWithGetterQuery_A_notnull-level_2.smt2 |
| Global_MyNamespace.Old.IncXBad.smt2 |
| WhereMotivation_Types.MLoop2-modifiesOnLoop_1.smt2 |
| CallLoop_Test..ctor-modifiesOnLoop-noinfer.smt2 |
| StrictReadOnly_C2.W1.smt2 |
| AllocBeforeLoop_Test.Method-modifiesOnLoop-noinfer.smt2 |
| Old_Q-noinfer.smt2 |
| MustOverride_Ex2.B..ctor.smt2 |
| Old_R-noinfer.smt2 |
| Bag8_Bag.RemoveMin.smt2 |
| ManualRange1_Tools.Range_Enumerator..cctor.smt2 |
| ExactTypes_F..cctor.smt2 |
| ValidAndPrevalid_Interval.Foo9.smt2 |
| loopinv1_LoopInv1.Test0b_F_notnull-infer_eh.smt2 |
| Chunker11-AdditiveExpose_Chunker..cctor.smt2 |
| Call_Call.M_System.Int32.smt2 |
| Interval_Interval.BadShift_System.Int32.smt2 |
| AssignToRepField_Abc..ctor_System.Boolean.smt2 |
| PeerFields_Child.M.smt2 |
| VisibilityBasedInvariants_Thing..ctor.smt2 |
| ModifiesClauses_ModifiesClauses.Test3_D_notnull.smt2 |
| QuantifierVisibilityInvariant_AnotherInvariantNameIssue.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| Chunker1_Chunker.NextChunk.smt2 |
| VarMapFixPoint_SimpleWhile5.smt2 |
| SimpleWhile3_SimpleWhile3.AMethod-infer_i.smt2 |
| FormulaTerm_plus-noinfer_2.smt2 |
| Spouse_Person.PP.smt2 |
| BoxedInt_BoxedInt.Q_System.Object.smt2 |
| ExplicitExposeVersionHavoc_D.Unsound-level_2.smt2 |
| Search_Search.Reverse_Mul_System.Int32.array_notnull-noinfer.smt2 |
| AssignToNonInvariantField_T.Me.smt2 |
| AdvancedTypes_P_JKL..ctor-orderStrength_1.smt2 |
| BasicMethodology_CS.test1.smt2 |
| ExposeVersion_A.PureCall_A_notnull-level_2.smt2 |
| Ensures_P-noinfer.smt2 |
| LocalExpose_S.V3.smt2 |
| MustOverride_Ex3.C..ctor.smt2 |
| AssignToNonInvariantField_AssignToNonInvariantField.N.smt2 |
| Boxes_Boxes_2.S0_Boxes_2..type.parameter.T.smt2 |
| StructTests_St.S_System.Int32.ptr_System.Int32.ptr-level_2.smt2 |
| Typeof_Typeof..ctor.smt2 |
| QuantifierVisibilityInvariant_B..ctor_System.Int32.smt2 |
| AllocBeforeLoop_Test..ctor-modifiesOnLoop-noinfer.smt2 |
| StrictReadOnly_C2.Y1.smt2 |
| Branching_T.Q_System.Int32.ptr.smt2 |
| StructTests_St.R-level_2.smt2 |
| Passification_Array1-noinfer.smt2 |
| Modifies_Arraytests.M0_System.Int32.array_notnull-level_2.smt2 |
| LocalExpose_C.M5.smt2 |
| Ensures_Q-noinfer_4.smt2 |
| FormulaTerm2_PX-noinfer.smt2 |
| Bag4_Bag.Add_System.Int32.smt2 |
| Iff_Iff..ctor.smt2 |
| PeerFields_PeerFields.N_System.Int32.smt2 |
| Chunker5_Chunker.NextChunk.smt2 |
| Types_MoreTypes.M_System.Object-orderStrength_1.smt2 |
| SimpleWhile1_SimpleWhile1.Example-infer_i.smt2 |
| AdditiveMethods_AdditiveMethods.N.smt2 |
| DefinedExpressions_DefinedExpressions.Division_System.Boolean_System.Int32.array_notnull.smt2 |
| ExactTypes_W..ctor.smt2 |
| AssumeEnsures_Caller1-noinfer.smt2 |
| Strings_test3.MyStrings.StringCoolness2_System.Boolean.smt2 |
| WhileGood_Test.Copy_System.Int32.smt2 |
| Recursion0_Recursion0.SomeIterations_System.Int32-infer_i.smt2 |
| PeerFields_PeerFields..ctor_System.Int32.smt2 |
| Quantifiers_P-noinfer.smt2 |
| Types_C..ctor-orderStrength_1.smt2 |
| Branching_T.M_T_notnull_System.Int32.smt2 |
| Change775_Test7..ctor.smt2 |
| AssignToNonInvariantField_ClientClass.BadUpdateOfY.smt2 |
| StrictReadOnly_D.foo4_D_notnull.smt2 |
| DefaultLoopInv0_A..ctor-modifiesOnLoop-noinfer.smt2 |
| AdditiveMethods_OwnedResults.Pw.smt2 |
| BClient_Client.R1_MyClass_notnull.smt2 |
| SimpleAssignments0_SimpleAssignments0..ctor-infer_i.smt2 |
| Strings_test3.XY.M0_System.String_notnull.smt2 |
| VisibilityBasedInvariants_Friend..ctor_Thing_notnull.smt2 |
| BasicMethodology_CS.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| Capture_Capture.Caller3_System.Object_notnull.smt2 |
| CommittedOblivious_CO.M.smt2 |
| Delegate_Delegate.StaticDelegateTarget_System.Int32_System.Object_notnull.smt2 |
| PureAxioms_GetterClient.Dummy-level_2.smt2 |
| Chunker9_Chunker..ctor_System.String_notnull_System.Int32.smt2 |
| AdvancedTypes_AdvancedTypes..ctor-orderStrength_1.smt2 |
| Chunker7_Chunker.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| Bag1_Bag..ctor_System.Int32.array_notnull_System.Int32_System.Int32.smt2 |
| Pack_Good2.Cell.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| Interval_Interval.GetLength.smt2 |
| WC-EI2_RTE.ExecuteInstruction-vc_nested.smt2 |
| PeerFields_Child..ctor_System.Int32.smt2 |
| Bag4_Bag.SpecSharp.CheckInvariant_System.Boolean.smt2 |
| Bag5_Bag.RemoveMin.smt2 |
| Assumptions_Sub.M.smt2 |
| Assumptions_T..ctor.smt2 |
| AdditiveMethods_AdditiveMethods.Y.smt2 |
| Strengthen_MainClass.Main.HARD.smt2 |
| ExposeVersion_A.DummyPure_System.Int32_System.Int32-level_2.smt2 |
| WhereMotivation_Types.MLoop1-modifiesOnLoop_1.smt2 |
| SimpleWhile4_SimpleWhile4..ctor-infer_i.smt2 |
| DynamicTypes_DynamicTypes..ctor.smt2 |
| List_Node..ctor.smt2 |
| Capture_Capture.Foo_System.Object_notnull.smt2 |
| Quantifiers_U0-noinfer.smt2 |
| AdditiveMethods_OwnedResults.F0.smt2 |
| StaticField_Test..ctor.smt2 |
| quant0_Test.DeprivedMain_System.String.array_notnull.smt2 |
| Chunker11b_Chunker..cctor.smt2 |
| StrictReadOnly_C1.Z0.smt2 |
| Good_Cell.DoStuff_Cell.smt2 |
| Bag7_Bag..ctor_System.Int32.array_notnull_System.Int32_System.Int32.smt2 |
| StructTests_St.Q-level_2.smt2 |
| Ensures_Q-noinfer_6.smt2 |
| ParamOut_Test.Main.smt2 |
| ModifiesClauses_C.Method3.smt2 |
| Modifies_Arraytests..ctor-level_2.smt2 |
| AdditiveMethods_OwnedResults.Qz_System.Int32.smt2 |
| Irreducible_Test..ctor.smt2 |
| StrictReadOnly_D.foo2_AlsoImpossible_notnull.smt2 |
| ModifiesClauses_ModifiesClauses.Test2_C_notnull.smt2 |
| SimpleWhile5_SimpleWhile5.NegativeIntermediates_System.Int32_System.Int32_System.Int32-infer_i.smt2 |
| ModifiesClauses_C.Method1_System.Int32.array_notnull.smt2 |
| Cast_Cast.P_System.Object.smt2 |
| DynamicTypes_MyTestSpace.A..ctor.smt2 |
| Boxes_Boxes_2.R_Boxes_2..type.parameter.T_notnull.smt2 |