Test Summary

3046

tests

failures

102

ignored

8m5.17s

duration

98%

successful

Failed tests
Ignored tests
Packages
Classes

Failed tests

TestOneStepSimplifier. loadWithRestriction()
TestProofBundleIO. testComplexBundleGeneration()
TestProofBundleIO. testSimpleBundleGeneration()
TestApplyTaclet. testTacletWithIf()
LoopScopeInvRuleTests. testDoAutomaticProofOfBenchmarkWithLabeledBreaksAndContinues()
MergeRuleTests. testDoAutomaticGcdProofWithMergePointStatementAndBlockContract()
MergeRuleTests. testDoAutomaticGcdProofWithMergePointStatements()
MergeRuleTests. testDoManualGcdProof()
MergeRuleTests. testLoadClosedGcdProofWithMergePointStatements()
MergeRuleTests. testLoadGcdProof()
MergeRuleTests. testLoadGcdProofWithPredAbstr()
MergeRuleTests. testLoadGcdProofWithPredAbstrAndUserChoices()
MergeRuleTests. testLoadProofWithDiffVarsWithSameNameAndMPS()
MergeRuleTests. testMergeIndistinguishablePathConditionsWithFullAnonymization()
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)
TestProofStarter. testDirectProof()
TestProofStarter. testDirectProofWithOneStepSimplification()

Ignored tests

Packages

Package	Tests	Failures	Ignored	Duration	Success rate
de.uka.ilkd.key.java	24	0	1	12.099s	100%
de.uka.ilkd.key.java.recoderext	3	0	0	0.028s	100%
de.uka.ilkd.key.java.visitor	1	0	0	0.009s	100%
de.uka.ilkd.key.logic	138	0	2	1m53.97s	100%
de.uka.ilkd.key.macros.scripts	11	0	0	33.512s	100%
de.uka.ilkd.key.macros.scripts.meta	5	0	0	7.519s	100%
de.uka.ilkd.key.nparser	2057	0	0	7.685s	100%
de.uka.ilkd.key.parser	196	0	7	1m13.59s	100%
de.uka.ilkd.key.parser.messages	3	0	3	0.001s	-
de.uka.ilkd.key.parser.proofjava	4	0	0	0.021s	100%
de.uka.ilkd.key.pp	1	0	0	0s	100%
de.uka.ilkd.key.proof	11	1	1	6.319s	90%
de.uka.ilkd.key.proof.io	1	0	0	9.049s	100%
de.uka.ilkd.key.proof.io.consistency	3	2	0	4.873s	33%
de.uka.ilkd.key.rule	56	1	0	8.203s	98%
de.uka.ilkd.key.rule.conditions	3	0	0	0.009s	100%
de.uka.ilkd.key.rule.inst	8	0	0	0.012s	100%
de.uka.ilkd.key.rule.loop	1	1	0	5.673s	0%
de.uka.ilkd.key.rule.match.legacy	4	0	0	1.490s	100%
de.uka.ilkd.key.rule.match.vm	6	0	0	0.007s	100%
de.uka.ilkd.key.rule.merge	14	9	0	57.669s	35%
de.uka.ilkd.key.rule.metaconstruct	7	0	1	0.034s	100%
de.uka.ilkd.key.rule.tacletbuilder	5	0	0	4.982s	100%
de.uka.ilkd.key.smt	22	0	0	0.016s	100%
de.uka.ilkd.key.smt.communication	5	0	0	0.004s	100%
de.uka.ilkd.key.smt.newsmt2	73	25	24	1m33.45s	48%
de.uka.ilkd.key.smt.test	58	0	58	0.059s	-
de.uka.ilkd.key.speclang	3	0	0	11.152s	100%
de.uka.ilkd.key.speclang.jml	47	0	2	3.874s	100%
de.uka.ilkd.key.speclang.jml.pretranslation	1	0	0	0.009s	100%
de.uka.ilkd.key.speclang.njml	222	0	0	18.570s	100%
de.uka.ilkd.key.strategy.quantifierHeuristics	2	0	1	0.023s	100%
de.uka.ilkd.key.taclettranslation	5	0	0	0.023s	100%
de.uka.ilkd.key.taclettranslation.lemma	1	0	0	0.011s	100%
de.uka.ilkd.key.util	35	2	2	11.224s	93%
de.uka.ilkd.key.util.pp	10	0	0	0.003s	100%

Classes

Class	Tests	Failures	Ignored	Duration	Success rate
de.uka.ilkd.key.java.ProofJavaProgramFactoryTest	5	0	0	1.933s	100%
de.uka.ilkd.key.java.TestContextStatementBlock	1	0	0	1.492s	100%
de.uka.ilkd.key.java.TestJavaCardDLJavaExtensions	2	0	0	7.908s	100%
de.uka.ilkd.key.java.TestJavaInfo	9	0	0	0.016s	100%
de.uka.ilkd.key.java.TestKeYRecoderMapping	2	0	0	0.007s	100%
de.uka.ilkd.key.java.TestPositions	1	0	0	0.078s	100%
de.uka.ilkd.key.java.TestRecoder2KeY	4	0	1	0.665s	100%
de.uka.ilkd.key.java.recoderext.TestEnumClassDeclaration	3	0	0	0.028s	100%
de.uka.ilkd.key.java.visitor.TestDeclarationProgramVariableCollector	1	0	0	0.009s	100%
de.uka.ilkd.key.logic.LabeledTermImplTest	2	0	0	0.024s	100%
de.uka.ilkd.key.logic.TestClashFreeSubst	14	0	2	13.812s	100%
de.uka.ilkd.key.logic.TestLocalSymbols	2	0	0	6.581s	100%
de.uka.ilkd.key.logic.TestName	1	0	0	0.001s	100%
de.uka.ilkd.key.logic.TestNamespace	4	0	0	0.004s	100%
de.uka.ilkd.key.logic.TestPosInOcc	2	0	0	0s	100%
de.uka.ilkd.key.logic.TestPosInProgram	31	0	0	0.052s	100%
de.uka.ilkd.key.logic.TestPosInTerm	7	0	0	0.009s	100%
de.uka.ilkd.key.logic.TestSemisequent	15	0	0	0.015s	100%
de.uka.ilkd.key.logic.TestSyntacticalReplaceVisitor	2	0	0	0.003s	100%
de.uka.ilkd.key.logic.TestTerm	9	0	0	0.374s	100%
de.uka.ilkd.key.logic.TestTermBuilder	6	0	0	22.129s	100%
de.uka.ilkd.key.logic.TestTermFactory	19	0	0	0.029s	100%
de.uka.ilkd.key.logic.TestTermLabelManager	21	0	0	1m10.93s	100%
de.uka.ilkd.key.logic.TestVariableNamer	3	0	0	0.004s	100%
de.uka.ilkd.key.macros.scripts.FocusCommandTest	2	0	0	7.408s	100%
de.uka.ilkd.key.macros.scripts.SMTCommandTest	1	0	0	0.001s	100%
de.uka.ilkd.key.macros.scripts.ScriptLineParserTest	1	0	0	0.001s	100%
de.uka.ilkd.key.macros.scripts.TestProofScriptCommand	7	0	0	26.102s	100%
de.uka.ilkd.key.macros.scripts.meta.RewriteTest	2	0	0	7.517s	100%
de.uka.ilkd.key.macros.scripts.meta.ValueInjectorTest	3	0	0	0.002s	100%
de.uka.ilkd.key.nparser.ExprTest	23	0	0	3.439s	100%
de.uka.ilkd.key.nparser.ParseLDTsTests	2	0	0	1.514s	100%
de.uka.ilkd.key.nparser.TestTacletEquality	2032	0	0	2.732s	100%
de.uka.ilkd.key.parser.TestDeclParser	14	0	2	14.049s	100%
de.uka.ilkd.key.parser.TestIntLiteralParsing	67	0	0	0.066s	100%
de.uka.ilkd.key.parser.TestJMLParserAssociativity	1	0	0	36.516s	100%
de.uka.ilkd.key.parser.TestParallelParsing	1	0	0	16.217s	100%
de.uka.ilkd.key.parser.TestParser	5	0	1	6.066s	100%
de.uka.ilkd.key.parser.TestTacletParser	20	0	0	0.083s	100%
de.uka.ilkd.key.parser.TestTermParser	47	0	4	0.319s	100%
de.uka.ilkd.key.parser.TestTermParserHeap	39	0	0	0.248s	100%
de.uka.ilkd.key.parser.TestTermParserSorts	2	0	0	0.028s	100%
de.uka.ilkd.key.parser.messages.ParserMessageTest	3	0	3	0.001s	-
de.uka.ilkd.key.parser.proofjava.TestProofJavaParser	4	0	0	0.021s	100%
de.uka.ilkd.key.pp.PrettyPrinterTest	1	0	0	0s	100%
de.uka.ilkd.key.proof.TestGoal	2	0	0	0.038s	100%
de.uka.ilkd.key.proof.TestOneStepSimplifier	1	1	0	5.015s	0%
de.uka.ilkd.key.proof.TestProofTree	1	0	0	0.014s	100%
de.uka.ilkd.key.proof.TestTacletIndex	5	0	1	1.247s	100%
de.uka.ilkd.key.proof.TestTermTacletAppIndex	2	0	0	0.005s	100%
de.uka.ilkd.key.proof.io.TestZipProofSaving	1	0	0	9.049s	100%
de.uka.ilkd.key.proof.io.consistency.TestProofBundleIO	3	2	0	4.873s	33%
de.uka.ilkd.key.rule.TestApplyTaclet	29	1	0	5.265s	96%
de.uka.ilkd.key.rule.TestCollisionResolving	7	0	0	0.042s	100%
de.uka.ilkd.key.rule.TestMatchTaclet	16	0	0	1.352s	100%
de.uka.ilkd.key.rule.TestSchemaModalOperators	4	0	0	1.544s	100%
de.uka.ilkd.key.rule.conditions.TestDropEffectlessElementary	3	0	0	0.009s	100%
de.uka.ilkd.key.rule.inst.TestGenericSortInstantiations	8	0	0	0.012s	100%
de.uka.ilkd.key.rule.loop.LoopScopeInvRuleTests	1	1	0	5.673s	0%
de.uka.ilkd.key.rule.match.legacy.TestLegacyTacletMatch	4	0	0	1.490s	100%
de.uka.ilkd.key.rule.match.vm.VMTacletMatcherTest	6	0	0	0.007s	100%
de.uka.ilkd.key.rule.merge.MergeRuleTests	11	9	0	50.105s	18%
de.uka.ilkd.key.rule.merge.PredicateAbstractionLatticeTests	3	0	0	7.564s	100%
de.uka.ilkd.key.rule.metaconstruct.TestProgramMetaConstructs	7	0	1	0.034s	100%
de.uka.ilkd.key.rule.tacletbuilder.TestTacletBuild	5	0	0	4.982s	100%
de.uka.ilkd.key.smt.SMTBeautifierTest	22	0	0	0.016s	100%
de.uka.ilkd.key.smt.communication.BufferedMessageReaderTest	5	0	0	0.004s	100%
de.uka.ilkd.key.smt.newsmt2.MasterHandlerTest	48	0	24	0.444s	100%
de.uka.ilkd.key.smt.newsmt2.ProveSMTLemmasTest	25	25	0	1m33.00s	0%
de.uka.ilkd.key.smt.test.TestCvc4	27	0	27	0.031s	-
de.uka.ilkd.key.smt.test.TestZ3	31	0	31	0.028s	-
de.uka.ilkd.key.speclang.ContractFactoryTest	3	0	0	11.152s	100%
de.uka.ilkd.key.speclang.jml.JMLUtilsTest	2	0	0	0.006s	100%
de.uka.ilkd.key.speclang.jml.TestJMLPreTranslator	20	0	2	0.038s	100%
de.uka.ilkd.key.speclang.jml.TestJMLTranslator	25	0	0	3.830s	100%
de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLAssertStatementTest	1	0	0	0.009s	100%
de.uka.ilkd.key.speclang.njml.ClasslevelTranslatorTest	184	0	0	1.335s	100%
de.uka.ilkd.key.speclang.njml.ContractLoadingTests	4	0	0	17.062s	100%
de.uka.ilkd.key.speclang.njml.ExpressionTranslatorTest	14	0	0	0.045s	100%
de.uka.ilkd.key.speclang.njml.MethodlevelTranslatorTest	13	0	0	0.112s	100%
de.uka.ilkd.key.speclang.njml.NJmlTranslatorTests	5	0	0	0.012s	100%
de.uka.ilkd.key.speclang.njml.TextualTranslatorTest	2	0	0	0.004s	100%
de.uka.ilkd.key.strategy.quantifierHeuristics.TestTriggersSet	2	0	1	0.023s	100%
de.uka.ilkd.key.taclettranslation.TestTacletTranslator	5	0	0	0.023s	100%
de.uka.ilkd.key.taclettranslation.lemma.TestGenericRemovingLemmaGenerator	1	0	0	0.011s	100%
de.uka.ilkd.key.util.DesignTests	3	0	1	1.116s	100%
de.uka.ilkd.key.util.TestLexicographicComparator	1	0	0	0s	100%
de.uka.ilkd.key.util.TestMiscTools	9	0	0	0.074s	100%
de.uka.ilkd.key.util.TestNodePreorderIterator	4	0	0	0.025s	100%
de.uka.ilkd.key.util.TestProofStarter	2	2	0	9.944s	0%
de.uka.ilkd.key.util.TestProofUserManager	3	0	1	0.027s	100%
de.uka.ilkd.key.util.TestSearchNodePreorderIterator	4	0	0	0.019s	100%
de.uka.ilkd.key.util.TestSearchNodeReversePreorderIterator	4	0	0	0.018s	100%
de.uka.ilkd.key.util.TestVersionStringComparator	5	0	0	0.001s	100%
de.uka.ilkd.key.util.pp.TestLayouter	10	0	0	0.003s	100%