Test Summary

3023

tests

failures

104

ignored

7m12.64s

duration

98%

successful

Failed tests
Ignored tests
Packages
Classes

Failed tests

TestTacletEquality. [1532] postdecrement_array, postdecrement_array { \find(#allmodal ( (modal operator))\[{ .. #e[#e0]--; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#e0 (program Expression))), \new(#v (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e (program Expression)); #v = #e; #typeof( #e0 (program Expression)); #v0 = #e0; #v[#v0] = (#typeof( #e[#e0]);) (#v[#v0] - 1); ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
TestTacletEquality. [1534] postdecrement_assignment_array, postdecrement_assignment_array { \find(#allmodal ( (modal operator))\[{ .. #lhs0 = #e[#e0]--; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#lhs0 (program LeftHandSide))), \new(#v0 (program Variable), \typeof(#e0 (program Expression))), \new(#v (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e (program Expression)); #v = #e; #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #lhs0 (program LeftHandSide)); #v1 = #…
TestTacletEquality. [1538] postincrement_array, postincrement_array { \find(#allmodal ( (modal operator))\[{ .. #e[#e0]++; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#e0 (program Expression))), \new(#v (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e (program Expression)); #v = #e; #typeof( #e0 (program Expression)); #v0 = #e0; #v[#v0] = (#typeof( #e[#e0]);) (#v[#v0] + 1); ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
TestTacletEquality. [1540] postincrement_assignment_array, postincrement_assignment_array { \find(#allmodal ( (modal operator))\[{ .. #lhs0 = #e[#e0]++; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#lhs0 (program LeftHandSide))), \new(#v0 (program Variable), \typeof(#e0 (program Expression))), \new(#v (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e (program Expression)); #v = #e; #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #lhs0 (program LeftHandSide)); #v1 = #…
TestTacletEquality. [1576] predecrement_array, predecrement_array { \find(#allmodal ( (modal operator))\[{ .. --#e[#e0]; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#e0 (program Expression))), \new(#v (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e (program Expression)); #v = #e; #typeof( #e0 (program Expression)); #v0 = #e0; #v[#v0] = (#typeof( #e[#e0]);) (#v[#v0] - 1); ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
TestTacletEquality. [1578] predecrement_assignment_array, predecrement_assignment_array { \find(#allmodal ( (modal operator))\[{ .. #lhs0 = --#e[#e0]; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#e0 (program Expression))), \new(#v (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e (program Expression)); #v = #e; #typeof( #e0 (program Expression)); #v0 = #e0; #v[#v0] = (#typeof( #e[#e0]);) (#v[#v0] - 1); #lhs0 = #v[#v0]; ... }\] (post)) \heuristics(simplify_expression) Ch…
TestTacletEquality. [1582] preincrement_array, preincrement_array { \find(#allmodal ( (modal operator))\[{ .. ++#e[#e0]; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#e0 (program Expression))), \new(#v (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e (program Expression)); #v = #e; #typeof( #e0 (program Expression)); #v0 = #e0; #v[#v0] = (#typeof( #e[#e0]);) (#v[#v0] + 1); ... }\] (post)) \heuristics(simplify_expression) Choices: programRules:Java}
TestTacletEquality. [1584] preincrement_assignment_array, preincrement_assignment_array { \find(#allmodal ( (modal operator))\[{ .. #lhs0 = ++#e[#e0]; ... }\] (post)) \varcond(\new(#v0 (program Variable), \typeof(#e0 (program Expression))), \new(#v (program Variable), \typeof(#e (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e (program Expression)); #v = #e; #typeof( #e0 (program Expression)); #v0 = #e0; #v[#v0] = (#typeof( #e[#e0]);) (#v[#v0] + 1); #lhs0 = #v[#v0]; ... }\] (post)) \heuristics(simplify_expression) Ch…
TestTacletEquality. [423] compound_assignment_op_and_array, compound_assignment_op_and_array { \find(#allmodal ( (modal operator))\[{ .. #e0[#e] &= #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] & #e1); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules…
TestTacletEquality. [426] compound_assignment_op_div_array, compound_assignment_op_div_array { \find(#allmodal ( (modal operator))\[{ .. #e0[#e] /= #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] / #e1); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules…
TestTacletEquality. [429] compound_assignment_op_minus_array, compound_assignment_op_minus_array { \find(#allmodal ( (modal operator))\[{ .. #e0[#e] -= #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] - #e1); ... }\] (post)) \heuristics(simplify_prog) Choices: programRul…
TestTacletEquality. [432] compound_assignment_op_mod_array, compound_assignment_op_mod_array { \find(#allmodal ( (modal operator))\[{ .. #e0[#e] %= #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] % #e1); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules…
TestTacletEquality. [435] compound_assignment_op_mul_array, compound_assignment_op_mul_array { \find(#allmodal ( (modal operator))\[{ .. #e0[#e] *= #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] * #e1); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules…
TestTacletEquality. [438] compound_assignment_op_or_array, compound_assignment_op_or_array { \find(#allmodal ( (modal operator))\[{ .. #e0[#e] |= #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] | #e1); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules:…
TestTacletEquality. [441] compound_assignment_op_plus_array, compound_assignment_op_plus_array { \find(#allmodal ( (modal operator))\[{ .. #e0[#e] += #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] + #e1); ... }\] (post)) \heuristics(simplify_prog) Choices: programRule…
TestTacletEquality. [444] compound_assignment_op_shiftleft_array, compound_assignment_op_shiftleft_array { \find(#allmodal ( (modal operator))\[{ .. #e0[#e] <<= #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] << #e1); ... }\] (post)) \heuristics(simplify_prog) Choices: prog…
TestTacletEquality. [447] compound_assignment_op_shiftright_array, compound_assignment_op_shiftright_array { \find(#allmodal ( (modal operator))\[{ .. #e0[#e] >>= #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] >> #e1); ... }\] (post)) \heuristics(simplify_prog) Choices: pro…
TestTacletEquality. [450] compound_assignment_op_unsigned_shiftright_array, compound_assignment_op_unsigned_shiftright_array { \find(#allmodal ( (modal operator))\[{ .. #e0[#e] >>>= #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] >>> #e1); ... }\] (post)) \heuristics(simplify_prog) C…
TestTacletEquality. [453] compound_assignment_op_xor_array, compound_assignment_op_xor_array { \find(#allmodal ( (modal operator))\[{ .. #e0[#e] ^= #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] ^ #e1); ... }\] (post)) \heuristics(simplify_prog) Choices: programRules…
TestTacletEquality. [818] eval_order_iterated_assignments_10_0, eval_order_iterated_assignments_10_0 { \find(#allmodal ( (modal operator))\[{ .. #lhs0 = #e0[#e] |= #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] | #e1); #lhs0 = #v0[#v1]; ... }\] (post)) \heuristics(simp…
TestTacletEquality. [820] eval_order_iterated_assignments_11_0, eval_order_iterated_assignments_11_0 { \find(#allmodal ( (modal operator))\[{ .. #lhs0 = #e0[#e] ^= #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] ^ #e1); #lhs0 = #v0[#v1]; ... }\] (post)) \heuristics(simp…
TestTacletEquality. [822] eval_order_iterated_assignments_1_0, eval_order_iterated_assignments_1_0 { \find(#allmodal ( (modal operator))\[{ .. #lhs0 = #e0[#e] *= #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] * #e1); #lhs0 = #v0[#v1]; ... }\] (post)) \heuristics(simpl…
TestTacletEquality. [824] eval_order_iterated_assignments_2_0, eval_order_iterated_assignments_2_0 { \find(#allmodal ( (modal operator))\[{ .. #lhs0 = #e0[#e] /= #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] / #e1); #lhs0 = #v0[#v1]; ... }\] (post)) \heuristics(simpl…
TestTacletEquality. [826] eval_order_iterated_assignments_3_0, eval_order_iterated_assignments_3_0 { \find(#allmodal ( (modal operator))\[{ .. #lhs0 = #e0[#e] %= #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] % #e1); #lhs0 = #v0[#v1]; ... }\] (post)) \heuristics(simpl…
TestTacletEquality. [828] eval_order_iterated_assignments_4_0, eval_order_iterated_assignments_4_0 { \find(#allmodal ( (modal operator))\[{ .. #lhs0 = #e0[#e] += #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] + #e1); #lhs0 = #v0[#v1]; ... }\] (post)) \heuristics(simpl…
TestTacletEquality. [830] eval_order_iterated_assignments_5_0, eval_order_iterated_assignments_5_0 { \find(#allmodal ( (modal operator))\[{ .. #lhs0 = #e0[#e] -= #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] - #e1); #lhs0 = #v0[#v1]; ... }\] (post)) \heuristics(simpl…
TestTacletEquality. [832] eval_order_iterated_assignments_6_0, eval_order_iterated_assignments_6_0 { \find(#allmodal ( (modal operator))\[{ .. #lhs0 = #e0[#e] <<= #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] << #e1); #lhs0 = #v0[#v1]; ... }\] (post)) \heuristics(sim…
TestTacletEquality. [834] eval_order_iterated_assignments_7_0, eval_order_iterated_assignments_7_0 { \find(#allmodal ( (modal operator))\[{ .. #lhs0 = #e0[#e] >>= #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] >> #e1); #lhs0 = #v0[#v1]; ... }\] (post)) \heuristics(sim…
TestTacletEquality. [836] eval_order_iterated_assignments_8_0, eval_order_iterated_assignments_8_0 { \find(#allmodal ( (modal operator))\[{ .. #lhs0 = #e0[#e] >>>= #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] >>> #e1); #lhs0 = #v0[#v1]; ... }\] (post)) \heuristics(s…
TestTacletEquality. [838] eval_order_iterated_assignments_9_0, eval_order_iterated_assignments_9_0 { \find(#allmodal ( (modal operator))\[{ .. #lhs0 = #e0[#e] &= #e1; ... }\] (post)) \varcond(\new(#v1 (program Variable), \typeof(#e (program Expression))), \new(#v0 (program Variable), \typeof(#e0 (program Expression)))) \replacewith(#allmodal ( (modal operator))\[{ .. #typeof( #e0 (program Expression)); #v0 = #e0; #typeof( #e (program Expression)); #v1 = #e; #v0[#v1] = (#typeof( #e0[#e]);) (#v0[#v1] & #e1); #lhs0 = #v0[#v1]; ... }\] (post)) \heuristics(simpl…

Ignored tests

Packages

Package	Tests	Failures	Ignored	Duration	Success rate
de.uka.ilkd.key.java	23	0	1	8.223s	100%
de.uka.ilkd.key.java.recoderext	3	0	0	0.013s	100%
de.uka.ilkd.key.java.visitor	1	0	0	0.005s	100%
de.uka.ilkd.key.logic	137	0	2	1m26.12s	100%
de.uka.ilkd.key.macros.scripts	11	0	0	25.769s	100%
de.uka.ilkd.key.macros.scripts.meta	5	0	0	5.732s	100%
de.uka.ilkd.key.nparser	2041	30	0	5.028s	98%
de.uka.ilkd.key.parser	196	0	7	57.014s	100%
de.uka.ilkd.key.parser.messages	3	0	3	0s	-
de.uka.ilkd.key.parser.proofjava	4	0	0	0.008s	100%
de.uka.ilkd.key.proof	10	0	3	0.917s	100%
de.uka.ilkd.key.proof.io	1	0	0	6.968s	100%
de.uka.ilkd.key.proof.io.consistency	3	0	0	7.075s	100%
de.uka.ilkd.key.rule	56	0	0	4.611s	100%
de.uka.ilkd.key.rule.conditions	3	0	0	0.003s	100%
de.uka.ilkd.key.rule.inst	8	0	0	0.009s	100%
de.uka.ilkd.key.rule.loop	1	0	0	4.484s	100%
de.uka.ilkd.key.rule.match.legacy	4	0	0	1.109s	100%
de.uka.ilkd.key.rule.match.vm	6	0	0	0.005s	100%
de.uka.ilkd.key.rule.merge	14	0	0	1m11.31s	100%
de.uka.ilkd.key.rule.metaconstruct	7	0	1	0.008s	100%
de.uka.ilkd.key.rule.tacletbuilder	5	0	0	3.795s	100%
de.uka.ilkd.key.smt	22	0	0	0.003s	100%
de.uka.ilkd.key.smt.communication	5	0	0	0.001s	100%
de.uka.ilkd.key.smt.newsmt2	73	0	24	1m12.43s	100%
de.uka.ilkd.key.smt.test	58	0	58	0.013s	-
de.uka.ilkd.key.speclang	3	0	0	8.548s	100%
de.uka.ilkd.key.speclang.jml	47	0	2	2.985s	100%
de.uka.ilkd.key.speclang.jml.pretranslation	1	0	0	0.006s	100%
de.uka.ilkd.key.speclang.njml	219	0	0	14.312s	100%
de.uka.ilkd.key.strategy.quantifierHeuristics	2	0	1	0.002s	100%
de.uka.ilkd.key.taclettranslation	5	0	0	0.006s	100%
de.uka.ilkd.key.taclettranslation.lemma	1	0	0	0.003s	100%
de.uka.ilkd.key.util	35	0	2	46.121s	100%
de.uka.ilkd.key.util.pp	10	0	0	0s	100%

Classes

Class	Tests	Failures	Ignored	Duration	Success rate
de.uka.ilkd.key.java.ProofJavaProgramFactoryTest	5	0	0	0.714s	100%
de.uka.ilkd.key.java.TestContextStatementBlock	1	0	0	1.067s	100%
de.uka.ilkd.key.java.TestJavaCardDLJavaExtensions	2	0	0	5.935s	100%
de.uka.ilkd.key.java.TestJavaInfo	9	0	0	0.006s	100%
de.uka.ilkd.key.java.TestKeYRecoderMapping	2	0	0	0.001s	100%
de.uka.ilkd.key.java.TestRecoder2KeY	4	0	1	0.500s	100%
de.uka.ilkd.key.java.recoderext.TestEnumClassDeclaration	3	0	0	0.013s	100%
de.uka.ilkd.key.java.visitor.TestDeclarationProgramVariableCollector	1	0	0	0.005s	100%
de.uka.ilkd.key.logic.LabeledTermImplTest	2	0	0	0.002s	100%
de.uka.ilkd.key.logic.TestClashFreeSubst	14	0	2	10.593s	100%
de.uka.ilkd.key.logic.TestLocalSymbols	1	0	0	4.129s	100%
de.uka.ilkd.key.logic.TestName	1	0	0	0.001s	100%
de.uka.ilkd.key.logic.TestNamespace	4	0	0	0.010s	100%
de.uka.ilkd.key.logic.TestPosInOcc	2	0	0	0.001s	100%
de.uka.ilkd.key.logic.TestPosInProgram	31	0	0	0.058s	100%
de.uka.ilkd.key.logic.TestPosInTerm	7	0	0	0.007s	100%
de.uka.ilkd.key.logic.TestSemisequent	15	0	0	0.006s	100%
de.uka.ilkd.key.logic.TestSyntacticalReplaceVisitor	2	0	0	0.010s	100%
de.uka.ilkd.key.logic.TestTerm	9	0	0	0.013s	100%
de.uka.ilkd.key.logic.TestTermBuilder	6	0	0	16.741s	100%
de.uka.ilkd.key.logic.TestTermFactory	19	0	0	0.015s	100%
de.uka.ilkd.key.logic.TestTermLabelManager	21	0	0	54.532s	100%
de.uka.ilkd.key.logic.TestVariableNamer	3	0	0	0.004s	100%
de.uka.ilkd.key.macros.scripts.FocusCommandTest	2	0	0	5.685s	100%
de.uka.ilkd.key.macros.scripts.SMTCommandTest	1	0	0	0s	100%
de.uka.ilkd.key.macros.scripts.ScriptLineParserTest	1	0	0	0.002s	100%
de.uka.ilkd.key.macros.scripts.TestProofScriptCommand	7	0	0	20.082s	100%
de.uka.ilkd.key.macros.scripts.meta.RewriteTest	2	0	0	5.728s	100%
de.uka.ilkd.key.macros.scripts.meta.ValueInjectorTest	3	0	0	0.004s	100%
de.uka.ilkd.key.nparser.ExprTest	23	0	0	2.122s	100%
de.uka.ilkd.key.nparser.ParseLDTsTests	2	0	0	0.732s	100%
de.uka.ilkd.key.nparser.TestTacletEquality	2016	30	0	2.174s	98%
de.uka.ilkd.key.parser.TestDeclParser	14	0	2	10.947s	100%
de.uka.ilkd.key.parser.TestIntLiteralParsing	67	0	0	0.049s	100%
de.uka.ilkd.key.parser.TestJMLParserAssociativity	1	0	0	28.428s	100%
de.uka.ilkd.key.parser.TestParallelParsing	1	0	0	12.543s	100%
de.uka.ilkd.key.parser.TestParser	5	0	1	4.717s	100%
de.uka.ilkd.key.parser.TestTacletParser	20	0	0	0.065s	100%
de.uka.ilkd.key.parser.TestTermParser	47	0	4	0.173s	100%
de.uka.ilkd.key.parser.TestTermParserHeap	39	0	0	0.079s	100%
de.uka.ilkd.key.parser.TestTermParserSorts	2	0	0	0.013s	100%
de.uka.ilkd.key.parser.messages.ParserMessageTest	3	0	3	0s	-
de.uka.ilkd.key.parser.proofjava.TestProofJavaParser	4	0	0	0.008s	100%
de.uka.ilkd.key.proof.TestGoal	2	0	2	0s	-
de.uka.ilkd.key.proof.TestProofTree	1	0	0	0.005s	100%
de.uka.ilkd.key.proof.TestTacletIndex	5	0	1	0.910s	100%
de.uka.ilkd.key.proof.TestTermTacletAppIndex	2	0	0	0.002s	100%
de.uka.ilkd.key.proof.io.TestZipProofSaving	1	0	0	6.968s	100%
de.uka.ilkd.key.proof.io.consistency.TestProofBundleIO	3	0	0	7.075s	100%
de.uka.ilkd.key.rule.TestApplyTaclet	29	0	0	2.514s	100%
de.uka.ilkd.key.rule.TestCollisionResolving	7	0	0	0.019s	100%
de.uka.ilkd.key.rule.TestMatchTaclet	16	0	0	1.118s	100%
de.uka.ilkd.key.rule.TestSchemaModalOperators	4	0	0	0.960s	100%
de.uka.ilkd.key.rule.conditions.TestDropEffectlessElementary	3	0	0	0.003s	100%
de.uka.ilkd.key.rule.inst.TestGenericSortInstantiations	8	0	0	0.009s	100%
de.uka.ilkd.key.rule.loop.LoopScopeInvRuleTests	1	0	0	4.484s	100%
de.uka.ilkd.key.rule.match.legacy.TestLegacyTacletMatch	4	0	0	1.109s	100%
de.uka.ilkd.key.rule.match.vm.VMTacletMatcherTest	6	0	0	0.005s	100%
de.uka.ilkd.key.rule.merge.MergeRuleTests	11	0	0	1m5.58s	100%
de.uka.ilkd.key.rule.merge.PredicateAbstractionLatticeTests	3	0	0	5.734s	100%
de.uka.ilkd.key.rule.metaconstruct.TestProgramMetaConstructs	7	0	1	0.008s	100%
de.uka.ilkd.key.rule.tacletbuilder.TestTacletBuild	5	0	0	3.795s	100%
de.uka.ilkd.key.smt.SMTBeautifierTest	22	0	0	0.003s	100%
de.uka.ilkd.key.smt.communication.BufferedMessageReaderTest	5	0	0	0.001s	100%
de.uka.ilkd.key.smt.newsmt2.MasterHandlerTest	48	0	24	0.012s	100%
de.uka.ilkd.key.smt.newsmt2.ProveSMTLemmasTest	25	0	0	1m12.42s	100%
de.uka.ilkd.key.smt.test.TestCvc4	27	0	27	0.008s	-
de.uka.ilkd.key.smt.test.TestZ3	31	0	31	0.005s	-
de.uka.ilkd.key.speclang.ContractFactoryTest	3	0	0	8.548s	100%
de.uka.ilkd.key.speclang.jml.JMLUtilsTest	2	0	0	0.003s	100%
de.uka.ilkd.key.speclang.jml.TestJMLPreTranslator	20	0	2	0.024s	100%
de.uka.ilkd.key.speclang.jml.TestJMLTranslator	25	0	0	2.958s	100%
de.uka.ilkd.key.speclang.jml.pretranslation.TextualJMLAssertStatementTest	1	0	0	0.006s	100%
de.uka.ilkd.key.speclang.njml.ClasslevelTranslatorTest	184	0	0	1.068s	100%
de.uka.ilkd.key.speclang.njml.ContractLoadingTests	4	0	0	13.122s	100%
de.uka.ilkd.key.speclang.njml.ExpressionTranslatorTest	14	0	0	0.033s	100%
de.uka.ilkd.key.speclang.njml.MethodlevelTranslatorTest	13	0	0	0.083s	100%
de.uka.ilkd.key.speclang.njml.NJmlTranslatorTests	2	0	0	0.003s	100%
de.uka.ilkd.key.speclang.njml.TextualTranslatorTest	2	0	0	0.003s	100%
de.uka.ilkd.key.strategy.quantifierHeuristics.TestTriggersSet	2	0	1	0.002s	100%
de.uka.ilkd.key.taclettranslation.TestTacletTranslator	5	0	0	0.006s	100%
de.uka.ilkd.key.taclettranslation.lemma.TestGenericRemovingLemmaGenerator	1	0	0	0.003s	100%
de.uka.ilkd.key.util.DesignTests	3	0	1	0.318s	100%
de.uka.ilkd.key.util.TestLexicographicComparator	1	0	0	0.001s	100%
de.uka.ilkd.key.util.TestMiscTools	9	0	0	0.017s	100%
de.uka.ilkd.key.util.TestNodePreorderIterator	4	0	0	0.008s	100%
de.uka.ilkd.key.util.TestProofStarter	2	0	0	45.767s	100%
de.uka.ilkd.key.util.TestProofUserManager	3	0	1	0.003s	100%
de.uka.ilkd.key.util.TestSearchNodePreorderIterator	4	0	0	0.003s	100%
de.uka.ilkd.key.util.TestSearchNodeReversePreorderIterator	4	0	0	0.003s	100%
de.uka.ilkd.key.util.TestVersionStringComparator	5	0	0	0.001s	100%
de.uka.ilkd.key.util.pp.TestLayouter	10	0	0	0s	100%