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

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

tests
0

failures
0

ignored
10m3.89s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 2.959s passed
powPositiveConcrete data()[101] 2.935s passed
powGeq1Concrete data()[102] 2.925s passed
pow2InIntLower data()[103] 2.936s passed
pow2InIntUpper data()[104] 2.938s passed
logSelfConcrete data()[105] 2.940s passed
log1Concrete data()[106] 2.931s passed
logProduct data()[107] 2.944s passed
logTimesBaseConcrete data()[108] 2.948s passed
logProdIdentity data()[109] 2.959s passed
moduloByteIsInByte data()[10] 2.991s passed
logProdIdentityConcrete data()[110] 2.944s passed
logPowIdentity data()[111] 2.925s passed
logPowIdentityConcrete data()[112] 2.935s passed
logPositive data()[113] 2.977s passed
logPositiveConcrete data()[114] 2.959s passed
logMono data()[115] 3.005s passed
logMonoConcrete data()[116] 2.950s passed
powLogLess data()[117] 2.972s passed
powLogMore2 data()[118] 2.972s passed
logLessThanPow data()[119] 3.001s passed
moduloCharIsInChar data()[11] 3.006s passed
logLessThanPowConcrete data()[120] 2.955s passed
logSqueeze data()[121] 2.960s passed
ifthenelse_equals data()[122] 2.929s passed
ifthenelse_equals_1 data()[123] 2.943s passed
ifthenelse_equals_2 data()[124] 2.942s passed
disjointWithSingleton1 data()[125] 2.955s passed
disjointWithSingleton2 data()[126] 2.935s passed
disjointArrayRanges data()[127] 2.977s passed
disjointArrayRangeAllFields1 data()[128] 2.960s passed
disjointArrayRangeAllFields2 data()[129] 2.948s passed
div_unique1 data()[12] 3.093s passed
seqSelfDefinition data()[130] 2.950s passed
seqOutsideValue data()[131] 2.949s passed
castedGetAny data()[132] 2.953s passed
seqGetAlphaCast data()[133] 2.962s passed
getOfSeqSingleton data()[134] 2.950s passed
getOfSeqSingletonConcrete data()[135] 2.944s passed
getOfSeqConcat data()[136] 2.950s passed
getOfSeqSub data()[137] 2.956s passed
getOfSeqReverse data()[138] 2.946s passed
lenOfSeqEmpty data()[139] 2.944s passed
div_unique2 data()[13] 3.103s passed
lenOfSeqSingleton data()[140] 2.942s passed
lenOfSeqConcat data()[141] 2.963s passed
lenOfSeqSub data()[142] 2.944s passed
lenOfSeqReverse data()[143] 2.945s passed
equalityToSeqGetAndSeqLenLeft data()[144] 2.938s passed
equalityToSeqGetAndSeqLenRight data()[145] 2.952s passed
getOfSeqSingletonEQ data()[146] 2.945s passed
getOfSeqConcatEQ data()[147] 2.951s passed
getOfSeqSubEQ data()[148] 2.954s passed
getOfSeqReverseEQ data()[149] 2.943s passed
div_exists data()[14] 3.261s passed
lenOfSeqEmptyEQ data()[150] 2.941s passed
lenOfSeqSingletonEQ data()[151] 2.951s passed
lenOfSeqConcatEQ data()[152] 2.945s passed
lenOfSeqSubEQ data()[153] 2.953s passed
lenOfSeqReverseEQ data()[154] 2.965s passed
getOfSeqDefEQ data()[155] 2.951s passed
lenOfSeqDefEQ data()[156] 2.944s passed
seqConcatWithSeqEmpty1 data()[157] 2.963s passed
seqConcatWithSeqEmpty2 data()[158] 2.947s passed
seqReverseOfSeqEmpty data()[159] 2.957s passed
div_one data()[15] 3.003s passed
subSeqComplete data()[160] 2.951s passed
subSeqTailR data()[161] 2.981s passed
subSeqTailL data()[162] 2.959s passed
subSeqTailEQR data()[163] 2.968s passed
subSeqTailEQL data()[164] 2.963s passed
seqDef_split data()[165] 2.998s passed
seqDef_induction_upper data()[166] 3.010s passed
seqDef_induction_upper_concrete data()[167] 2.992s passed
seqDef_induction_lower data()[168] 2.992s passed
seqDef_induction_lower_concrete data()[169] 2.983s passed
jdiv_one data()[16] 2.986s passed
seqDef_split_in_three data()[170] 3.194s passed
seqDef_empty data()[171] 2.976s passed
seqDef_one_summand data()[172] 2.955s passed
seqDef_lower_equals_upper data()[173] 2.951s passed
seqDefOfSeq data()[174] 2.988s passed
seqSelfDefinitionEQ2 data()[175] 2.963s passed
indexOfSeqSingleton data()[176] 2.947s passed
indexOfSeqConcatFirst data()[177] 2.972s passed
indexOfSeqConcatSecond data()[178] 2.984s passed
indexOfSeqSub data()[179] 2.981s passed
div_zero data()[17] 3.032s passed
lenOfArray2seq data()[180] 2.960s passed
getAnyOfArray2seq data()[181] 3.050s passed
getOfArray2seq data()[182] 2.942s passed
getAnyOfNPermInv data()[183] 2.941s passed
seqNPermRange data()[184] 3.029s passed
seqPermTrans data()[185] 3.042s passed
seqPermRefl data()[186] 2.958s passed
seqPermSplit data()[187] 2.958s passed
seqNPermRight data()[188] 3.298s passed
seqPermFromSwap data()[189] 3.095s passed
divResZero1 data()[18] 3.027s passed
seqPermTransAlt0 data()[190] 3.060s passed
seqPermTransAlt1 data()[191] 3.033s passed
seqPermTransAlt2 data()[192] 2.960s passed
seqPermTransAlt3 data()[193] 2.948s passed
schiffl_lemma_2 data()[194] 20.532s passed
schiffl_thm_1 data()[195] 3.677s passed
eqSameSeq data()[196] 3.041s passed
divResZero2 data()[19] 3.006s passed
eqTermCut data()[1] 3.482s passed
divResOne1 data()[20] 3.024s passed
divResOne2 data()[21] 2.989s passed
div_cancel1 data()[22] 3.001s passed
div_cancel2 data()[23] 2.975s passed
divAddMultDenom data()[24] 3.021s passed
divMinus data()[25] 3.042s passed
divMinusDenom data()[26] 3.036s passed
divLeastDPos data()[27] 2.975s passed
divLeastDNeg data()[28] 2.987s passed
divGreatestDPos data()[29] 2.995s passed
equivAllRight data()[2] 3.358s passed
divGreatestDNeg data()[30] 2.975s passed
divIncreasingPos data()[31] 2.965s passed
divIncreasingNeg data()[32] 2.956s passed
jdiv_zero data()[33] 2.959s passed
jdivPulloutMinusNum data()[34] 2.970s passed
jdivPulloutMinusDenom data()[35] 3.016s passed
jdiv_uniquePosPos data()[36] 3.008s passed
jdiv_uniquePosNeg data()[37] 2.989s passed
jdiv_uniqueNegPos data()[38] 2.975s passed
jdiv_uniqueNegNeg data()[39] 2.979s passed
irrflConcrete1 data()[3] 3.201s passed
jdivMultDenom1 data()[40] 3.000s passed
jdivMultDenom2 data()[41] 2.958s passed
mod_geZero data()[42] 2.986s passed
mod_lessDenom data()[43] 2.957s passed
jmod_NumPos data()[44] 2.960s passed
jmod_NumNeg data()[45] 2.980s passed
jmod_geZero data()[46] 2.952s passed
jmodNumZero data()[47] 2.990s passed
jmod_pulloutminusNum data()[48] 2.980s passed
jmod_pulloutminusDenom data()[49] 2.960s passed
irrflConcrete2 data()[4] 3.108s passed
jmodUnique1 data()[50] 3.072s passed
jmodUnique2 data()[51] 3.079s passed
intDivRem data()[52] 2.949s passed
jmodjmod data()[53] 3.019s passed
jmodDivisible data()[54] 2.979s passed
jmodDivisibleRep data()[55] 2.980s passed
jdivAddMultDenom data()[56] 3.159s passed
jmodAltZero data()[57] 2.958s passed
jmodAddMultDenomZero data()[58] 2.963s passed
polyDiv_zero data()[59] 2.968s passed
cancel_gtPos data()[5] 3.200s passed
polyMod_ltdivDenom data()[60] 2.960s passed
bsum_empty data()[61] 2.946s passed
bsum_induction_upper data()[62] 2.949s passed
bsum_induction_lower data()[63] 2.977s passed
bsum_num_of_bounds data()[64] 2.971s passed
bsum_num_of_bounds2 data()[65] 2.970s passed
bsum_induction_upper2 data()[66] 2.975s passed
bsum_induction_upper_concrete data()[67] 3.047s passed
bsum_induction_upper_concrete_2 data()[68] 2.926s passed
bsum_induction_upper2_concrete data()[69] 2.943s passed
cancel_gtNeg data()[6] 3.100s passed
bsum_induction_lower_concrete data()[70] 2.943s passed
bsum_induction_lower2 data()[71] 3.012s passed
bsum_induction_lower2_concrete data()[72] 2.964s passed
bsum_positive data()[73] 3.034s passed
bsum_upper_bound data()[74] 2.984s passed
bsum_lower_bound data()[75] 2.997s passed
bsum_positive_lower_bound_element data()[76] 2.983s passed
bsum_sub_same_index data()[77] 2.980s passed
bsum_less_same_index data()[78] 2.996s passed
bsum_equal_except_one_index data()[79] 2.966s passed
moduloIntIsInInt data()[7] 3.065s passed
bsum_num_of_is_max data()[80] 2.962s passed
bsum_num_of_is_max2 data()[81] 2.969s passed
bsum_num_of_is_max3 data()[82] 2.947s passed
bsum_num_of_is_max4 data()[83] 2.970s passed
bsum_num_of_lt_max data()[84] 2.978s passed
bsum_num_of_lt_max2 data()[85] 2.970s passed
bsum_num_of_lt_max3 data()[86] 2.986s passed
bsum_num_of_lt_max4 data()[87] 2.972s passed
bsum_num_of_gt0 data()[88] 2.953s passed
bsum_num_of_gt0_alt data()[89] 2.964s passed
moduloLongIsInLong data()[8] 3.044s passed
bsum_add_concrete data()[90] 2.957s passed
bprod_all_positive data()[91] 2.951s passed
bprod_split data()[92] 2.992s passed
powConcrete0 data()[93] 2.934s passed
powConcrete1 data()[94] 2.944s passed
powSplitFactor data()[95] 2.944s passed
powAdd data()[96] 2.930s passed
powMono data()[97] 2.991s passed
powMonoConcrete data()[98] 3.019s passed
powMonoConcreteRight data()[99] 2.953s passed
moduloShortIsInShort data()[9] 3.035s passed

Standard output

08:24:25,010 |-INFO in ch.qos.logback.classic.LoggerContext[default] - This is logback-classic version 1.4.5
08:24:25,079 |-INFO in ch.qos.logback.classic.LoggerContext[default] - Could NOT find resource [logback-test.xml]
08:24:25,089 |-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:24:25,911 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - Processing appender named [STDOUT]
08:24:25,911 |-INFO in ch.qos.logback.core.model.processor.AppenderModelHandler - About to instantiate appender of type [ch.qos.logback.core.ConsoleAppender]
08:24:25,922 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [file] in [ch.qos.logback.core.ConsoleAppender]
08:24:25,922 |-WARN in ch.qos.logback.core.model.processor.ImplicitModelHandler - Ignoring unknown property [append] in [ch.qos.logback.core.ConsoleAppender]
08:24:25,922 |-INFO in ch.qos.logback.core.model.processor.ImplicitModelHandler - Assuming default type [ch.qos.logback.classic.encoder.PatternLayoutEncoder] for [encoder] property
08:24:25,935 |-INFO in ch.qos.logback.classic.model.processor.RootLoggerModelHandler - Setting level of ROOT logger to WARN
08:24:25,939 |-INFO in ch.qos.logback.core.model.processor.AppenderRefModelHandler - Attaching appender named [STDOUT] to Logger[ROOT]
08:24:25,939 |-INFO in ch.qos.logback.core.model.processor.DefaultProcessor@6f80fafe - End of configuration.
08:24:25,940 |-INFO in ch.qos.logback.classic.joran.JoranConfigurator@3af17be2 - Registering current configuration as safe fallback point

1368       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)