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

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

tests
0

failures
0

ignored
13m45.11s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 3.973s passed
powPositiveConcrete data()[101] 4.009s passed
powGeq1Concrete data()[102] 3.964s passed
pow2InIntLower data()[103] 4.103s passed
pow2InIntUpper data()[104] 4.111s passed
logSelfConcrete data()[105] 4.024s passed
log1Concrete data()[106] 4.254s passed
logProduct data()[107] 4.278s passed
logTimesBaseConcrete data()[108] 4.271s passed
logProdIdentity data()[109] 4.042s passed
moduloByteIsInByte data()[10] 4.115s passed
logProdIdentityConcrete data()[110] 4.276s passed
logPowIdentity data()[111] 4.231s passed
logPowIdentityConcrete data()[112] 4.268s passed
logPositive data()[113] 4.228s passed
logPositiveConcrete data()[114] 4.067s passed
logMono data()[115] 4.050s passed
logMonoConcrete data()[116] 4.029s passed
powLogLess data()[117] 4.028s passed
powLogMore2 data()[118] 4.007s passed
logLessThanPow data()[119] 4.143s passed
moduloCharIsInChar data()[11] 4.096s passed
logLessThanPowConcrete data()[120] 3.998s passed
logSqueeze data()[121] 4.061s passed
ifthenelse_equals data()[122] 3.982s passed
ifthenelse_equals_1 data()[123] 4.026s passed
ifthenelse_equals_2 data()[124] 4.066s passed
disjointWithSingleton1 data()[125] 3.939s passed
disjointWithSingleton2 data()[126] 3.902s passed
disjointArrayRanges data()[127] 4.013s passed
disjointArrayRangeAllFields1 data()[128] 4.083s passed
disjointArrayRangeAllFields2 data()[129] 3.992s passed
div_unique1 data()[12] 4.134s passed
seqSelfDefinition data()[130] 3.935s passed
seqOutsideValue data()[131] 3.952s passed
castedGetAny data()[132] 3.964s passed
seqGetAlphaCast data()[133] 3.983s passed
getOfSeqSingleton data()[134] 4.008s passed
getOfSeqSingletonConcrete data()[135] 3.958s passed
getOfSeqConcat data()[136] 3.976s passed
getOfSeqSub data()[137] 4.084s passed
getOfSeqReverse data()[138] 4.046s passed
lenOfSeqEmpty data()[139] 3.929s passed
div_unique2 data()[13] 4.291s passed
lenOfSeqSingleton data()[140] 3.928s passed
lenOfSeqConcat data()[141] 3.910s passed
lenOfSeqSub data()[142] 4.028s passed
lenOfSeqReverse data()[143] 4.010s passed
equalityToSeqGetAndSeqLenLeft data()[144] 4.094s passed
equalityToSeqGetAndSeqLenRight data()[145] 4.072s passed
getOfSeqSingletonEQ data()[146] 4.133s passed
getOfSeqConcatEQ data()[147] 4.073s passed
getOfSeqSubEQ data()[148] 3.953s passed
getOfSeqReverseEQ data()[149] 3.950s passed
div_exists data()[14] 4.470s passed
lenOfSeqEmptyEQ data()[150] 4.013s passed
lenOfSeqSingletonEQ data()[151] 3.946s passed
lenOfSeqConcatEQ data()[152] 3.968s passed
lenOfSeqSubEQ data()[153] 3.975s passed
lenOfSeqReverseEQ data()[154] 4.031s passed
getOfSeqDefEQ data()[155] 3.991s passed
lenOfSeqDefEQ data()[156] 4.010s passed
seqConcatWithSeqEmpty1 data()[157] 3.967s passed
seqConcatWithSeqEmpty2 data()[158] 3.972s passed
seqReverseOfSeqEmpty data()[159] 3.939s passed
div_one data()[15] 4.162s passed
subSeqComplete data()[160] 4.013s passed
subSeqTailR data()[161] 3.985s passed
subSeqTailL data()[162] 4.021s passed
subSeqTailEQR data()[163] 4.132s passed
subSeqTailEQL data()[164] 4.177s passed
seqDef_split data()[165] 4.318s passed
seqDef_induction_upper data()[166] 4.083s passed
seqDef_induction_upper_concrete data()[167] 4.115s passed
seqDef_induction_lower data()[168] 4.237s passed
seqDef_induction_lower_concrete data()[169] 4.342s passed
jdiv_one data()[16] 4.125s passed
seqDef_split_in_three data()[170] 4.533s passed
seqDef_empty data()[171] 4.256s passed
seqDef_one_summand data()[172] 4.264s passed
seqDef_lower_equals_upper data()[173] 4.186s passed
seqDefOfSeq data()[174] 4.294s passed
seqSelfDefinitionEQ2 data()[175] 4.117s passed
indexOfSeqSingleton data()[176] 3.966s passed
indexOfSeqConcatFirst data()[177] 4.023s passed
indexOfSeqConcatSecond data()[178] 4.013s passed
indexOfSeqSub data()[179] 4.040s passed
div_zero data()[17] 4.236s passed
lenOfArray2seq data()[180] 3.974s passed
getAnyOfArray2seq data()[181] 3.959s passed
getOfArray2seq data()[182] 4.042s passed
getAnyOfNPermInv data()[183] 4.157s passed
seqNPermRange data()[184] 4.071s passed
seqPermTrans data()[185] 4.122s passed
seqPermRefl data()[186] 4.068s passed
seqPermSplit data()[187] 3.978s passed
seqNPermRight data()[188] 4.482s passed
seqPermFromSwap data()[189] 4.223s passed
divResZero1 data()[18] 4.166s passed
seqPermTransAlt0 data()[190] 4.071s passed
seqPermTransAlt1 data()[191] 4.119s passed
seqPermTransAlt2 data()[192] 4.075s passed
seqPermTransAlt3 data()[193] 3.953s passed
schiffl_lemma_2 data()[194] 24.005s passed
schiffl_thm_1 data()[195] 5.002s passed
eqSameSeq data()[196] 4.135s passed
divResZero2 data()[19] 4.115s passed
eqTermCut data()[1] 5.189s passed
divResOne1 data()[20] 4.155s passed
divResOne2 data()[21] 4.088s passed
div_cancel1 data()[22] 4.033s passed
div_cancel2 data()[23] 4.066s passed
divAddMultDenom data()[24] 4.227s passed
divMinus data()[25] 4.242s passed
divMinusDenom data()[26] 4.290s passed
divLeastDPos data()[27] 4.135s passed
divLeastDNeg data()[28] 4.247s passed
divGreatestDPos data()[29] 4.204s passed
equivAllRight data()[2] 4.474s passed
divGreatestDNeg data()[30] 4.131s passed
divIncreasingPos data()[31] 4.168s passed
divIncreasingNeg data()[32] 4.087s passed
jdiv_zero data()[33] 4.040s passed
jdivPulloutMinusNum data()[34] 4.131s passed
jdivPulloutMinusDenom data()[35] 4.189s passed
jdiv_uniquePosPos data()[36] 4.173s passed
jdiv_uniquePosNeg data()[37] 4.150s passed
jdiv_uniqueNegPos data()[38] 4.113s passed
jdiv_uniqueNegNeg data()[39] 4.138s passed
irrflConcrete1 data()[3] 4.451s passed
jdivMultDenom1 data()[40] 4.120s passed
jdivMultDenom2 data()[41] 4.037s passed
mod_geZero data()[42] 4.003s passed
mod_lessDenom data()[43] 4.093s passed
jmod_NumPos data()[44] 3.945s passed
jmod_NumNeg data()[45] 4.080s passed
jmod_geZero data()[46] 4.083s passed
jmodNumZero data()[47] 4.038s passed
jmod_pulloutminusNum data()[48] 4.002s passed
jmod_pulloutminusDenom data()[49] 3.996s passed
irrflConcrete2 data()[4] 4.323s passed
jmodUnique1 data()[50] 4.298s passed
jmodUnique2 data()[51] 4.494s passed
intDivRem data()[52] 4.157s passed
jmodjmod data()[53] 4.170s passed
jmodDivisible data()[54] 4.289s passed
jmodDivisibleRep data()[55] 4.265s passed
jdivAddMultDenom data()[56] 4.492s passed
jmodAltZero data()[57] 4.252s passed
jmodAddMultDenomZero data()[58] 4.279s passed
polyDiv_zero data()[59] 4.298s passed
cancel_gtPos data()[5] 4.372s passed
polyMod_ltdivDenom data()[60] 4.334s passed
bsum_empty data()[61] 4.004s passed
bsum_induction_upper data()[62] 3.995s passed
bsum_induction_lower data()[63] 4.067s passed
bsum_num_of_bounds data()[64] 4.134s passed
bsum_num_of_bounds2 data()[65] 3.975s passed
bsum_induction_upper2 data()[66] 3.943s passed
bsum_induction_upper_concrete data()[67] 3.944s passed
bsum_induction_upper_concrete_2 data()[68] 3.978s passed
bsum_induction_upper2_concrete data()[69] 4.007s passed
cancel_gtNeg data()[6] 4.292s passed
bsum_induction_lower_concrete data()[70] 4.076s passed
bsum_induction_lower2 data()[71] 3.975s passed
bsum_induction_lower2_concrete data()[72] 3.956s passed
bsum_positive data()[73] 4.168s passed
bsum_upper_bound data()[74] 4.167s passed
bsum_lower_bound data()[75] 4.079s passed
bsum_positive_lower_bound_element data()[76] 4.165s passed
bsum_sub_same_index data()[77] 4.061s passed
bsum_less_same_index data()[78] 4.074s passed
bsum_equal_except_one_index data()[79] 3.942s passed
moduloIntIsInInt data()[7] 4.195s passed
bsum_num_of_is_max data()[80] 4.013s passed
bsum_num_of_is_max2 data()[81] 3.990s passed
bsum_num_of_is_max3 data()[82] 3.903s passed
bsum_num_of_is_max4 data()[83] 4.158s passed
bsum_num_of_lt_max data()[84] 4.113s passed
bsum_num_of_lt_max2 data()[85] 4.060s passed
bsum_num_of_lt_max3 data()[86] 3.947s passed
bsum_num_of_lt_max4 data()[87] 4.019s passed
bsum_num_of_gt0 data()[88] 4.047s passed
bsum_num_of_gt0_alt data()[89] 3.997s passed
moduloLongIsInLong data()[8] 4.141s passed
bsum_add_concrete data()[90] 4.084s passed
bprod_all_positive data()[91] 4.036s passed
bprod_split data()[92] 4.092s passed
powConcrete0 data()[93] 3.991s passed
powConcrete1 data()[94] 4.044s passed
powSplitFactor data()[95] 3.945s passed
powAdd data()[96] 4.021s passed
powMono data()[97] 4.044s passed
powMonoConcrete data()[98] 4.010s passed
powMonoConcreteRight data()[99] 3.960s passed
moduloShortIsInShort data()[9] 4.077s passed

Standard error

SLF4J: No SLF4J providers were found.
SLF4J: Defaulting to no-operation (NOP) logger implementation
SLF4J: See https://www.slf4j.org/codes.html#noProviders for further details.
SLF4J: Class path contains SLF4J bindings targeting slf4j-api versions 1.7.x or earlier.
SLF4J: Ignoring binding found at [jar:file:/home/runner/.gradle/caches/modules-2/files-2.1/ch.qos.logback/logback-classic/1.2.10/f69d97ef3335c6ab82fc21dfb77ac613f90c1221/logback-classic-1.2.10.jar!/org/slf4j/impl/StaticLoggerBinder.class]
SLF4J: See https://www.slf4j.org/codes.html#ignoredBindings for an explanation.