Test Summary
|
99%
successful |
Failed tests
- TestTacletEquality. [270] bitwiseNegationInt, bitwiseNegationInt { \find(#normalassign ( (modal operator))\[{ .. #loc = ~#seCharByteShortInt; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseNegateInt(#se)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
- TestTacletEquality. [271] bitwiseNegationLong, bitwiseNegationLong { \find(#normalassign ( (modal operator))\[{ .. #loc = ~#se; ... }\] (post)) \replacewith(update-application(elem-update(#loc (program Variable))(javaBitwiseNegateLong(#seLong)),#normalassign(post))) \heuristics(executeIntegerAssignment) Choices: programRules:Java}
Ignored tests
- TestRecoder2KeY. xtestFileInput()
- TestClashFreeSubst. xtestMultiClash()
- TestClashFreeSubst. xtestMultiClash1()
- TestDeclParser. testAmbiguousDecls()
- TestDeclParser. testGenericSortDecl5()
- TestParser. testRelativeInclude()
- TestTermParser. test12()
- TestTermParser. testJavaQueryAndAttribute_all()
- TestTermParser. xtestBindingUpdateTermOldBindingAlternative()
- TestTermParser. xtestParsingArrayWithSpaces()
- ParserMessageTest. verifyColumnNumber()
- ParserMessageTest. verifyLineNumber()
- ParserMessageTest. verifyMessage()
- TestTacletIndex. disabled_testNonInteractiveIsShownOnlyIfHeuristicIsMissed()
- TestProgramMetaConstructs. testASTWalker()
- MasterHandlerTest. [10] float.sinDouble.props
- MasterHandlerTest. [11] float.sqrt1.props
- MasterHandlerTest. [12] float.sqrt2.props
- MasterHandlerTest. [13] float1.props
- MasterHandlerTest. [14] float2.props
- MasterHandlerTest. [15] heap1.props
- MasterHandlerTest. [16] int1.props
- MasterHandlerTest. [17] ite1.props
- MasterHandlerTest. [18] quant1.props
- MasterHandlerTest. [19] quant2.props
- MasterHandlerTest. [1] bool1.props
- MasterHandlerTest. [20] types1.props
- MasterHandlerTest. [21] types2.props
- MasterHandlerTest. [22] uninterpreted1.props
- MasterHandlerTest. [23] upd1.props
- MasterHandlerTest. [24] upd2.props
- MasterHandlerTest. [2] bool2.props
- MasterHandlerTest. [3] bool3.props
- MasterHandlerTest. [4] cast1.props
- MasterHandlerTest. [5] cast2.props
- MasterHandlerTest. [6] cast3.props
- MasterHandlerTest. [7] ex1.props
- MasterHandlerTest. [8] ex2.props
- MasterHandlerTest. [9] float.eq.props
- 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()