Test Summary
|
99%
successful |
Failed tests
- 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()
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] bool2.props
- MasterHandlerTest. [11] float2.props
- MasterHandlerTest. [12] cast1.props
- MasterHandlerTest. [13] uninterpreted1.props
- MasterHandlerTest. [14] bool3.props
- MasterHandlerTest. [15] heap1.props
- MasterHandlerTest. [16] quant1.props
- MasterHandlerTest. [17] ex2.props
- MasterHandlerTest. [18] bool1.props
- MasterHandlerTest. [19] types1.props
- MasterHandlerTest. [1] upd2.props
- MasterHandlerTest. [20] ite1.props
- MasterHandlerTest. [21] float.eq.props
- MasterHandlerTest. [22] float1.props
- MasterHandlerTest. [23] float.sinDouble.props
- MasterHandlerTest. [24] cast3.props
- MasterHandlerTest. [2] quant2.props
- MasterHandlerTest. [3] ex1.props
- MasterHandlerTest. [4] float.sqrt2.props
- MasterHandlerTest. [5] types2.props
- MasterHandlerTest. [6] upd1.props
- MasterHandlerTest. [7] int1.props
- MasterHandlerTest. [8] float.sqrt1.props
- MasterHandlerTest. [9] cast2.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()
- TestTriggersSet. testTrigger2()
- DesignTests. xtestTermSubclassVisibility()
- TestProofUserManager. testUserManagement_NoEnvironment()