Test Summary
|
60%
successful |
Failed tests
- TestJP2KeY. { int j = 7; int i; i=1; byte d = 0; short f = 1; long l = 123; for (i=0, j=1; (i<42) && (i>0); i++, j--) { i=13; j=1; } while ((-i<7) || (i++==7--) | (--i==++7) ||(!true && false) || ('a'=='d') || ("asd"=="as"+"d") & (d==f) ^ (d/f+2>=f*d-f%d)|| (l<=~i) || !(this==null) || ((this!=null) ? (8<<j<8>>i) : (7&5>8>>>7L) || (7|5!=8^4)) && (i+=j) && (i=j) && (i/=j) && (i%=j) && (i-=j) && (i*=j) && (i<<=j) && (i>>=j) && (i >>>= j) && (i &= j) && (i ^= j) && (i |= j)) j=7; }
- TestJP2KeY. { int j=7; int i; i=1;do { j++; } while (i==1);if (j==42) j=7; else {i=7; j=43;}; ; label0: j=42; switch (j-i) {case 7: j=2; case 42: j=3; default: j=4; } while (j==42) loop1:{ if (j==7) break; if (j==43) break loop1; if (j==42) continue; if (j==41) continue loop1;} if (j>42) return;synchronized(null) { j=7; } }
- TestJP2KeY. { int x = 1; {java.util.List l;} }
- TestJP2KeY. {int[] a; a=new int[3]; a=new int[]{2,3,4}; int j=a[2]; j=a.length;}
- TestJP2KeY. class A1 { public A1() { }}
- TestJP2KeY. package qwe.rty; import qwe.rty.A; import dfg.hjk.*; import java.util.*; public abstract class A implements Z { static { d=3; Object v = new Object();} public static int d;A (int j) { d=5; } public A (int j, long k) {this(j); d=5; } private static final A[] b=new A[]{null}; long f; java.util.List s; public void abc() { Object z=new A(4, 5) { public int d=7; }; abc(); A a=(A)null; a=def(a); a=def(a).ghi(a).ghi(a); } { int x = 1; {int i = "\".length}"; } } protected A def(A a) {a=ghi(a); return new A(3);} private synchronized A ghi(A a) { a=ghi(a); ghi(a); A a1=null; a1=ghi(a1); a=def(a); return null;} protected abstract int[] jkl(A a, int i); protected Object o() {if (s instanceof Cloneable) return A.class;}} interface Z { public int d=0; } interface Z0 extends Z {} class A1 extends A { public static A a=new A(4); A1 (int j) {super(j);} }
- TestJP2KeY. public class B extends Object {class E { public E(Object s) {super();} }}
- TestJP2KeY. class circ_A { static int a = circ_B.b; } class circ_B { static int b = circ_A.a; }
- TestJP2KeY. class circ2_A { static final int a = circ2_B.b; } class circ2_B { static final int b = circ2_A.a; }
- TestJP2KeY. class Cycle1 { void m(Cycle2 c) {} } class Cycle2 { void m(Cycle1 c) {} }
- TestJP2KeY. class EmptyConstr { EmptyConstr(); }
- TestJP2KeY. testReadBlockWithContext()
- TestJavaCardDLJavaExtensions. testTypeNotInScopeShouldNotBeFound()
- TestJavaInfo. testFindImplicitAttributesForClassTypesOnly()
- TestClashFreeSubst. testClash()
- TestClashFreeSubst. testClashInSubstTerm()
- TestClashFreeSubst. testMultiShareBound()
- TestClashFreeSubst. testMultiSubst()
- TestClashFreeSubst. testShare()
- TestClashFreeSubst. testShareWary()
- TestClashFreeSubst. testSubst()
- TestClashFreeSubst. testSubstInSubstTerm()
- TestClashFreeSubst. testSubstWary()
- TestClashFreeSubst. testWary0()
- TestClashFreeSubst. testWary1()
- TestClashFreeSubst. testWary2()
- TestClashFreeSubst. xtestMultiClash()
- TestClashFreeSubst. xtestMultiClash1()
- TestLocalSymbols. testDoubleInstantiation()
- TestTermLabelManager. testGetSupportedTermLabelNames()
- TestTermLabelManager. testInstantiateLabels_applicationTermPolicies()
- TestTermLabelManager. testInstantiateLabels_childAndGrandchildPolicies_allRules()
- TestTermLabelManager. testInstantiateLabels_childAndGrandchildPolicies_ruleSpecific()
- TestTermLabelManager. testInstantiateLabels_directChildPolicies_allRules()
- TestTermLabelManager. testInstantiateLabels_directChildPolicies_ruleSpecific()
- TestTermLabelManager. testInstantiateLabels_modalityTermPolicies()
- TestTermLabelManager. testInstantiateLabels_taclet()
- TestTermLabelManager. testInstantiateLabels_updates_allRules()
- TestTermLabelManager. testInstantiateLabels_updates_ruleSpecific()
- TestTermLabelManager. testParseLabel()
- TestTermLabelManager. testrefactorGoal_childrenAndGrandchildren_allRules()
- TestTermLabelManager. testrefactorGoal_childrenAndGrandchildren_ruleSpecific()
- TestTermLabelManager. testrefactorGoal_directChildren_allRules()
- TestTermLabelManager. testrefactorGoal_directChildren_ruleSpecific()
- TestTermLabelManager. testrefactorGoal_none_allRules()
- TestTermLabelManager. testrefactorGoal_none_ruleSpecific()
- TestTermLabelManager. testrefactorGoal_sequent_allRules()
- TestTermLabelManager. testrefactorGoal_sequent_ruleSpecific()
- FocusCommandTest. testSelectionWithLabels()
- FocusCommandTest. testSimpleSelection()
- TestProofScriptCommand. [1] andRight.props, D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\macros\scripts\cases\andRight.props
- TestProofScriptCommand. [2] hide.exc.props, D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\macros\scripts\cases\hide.exc.props
- TestProofScriptCommand. [3] hide.props, D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\macros\scripts\cases\hide.props
- TestProofScriptCommand. [4] rule.exc.props, D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\macros\scripts\cases\rule.exc.props
- TestProofScriptCommand. [5] selectFormula.props, D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\macros\scripts\cases\selectFormula.props
- TestProofScriptCommand. [6] unhide.props, D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\macros\scripts\cases\unhide.props
- TestProofScriptCommand. [7] unhide2.props, D:\a\key\key\key.core\build\resources\test\de\uka\ilkd\key\macros\scripts\cases\unhide2.props
- RewriteTest. testLessTransitive()
- RewriteTest. testTransitive()
- ExprTest. [10] -5
- ExprTest. [11] 1 + 1 = 2
- ExprTest. [12] \if (3=4) \then (1) \else (2)
- ExprTest. [13] \if (3=4 & 1=1) \then (\if (3=4) \then (1) \else (2)) \else (2)
- ExprTest. [14] aa + bb*cc
- ExprTest. [15] aa%bb*cc < -123
- ExprTest. [16] \forall int x; true
- ExprTest. [17] \forall numbers x; x = x
- ExprTest. [18] (int)3+2
- ExprTest. [19] 1.f + 1f = 20e-1f * (2f-1f)
- ExprTest. [1] (bprod{int y;}(1, 2, y) = 0)
- ExprTest. [20] 1.d + 1d <= 20e+1d * .01d
- ExprTest. [21] 1f <= 2f
- ExprTest. [22] 2d > 1d
- ExprTest. [23] seqEmpty + seqEmpty
- ExprTest. [2] 1 = 1 -> 2 = 2
- ExprTest. [3] \< { int x = 1; } \> x=1
- ExprTest. [4] \<{ int x = 1; {int s = 2;} }\> x=x
- ExprTest. [5] true
- ExprTest. [6] true & false
- ExprTest. [7] 0
- ExprTest. [8] 1
- ExprTest. [9] 42
- ParseLDTsTests. testLDT()
- ParseLDTsTests. testSR()
- TestTacletEquality. initializationError
- TestDeclParser. testArrayDecl()
- TestDeclParser. testFunctionDecl()
- TestDeclParser. testGenericSortDecl1()
- TestDeclParser. testGenericSortDecl2()
- TestDeclParser. testGenericSortDecl3()
- TestDeclParser. testGenericSortDecl4()
- TestDeclParser. testGenericSortDecl6()
- TestDeclParser. testHeurDecl()
- TestDeclParser. testPredicateDecl()
- TestDeclParser. testProxySortDecl()
- TestDeclParser. testSVDecl()
- TestDeclParser. testSortDecl()
- TestIntLiteralParsing. initializationError
- TestIntLiteralParsing. initializationError
- TestIntLiteralParsing. initializationError
- TestIntLiteralParsing. initializationError
- TestIntLiteralParsing. initializationError
- TestJMLParserAssociativity. testLeftAssociativity()
- TestParser. testConstantEvaluationError()
- TestParser. testIssue1566()
- TestTacletParser. testFreeReplacewithVariables()
- TestTacletParser. testSchemaJava10()
- TestTacletParser. testSchemaJava4()
- TestTacletParser. testSchemaJava6()
- TestTacletParser. testSchemaJava8()
- TestTermParser. test1()
- TestTermParser. test10()
- TestTermParser. test11()
- TestTermParser. test12()
- TestTermParser. test13()
- TestTermParser. test14()
- TestTermParser. test1a()
- TestTermParser. test2()
- TestTermParser. test3()
- TestTermParser. test5()
- TestTermParser. test6()
- TestTermParser. test7()
- TestTermParser. test8()
- TestTermParser. test9()
- TestTermParser. testAmbigiousFuncVarPred()
- TestTermParser. testAttributeOnObject()
- TestTermParser. testAttributeWithSpecifiedSortOnObject()
- TestTermParser. testBindingUpdateTerm()
- TestTermParser. testBindingUpdateTerm_1()
- TestTermParser. testBindingUpdateTerm_3()
- TestTermParser. testBindingUpdateTerm_4()
- TestTermParser. testBindingUpdateTerm_5()
- TestTermParser. testBindingUpdateTerm_6()
- TestTermParser. testBindingUpdateTerm_7()
- TestTermParser. testBindingUpdateTerm_8()
- TestTermParser. testCast()
- TestTermParser. testIfThenElse()
- TestTermParser. testInfix1()
- TestTermParser. testInfix2()
- TestTermParser. testInfix3()
- TestTermParser. testInfix4()
- TestTermParser. testJavaAttributeAccessBoth_1()
- TestTermParser. testJavaAttributeAccessBoth_2()
- TestTermParser. testJavaAttributeAccessBoth_3()
- TestTermParser. testJavaAttributeAccess_4()
- TestTermParser. testJavaQueryAndAttribute_all()
- TestTermParser. testJavaStaticQuery()
- TestTermParser. testJavaStaticQueryWithParameter()
- TestTermParser. testNegativeLiteralParsing1()
- TestTermParser. testNegativeLiteralParsing2()
- TestTermParser. testNegativeLiteralParsing3()
- TestTermParser. testNotEqual()
- TestTermParser. testParsingArray()
- TestTermParser. testParsingArrayCombination()
- TestTermParser. testProgramVariables()
- TestTermParser. xtestBindingUpdateTermOldBindingAlternative()
- TestTermParser. xtestParsingArrayWithSpaces()
- TestTermParserHeap. testAccessStaticMembers()
- TestTermParserHeap. testAllFieldsSelector()
- TestTermParserHeap. testAtOperator_1()
- TestTermParserHeap. testAtOperator_2()
- TestTermParserHeap. testAtOperator_3()
- TestTermParserHeap. testAtOperator_4()
- TestTermParserHeap. testAtOperator_5()
- TestTermParserHeap. testAtOperator_6()
- TestTermParserHeap. testAtOperator_7()
- TestTermParserHeap. testAtOperator_8()
- TestTermParserHeap. testBracketHeapUpdate()
- TestTermParserHeap. testBugResettingCounter()
- TestTermParserHeap. testGenericObjectProperties()
- TestTermParserHeap. testLocationSets()
- TestTermParserHeap. testParsePrettyPrintedSelect()
- TestTermParserHeap. testQuantifiedSelect()
- TestTermParserHeap. testQueryBasic_1()
- TestTermParserHeap. testQueryBasic_10()
- TestTermParserHeap. testQueryBasic_11()
- TestTermParserHeap. testQueryBasic_2()
- TestTermParserHeap. testQueryBasic_3()
- TestTermParserHeap. testQueryBasic_4()
- TestTermParserHeap. testQueryBasic_5()
- TestTermParserHeap. testQueryBasic_6()
- TestTermParserHeap. testQueryBasic_7()
- TestTermParserHeap. testQueryBasic_8()
- TestTermParserHeap. testQueryBasic_9()
- TestTermParserHeap. testQueryInheritance_1()
- TestTermParserHeap. testQueryInheritance_2()
- TestTermParserHeap. testQueryInheritance_3()
- TestTermParserHeap. testQueryInheritance_4()
- TestTermParserHeap. testQueryInheritance_5()
- TestTermParserHeap. testQueryInheritance_6()
- TestTermParserHeap. testQueryInheritance_7()
- TestTermParserHeap. testQueryInheritance_8()
- TestTermParserHeap. testQueryInheritance_9()
- TestTermParserHeap. testStore()
- TestTermParserHeap. testUnknownConstant()
- TestTermParserHeap. testVerifyExceptionIfAtOperatorNotPreceededBySelectTerm()
- TestTermParserSorts. testParseIntegerArgs()
- TestTermParserSorts. testParseSequencePrettySyntax()
- TestOneStepSimplifier. loadWithRestriction()
- TestZipProofSaving. testZip()
- TestProofBundleIO. testComplexBundleGeneration()
- TestProofBundleIO. testSimpleBundleGeneration()
- TestApplyTaclet. testCatchList()
- TestApplyTaclet. testCompleteContextAddBug()
- TestApplyTaclet. testContextAdding()
- TestApplyTaclet. testPrgTacletApp()
- TestApplyTaclet. testRemoveEmptyBlock()
- TestMatchTaclet. testBugsThathaveBeenRemoved()
- TestMatchTaclet. testCloseWithBoundRenaming()
- TestMatchTaclet. testConflict()
- TestMatchTaclet. testInsequentStateRestriction()
- TestMatchTaclet. testNoContextMatching()
- TestMatchTaclet. testPrefixMatching()
- TestMatchTaclet. testProgramMatch4()
- TestMatchTaclet. testProgramMatchEmptyBlock()
- TestMatchTaclet. testRWVarOccursFindAndIf()
- TestMatchTaclet. testRWVarOccursInAddAndIf()
- TestMatchTaclet. testUpdateMatch()
- TestMatchTaclet. testVarOccursInFindAndAddRule()
- TestMatchTaclet. testVarOccursInIfAndAddRule()
- TestMatchTaclet. testWithSubSortsTermSV()
- TestMatchTaclet. testWithSubSortsVariableSV()
- TestMatchTaclet. testXNotFreeInYConflict()
- TestSchemaModalOperators. testSchemaModalities1()
- TestSchemaModalOperators. testSchemaModalities2()
- TestSchemaModalOperators. testSchemaModalities3()
- TestSchemaModalOperators. testSchemaModalities4()
- TestDropEffectlessElementary. testDoubleAssignment()
- TestDropEffectlessElementary. testFaultyCase()
- TestDropEffectlessElementary. testSelfAssignments()
- LoopScopeInvRuleTests. testDoAutomaticProofOfBenchmarkWithLabeledBreaksAndContinues()
- TestLegacyTacletMatch. testProgramMatch0()
- TestLegacyTacletMatch. testProgramMatch1()
- TestLegacyTacletMatch. testProgramMatch2()
- TestLegacyTacletMatch. testStatementListMatch()
- MergeRuleTests. testDoAutomaticGcdProofWithMergePointStatementAndBlockContract()
- MergeRuleTests. testDoAutomaticGcdProofWithMergePointStatements()
- MergeRuleTests. testDoManualGcdProof()
- MergeRuleTests. testLoadClosedGcdProofWithMergePointStatements()
- MergeRuleTests. testLoadGcdProof()
- MergeRuleTests. testLoadGcdProofWithPredAbstr()
- MergeRuleTests. testLoadGcdProofWithPredAbstrAndUserChoices()
- MergeRuleTests. testLoadProofWithDiffVarsWithSameNameAndMPS()
- MergeRuleTests. testMergeIndistinguishablePathConditionsWithFullAnonymization()
- MergeRuleTests. testMergeIndistinguishablePathConditionsWithITE()
- MergeRuleTests. testMergeThreeIndistinguishablePathConditionsWithITE()
- PredicateAbstractionLatticeTests. testCreateSignLatticeWithPredicates()
- PredicateAbstractionLatticeTests. testToAndFromString()
- TestProgramMetaConstructs. testForInitUnfoldTransformer1()
- TestProgramMetaConstructs. testForInitUnfoldTransformer2()
- TestTacletBuild. testSchemavariablesInAddrulesRespectPrefix()
- MasterHandlerTest. initializationError
- MasterHandlerTest. initializationError
- ProveSMTLemmasTest. [10] wellFormed.dl, \forall Heap h; \forall Object o; \forall Field f; (wellFormed(h) -> boolean::select(h, (java.lang.Object::select(h, o, f))<<Trigger>>, java.lang.Object::<created>) = TRUE | (java.lang.Object::select(h, o, f)) = null)
- ProveSMTLemmasTest. [11] jdiv.dl, \forall int divNum; \forall int divDenom; jdiv(divNum,divDenom) = \if (divNum >= 0) \then (div(divNum,divDenom)) \else (div(divNum*(-1),divDenom)*(-1))
- ProveSMTLemmasTest. [12] empty.dl, \forall Object o; \forall Field f; ( elementOf(o,f,empty)<<Trigger>> <-> false )
- ProveSMTLemmasTest. [13] allLocs.dl, \forall Object o; \forall Field f; ( elementOf(o,f,allLocs)<<Trigger>> <-> true )
- ProveSMTLemmasTest. [14] arrayRange.dl, \forall Object o; \forall Object o2; \forall Field f; \forall int lo; \forall int hi; (elementOf(o,f, arrayRange(o2, lo, hi))<<Trigger>> <-> o = o2 & \exists int iv; (f = arr(iv) & lo <= iv & iv <= hi))
- ProveSMTLemmasTest. [15] seqConcat.dl, \forall int i; \forall Seq s1; \forall Seq s2; ( 0 <= i & i < seqLen(s1) + seqLen(s2) -> any::seqGet(seqConcat(s1, s2), i) = \if (i < seqLen(s1)) \then (any::seqGet(s1, i)) \else (any::seqGet(s2, i-seqLen(s1))))
- ProveSMTLemmasTest. [16] seqLen.dl, \forall Seq s; seqLen(s)<<Trigger>> >= 0
- ProveSMTLemmasTest. [17] length.dl, \forall Object o; length(o) >= 0
- ProveSMTLemmasTest. [18] freshLocs.dl, \forall Heap h; \forall Object o; \forall Field f; ( elementOf(o,f,freshLocs(h))<<Trigger>> <-> o != null & !boolean::select(h,o,java.lang.Object::<created>)=TRUE )
- ProveSMTLemmasTest. [19] anon.dl, \forall Heap h; \forall Object o; \forall Field f; \forall Heap h2; \forall LocSet ls; any::select(anon(h, ls, h2), o, f)<<Trigger>> = \if(elementOf(o, f, ls) & f != java.lang.Object::<created> | elementOf(o, f, freshLocs(h))) \then(any::select(h2, o, f)) \else(any::select(h, o, f))
- ProveSMTLemmasTest. [1] jmod.dl, \forall int divNum; \forall int divDenom; jmod(divNum,divDenom) = divNum + jdiv(divNum,divDenom)*(-1)*divDenom
- ProveSMTLemmasTest. [20] memset.dl, \forall Heap h; \forall LocSet s; \forall any x; \forall Object o; \forall Field f; any::select(memset(h, s, x), o, f)<<Trigger>> = \if(elementOf(o, f, s) & f != java.lang.Object::<created>) \then(x) \else(any::select(h, o, f))
- ProveSMTLemmasTest. [21] store.dl, \forall Heap h; \forall Object o; \forall Field f; \forall Object o2; \forall Field f2; \forall any v; any::select(store(h,o,f,v), o2, f2)<<Trigger>> = \if(o = o2 & f = f2 & f != java.lang.Object::<created>) \then(v) \else(any::select(h, o2, f2))
- ProveSMTLemmasTest. [22] seqSub.dl.2, \forall Seq seq; \forall int from; \forall int to; seqLen(seqSub(seq, from, to)<<Trigger>>) = \if(from < to)\then(to - from)\else(0)
- ProveSMTLemmasTest. [23] seqSingleton.dl, \forall any x; any::seqGet(seqSingleton(x)<<Trigger>>, 0) = x
- ProveSMTLemmasTest. [24] seqSingleton.dl.2, \forall any x; seqLen(seqSingleton(x)<<Trigger>>) = 1
- ProveSMTLemmasTest. [25] null.dl, \forall any x; ((Null::instance(x))<<Trigger>> = TRUE -> x = null)
- ProveSMTLemmasTest. [2] seqSub.dl, \forall Seq seq; \forall int from; \forall int to; \forall int idx; any::seqGet(seqSub(seq, from, to)<<Trigger>>, idx) = \if(0 <= idx & idx < (to - from)) \then(any::seqGet(seq, idx + from)) \else(seqGetOutside)
- ProveSMTLemmasTest. [3] seqGetOutside.dl, \forall int i; \forall Seq s; ( i < 0 | i >= seqLen(s) -> any::seqGet(s, i)<<Trigger>> = seqGetOutside )
- ProveSMTLemmasTest. [4] singleton.dl, \forall Object o; \forall Field f; \forall Object o2; \forall Field f2; ( elementOf(o,f, singleton(o2,f2))<<Trigger>> <-> o = o2 & f = f2 )
- ProveSMTLemmasTest. [5] create.dl, \forall Heap h; \forall Object o; \forall Object o2; \forall Field f; any::select(create(h, o), o2, f)<<Trigger>> = \if(o = o2 & o != null & f = java.lang.Object::<created>) \then(TRUE) \else(any::select(h, o2, f))
- ProveSMTLemmasTest. [6] allFields.dl, \forall Object o; \forall Field f; \forall Object o2; ( elementOf(o,f, allFields(o2))<<Trigger>> <-> o = o2 )
- ProveSMTLemmasTest. [7] seqEmpty.dl, seqLen(seqEmpty) = 0
- ProveSMTLemmasTest. [8] union.dl, \forall Object o; \forall Field f; \forall LocSet l1; \forall LocSet l2; ( elementOf(o, f, union(l1, l2))<<Trigger>> <-> elementOf(o,f,l1) | elementOf(o,f,l2) )
- ProveSMTLemmasTest. [9] seqConcat.dl.2, \forall Seq s1; \forall Seq s2; seqLen(seqConcat(s1,s2)<<Trigger>>) = seqLen(s1) + seqLen(s2)
- ContractFactoryTest. testCombineDifferentAssignable()
- ContractFactoryTest. testCombineEmptyAssignable()
- ContractFactoryTest. testCombineEqualAssignable()
- TestJMLTranslator. testBsumBigInt()
- TestJMLTranslator. testBsumInt()
- TestJMLTranslator. testComplexExists()
- TestJMLTranslator. testComplexQueryResolving1()
- TestJMLTranslator. testComplexQueryResolving2()
- TestJMLTranslator. testComplexQueryResolving3()
- TestJMLTranslator. testCorrectImplicitThisResolution()
- TestJMLTranslator. testForAll()
- TestJMLTranslator. testForEx()
- TestJMLTranslator. testHexLiteral()
- TestJMLTranslator. testInfiniteUnion()
- TestJMLTranslator. testInfiniteUnion2()
- TestJMLTranslator. testIsInitialized()
- TestJMLTranslator. testLogicalExpression()
- TestJMLTranslator. testNonNullElements()
- TestJMLTranslator. testOld()
- TestJMLTranslator. testParenExpression()
- TestJMLTranslator. testPrimitiveField()
- TestJMLTranslator. testResultVar()
- TestJMLTranslator. testSelfVar()
- TestJMLTranslator. testSimpleQuery()
- TestJMLTranslator. testStaticQueryResolving()
- TestJMLTranslator. testSubtypeExpression()
- TestJMLTranslator. testSumParsing()
- TestJMLTranslator. testTrueTerm()
- ContractLoadingTests. issues1658()
- ContractLoadingTests. specMathBigintMathTest()
- ContractLoadingTests. specMathJavaMathTest()
- ContractLoadingTests. sumAndMax()
- JMLParserExceptionTest. case UnknownVar.java
- JMLParserExceptionTest. case UnknownVarInJML.java
- NJmlTranslatorTests. testContractModifiers()
- NJmlTranslatorTests. testContractModifiersMultiple()
- NJmlTranslatorTests. testContractModifiersMultipleAlso()
- NJmlTranslatorTests. testIgnoreOpenJML()
- NJmlTranslatorTests. testWarnRequires()
- TestTacletTranslator. testNegativePolarity()
- TestTacletTranslator. testNoPolarity()
- TestTacletTranslator. testPositivePolarity()
- TestTacletTranslator. testPropositional1()
- TestTacletTranslator. testPropositional2()
- TestEqualsModProofIrrelevancy. testJavaProof()
- TestProofStarter. testDirectProof()
- TestProofStarter. testDirectProofWithOneStepSimplification()
Ignored tests
- TestJP2KeY. xtestFileInput()
- TestDeclParser. testAmbiguousDecls()
- TestDeclParser. testGenericSortDecl5()
- TestParser. testRelativeInclude()
- ParserMessageTest. verifyColumnNumber()
- ParserMessageTest. verifyLineNumber()
- ParserMessageTest. verifyMessage()
- TestTacletIndex. disabled_testNonInteractiveIsShownOnlyIfHeuristicIsMissed()
- TestProgramMetaConstructs. testASTWalker()
- TestCvc4. testAdd1()
- TestCvc4. testAllex1()
- TestCvc4. testAllex2()
- TestCvc4. testAllex3()
- TestCvc4. testAndnot()
- TestCvc4. testAndornot()
- TestCvc4. testAndornot2()
- TestCvc4. testBProd1()
- TestCvc4. testBProd2()
- TestCvc4. testBProd3()
- TestCvc4. testBSum1()
- TestCvc4. testBSum2()
- TestCvc4. testBSum3()
- TestCvc4. testBinderPred2()
- TestCvc4. testBinderPred3()
- TestCvc4. testEqual1()
- TestCvc4. testEqual2()
- TestCvc4. testEqui1()
- TestCvc4. testEqui2()
- TestCvc4. testImply()
- TestCvc4. testImply2()
- TestCvc4. testImply3()
- TestCvc4. testLogicalIte1()
- TestCvc4. testLogicalIte2()
- TestCvc4. testOrnot()
- TestCvc4. testSubsort1()
- TestCvc4. testSubsort2()
- TestZ3. testAdd1()
- TestZ3. testAllex1()
- TestZ3. testAllex2()
- TestZ3. testAllex3()
- TestZ3. testAndnot()
- TestZ3. testAndornot()
- TestZ3. testAndornot2()
- TestZ3. testBProd1()
- TestZ3. testBProd2()
- TestZ3. testBProd3()
- TestZ3. testBSum1()
- TestZ3. testBSum2()
- TestZ3. testBSum3()
- TestZ3. testBinderPred2()
- TestZ3. testBinderPred3()
- TestZ3. testDiv1()
- TestZ3. testDiv3()
- TestZ3. testDiv5()
- TestZ3. testDiv6()
- TestZ3. testEqual1()
- TestZ3. testEqual2()
- TestZ3. testEqui1()
- TestZ3. testEqui2()
- TestZ3. testImply()
- TestZ3. testImply2()
- TestZ3. testImply3()
- TestZ3. testLogicalIte1()
- TestZ3. testLogicalIte2()
- TestZ3. testOrnot()
- TestZ3. testSubsort1()
- TestZ3. testSubsort2()
- TestJMLPreTranslator. disabled_testMLCommentEndInSLComment1()
- TestJMLPreTranslator. disabled_testMLCommentEndInSLComment2()
- JMLParserExceptionTest. case Bevhavioural.java
- JMLParserExceptionTest. case IllegalInv.java
- JMLParserExceptionTest. case KeyTest.java
- JMLParserExceptionTest. case TypeError.java
- TestTriggersSet. testTrigger2()
- DesignTests. xtestTermSubclassVisibility()
- TestProofUserManager. testUserManagement_NoEnvironment()