Class de.uka.ilkd.key.proof.proverules.ProveRulesTest

all > de.uka.ilkd.key.proof.proverules > ProveRulesTest
196

tests
0

failures
0

ignored
15m10.52s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 4.380s passed
powPositiveConcrete data()[101] 4.409s passed
powGeq1Concrete data()[102] 4.469s passed
pow2InIntLower data()[103] 4.346s passed
pow2InIntUpper data()[104] 4.420s passed
logSelfConcrete data()[105] 4.484s passed
log1Concrete data()[106] 4.351s passed
logProduct data()[107] 4.477s passed
logTimesBaseConcrete data()[108] 4.412s passed
logProdIdentity data()[109] 4.501s passed
moduloByteIsInByte data()[10] 4.607s passed
logProdIdentityConcrete data()[110] 4.509s passed
logPowIdentity data()[111] 4.470s passed
logPowIdentityConcrete data()[112] 4.481s passed
logPositive data()[113] 4.448s passed
logPositiveConcrete data()[114] 4.374s passed
logMono data()[115] 4.533s passed
logMonoConcrete data()[116] 4.445s passed
powLogLess data()[117] 4.402s passed
powLogMore2 data()[118] 4.437s passed
logLessThanPow data()[119] 4.548s passed
moduloCharIsInChar data()[11] 4.608s passed
logLessThanPowConcrete data()[120] 4.550s passed
logSqueeze data()[121] 4.466s passed
ifthenelse_equals data()[122] 4.374s passed
ifthenelse_equals_1 data()[123] 4.472s passed
ifthenelse_equals_2 data()[124] 4.387s passed
disjointWithSingleton1 data()[125] 4.338s passed
disjointWithSingleton2 data()[126] 4.559s passed
disjointArrayRanges data()[127] 4.545s passed
disjointArrayRangeAllFields1 data()[128] 4.424s passed
disjointArrayRangeAllFields2 data()[129] 4.528s passed
div_unique1 data()[12] 4.669s passed
seqSelfDefinition data()[130] 4.414s passed
seqOutsideValue data()[131] 4.461s passed
castedGetAny data()[132] 4.413s passed
seqGetAlphaCast data()[133] 4.439s passed
getOfSeqSingleton data()[134] 4.453s passed
getOfSeqSingletonConcrete data()[135] 4.497s passed
getOfSeqConcat data()[136] 4.435s passed
getOfSeqSub data()[137] 4.416s passed
getOfSeqReverse data()[138] 4.410s passed
lenOfSeqEmpty data()[139] 4.485s passed
div_unique2 data()[13] 4.748s passed
lenOfSeqSingleton data()[140] 4.403s passed
lenOfSeqConcat data()[141] 4.406s passed
lenOfSeqSub data()[142] 4.404s passed
lenOfSeqReverse data()[143] 4.453s passed
equalityToSeqGetAndSeqLenLeft data()[144] 4.495s passed
equalityToSeqGetAndSeqLenRight data()[145] 4.481s passed
getOfSeqSingletonEQ data()[146] 4.424s passed
getOfSeqConcatEQ data()[147] 4.478s passed
getOfSeqSubEQ data()[148] 4.395s passed
getOfSeqReverseEQ data()[149] 4.489s passed
div_exists data()[14] 4.798s passed
lenOfSeqEmptyEQ data()[150] 4.511s passed
lenOfSeqSingletonEQ data()[151] 4.471s passed
lenOfSeqConcatEQ data()[152] 4.551s passed
lenOfSeqSubEQ data()[153] 4.513s passed
lenOfSeqReverseEQ data()[154] 4.531s passed
getOfSeqDefEQ data()[155] 4.480s passed
lenOfSeqDefEQ data()[156] 4.486s passed
seqConcatWithSeqEmpty1 data()[157] 4.506s passed
seqConcatWithSeqEmpty2 data()[158] 4.629s passed
seqReverseOfSeqEmpty data()[159] 4.525s passed
div_one data()[15] 4.542s passed
subSeqComplete data()[160] 4.407s passed
subSeqTailR data()[161] 4.578s passed
subSeqTailL data()[162] 4.426s passed
subSeqTailEQR data()[163] 4.538s passed
subSeqTailEQL data()[164] 4.409s passed
seqDef_split data()[165] 4.451s passed
seqDef_induction_upper data()[166] 4.483s passed
seqDef_induction_upper_concrete data()[167] 4.545s passed
seqDef_induction_lower data()[168] 4.576s passed
seqDef_induction_lower_concrete data()[169] 4.603s passed
jdiv_one data()[16] 4.456s passed
seqDef_split_in_three data()[170] 4.756s passed
seqDef_empty data()[171] 4.528s passed
seqDef_one_summand data()[172] 4.412s passed
seqDef_lower_equals_upper data()[173] 4.402s passed
seqDefOfSeq data()[174] 4.440s passed
seqSelfDefinitionEQ2 data()[175] 4.457s passed
indexOfSeqSingleton data()[176] 4.457s passed
indexOfSeqConcatFirst data()[177] 4.610s passed
indexOfSeqConcatSecond data()[178] 4.580s passed
indexOfSeqSub data()[179] 4.538s passed
div_zero data()[17] 4.703s passed
lenOfArray2seq data()[180] 4.435s passed
getAnyOfArray2seq data()[181] 4.448s passed
getOfArray2seq data()[182] 4.552s passed
getAnyOfNPermInv data()[183] 4.475s passed
seqNPermRange data()[184] 4.538s passed
seqPermTrans data()[185] 4.617s passed
seqPermRefl data()[186] 4.495s passed
seqPermSplit data()[187] 4.450s passed
seqNPermRight data()[188] 5.073s passed
seqPermFromSwap data()[189] 4.672s passed
divResZero1 data()[18] 4.424s passed
seqPermTransAlt0 data()[190] 4.430s passed
seqPermTransAlt1 data()[191] 4.437s passed
seqPermTransAlt2 data()[192] 4.559s passed
seqPermTransAlt3 data()[193] 4.492s passed
schiffl_lemma_2 data()[194] 27.891s passed
schiffl_thm_1 data()[195] 5.239s passed
eqSameSeq data()[196] 4.709s passed
divResZero2 data()[19] 4.424s passed
eqTermCut data()[1] 5.274s passed
divResOne1 data()[20] 4.546s passed
divResOne2 data()[21] 4.435s passed
div_cancel1 data()[22] 4.605s passed
div_cancel2 data()[23] 4.607s passed
divAddMultDenom data()[24] 4.642s passed
divMinus data()[25] 4.565s passed
divMinusDenom data()[26] 4.707s passed
divLeastDPos data()[27] 4.397s passed
divLeastDNeg data()[28] 4.583s passed
divGreatestDPos data()[29] 4.606s passed
equivAllRight data()[2] 4.948s passed
divGreatestDNeg data()[30] 4.625s passed
divIncreasingPos data()[31] 4.652s passed
divIncreasingNeg data()[32] 4.651s passed
jdiv_zero data()[33] 4.576s passed
jdivPulloutMinusNum data()[34] 4.537s passed
jdivPulloutMinusDenom data()[35] 4.634s passed
jdiv_uniquePosPos data()[36] 4.562s passed
jdiv_uniquePosNeg data()[37] 4.652s passed
jdiv_uniqueNegPos data()[38] 4.431s passed
jdiv_uniqueNegNeg data()[39] 4.646s passed
irrflConcrete1 data()[3] 4.934s passed
jdivMultDenom1 data()[40] 4.573s passed
jdivMultDenom2 data()[41] 4.465s passed
mod_geZero data()[42] 4.561s passed
mod_lessDenom data()[43] 4.474s passed
jmod_NumPos data()[44] 4.380s passed
jmod_NumNeg data()[45] 4.430s passed
jmod_geZero data()[46] 4.362s passed
jmodNumZero data()[47] 4.524s passed
jmod_pulloutminusNum data()[48] 4.453s passed
jmod_pulloutminusDenom data()[49] 4.451s passed
irrflConcrete2 data()[4] 4.842s passed
jmodUnique1 data()[50] 4.706s passed
jmodUnique2 data()[51] 4.860s passed
intDivRem data()[52] 4.387s passed
jmodjmod data()[53] 4.471s passed
jmodDivisible data()[54] 4.496s passed
jmodDivisibleRep data()[55] 4.416s passed
jdivAddMultDenom data()[56] 4.933s passed
jmodAltZero data()[57] 4.475s passed
jmodAddMultDenomZero data()[58] 4.440s passed
polyDiv_zero data()[59] 4.416s passed
cancel_gtPos data()[5] 4.927s passed
polyMod_ltdivDenom data()[60] 4.460s passed
bsum_empty data()[61] 4.494s passed
bsum_induction_upper data()[62] 4.557s passed
bsum_induction_lower data()[63] 4.405s passed
bsum_num_of_bounds data()[64] 4.576s passed
bsum_num_of_bounds2 data()[65] 4.539s passed
bsum_induction_upper2 data()[66] 4.451s passed
bsum_induction_upper_concrete data()[67] 4.419s passed
bsum_induction_upper_concrete_2 data()[68] 4.401s passed
bsum_induction_upper2_concrete data()[69] 4.457s passed
cancel_gtNeg data()[6] 4.821s passed
bsum_induction_lower_concrete data()[70] 4.485s passed
bsum_induction_lower2 data()[71] 4.433s passed
bsum_induction_lower2_concrete data()[72] 4.445s passed
bsum_positive data()[73] 4.463s passed
bsum_upper_bound data()[74] 4.462s passed
bsum_lower_bound data()[75] 4.500s passed
bsum_positive_lower_bound_element data()[76] 4.516s passed
bsum_sub_same_index data()[77] 4.495s passed
bsum_less_same_index data()[78] 4.592s passed
bsum_equal_except_one_index data()[79] 4.427s passed
moduloIntIsInInt data()[7] 4.771s passed
bsum_num_of_is_max data()[80] 4.481s passed
bsum_num_of_is_max2 data()[81] 4.530s passed
bsum_num_of_is_max3 data()[82] 4.654s passed
bsum_num_of_is_max4 data()[83] 4.639s passed
bsum_num_of_lt_max data()[84] 4.492s passed
bsum_num_of_lt_max2 data()[85] 4.580s passed
bsum_num_of_lt_max3 data()[86] 4.430s passed
bsum_num_of_lt_max4 data()[87] 4.497s passed
bsum_num_of_gt0 data()[88] 4.496s passed
bsum_num_of_gt0_alt data()[89] 4.502s passed
moduloLongIsInLong data()[8] 4.650s passed
bsum_add_concrete data()[90] 4.581s passed
bprod_all_positive data()[91] 4.372s passed
bprod_split data()[92] 4.523s passed
powConcrete0 data()[93] 4.428s passed
powConcrete1 data()[94] 4.531s passed
powSplitFactor data()[95] 4.556s passed
powAdd data()[96] 4.471s passed
powMono data()[97] 4.438s passed
powMonoConcrete data()[98] 4.376s passed
powMonoConcreteRight data()[99] 4.411s passed
moduloShortIsInShort data()[9] 4.571s passed

Standard output

08:43:41,998 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.6
08:43:42,024 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
08:43:42,038 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Found resource [logback.xml] at [file:/home/runner/work/key/key/key.core/build/resources/test/logback.xml]
08:43:42,234 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
08:43:42,234 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
08:43:42,267 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
08:43:42,267 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
08:43:42,268 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
08:43:42,289 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
08:43:42,302 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
08:43:42,303 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@5c48c0c0 - End of configuration.
08:43:42,304 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@10c8f62 - Registering current configuration as safe fallback point

898        WARN  Test worker     d.u.i.k.s.ProofSettings   No proof-settings could be loaded, using defaults java.io.FileNotFoundException: /home/runner/.key/proof-settings.props (No such file or directory)
	at java.base/java.io.FileInputStream.open0(Native Method)