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

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

tests
0

failures
0

ignored
14m55.52s

duration
100%

successful

Tests

Test Method name Duration Result
powPositive data()[100] 4.363s passed
powPositiveConcrete data()[101] 4.393s passed
powGeq1Concrete data()[102] 4.331s passed
pow2InIntLower data()[103] 4.389s passed
pow2InIntUpper data()[104] 4.385s passed
logSelfConcrete data()[105] 4.460s passed
log1Concrete data()[106] 4.434s passed
logProduct data()[107] 4.439s passed
logTimesBaseConcrete data()[108] 4.422s passed
logProdIdentity data()[109] 4.416s passed
moduloByteIsInByte data()[10] 4.436s passed
logProdIdentityConcrete data()[110] 4.300s passed
logPowIdentity data()[111] 4.422s passed
logPowIdentityConcrete data()[112] 4.405s passed
logPositive data()[113] 4.369s passed
logPositiveConcrete data()[114] 4.268s passed
logMono data()[115] 4.468s passed
logMonoConcrete data()[116] 4.333s passed
powLogLess data()[117] 4.363s passed
powLogMore2 data()[118] 4.399s passed
logLessThanPow data()[119] 4.455s passed
moduloCharIsInChar data()[11] 4.467s passed
logLessThanPowConcrete data()[120] 4.329s passed
logSqueeze data()[121] 4.262s passed
ifthenelse_equals data()[122] 4.319s passed
ifthenelse_equals_1 data()[123] 4.314s passed
ifthenelse_equals_2 data()[124] 4.315s passed
disjointWithSingleton1 data()[125] 4.395s passed
disjointWithSingleton2 data()[126] 4.362s passed
disjointArrayRanges data()[127] 4.427s passed
disjointArrayRangeAllFields1 data()[128] 4.489s passed
disjointArrayRangeAllFields2 data()[129] 4.321s passed
div_unique1 data()[12] 4.548s passed
seqSelfDefinition data()[130] 4.357s passed
seqOutsideValue data()[131] 4.387s passed
castedGetAny data()[132] 4.389s passed
seqGetAlphaCast data()[133] 4.466s passed
getOfSeqSingleton data()[134] 4.463s passed
getOfSeqSingletonConcrete data()[135] 4.540s passed
getOfSeqConcat data()[136] 4.448s passed
getOfSeqSub data()[137] 4.455s passed
getOfSeqReverse data()[138] 4.443s passed
lenOfSeqEmpty data()[139] 4.472s passed
div_unique2 data()[13] 4.528s passed
lenOfSeqSingleton data()[140] 4.402s passed
lenOfSeqConcat data()[141] 4.421s passed
lenOfSeqSub data()[142] 4.416s passed
lenOfSeqReverse data()[143] 4.405s passed
equalityToSeqGetAndSeqLenLeft data()[144] 4.373s passed
equalityToSeqGetAndSeqLenRight data()[145] 4.364s passed
getOfSeqSingletonEQ data()[146] 4.405s passed
getOfSeqConcatEQ data()[147] 4.411s passed
getOfSeqSubEQ data()[148] 4.353s passed
getOfSeqReverseEQ data()[149] 4.356s passed
div_exists data()[14] 4.746s passed
lenOfSeqEmptyEQ data()[150] 4.357s passed
lenOfSeqSingletonEQ data()[151] 4.410s passed
lenOfSeqConcatEQ data()[152] 4.419s passed
lenOfSeqSubEQ data()[153] 4.397s passed
lenOfSeqReverseEQ data()[154] 4.373s passed
getOfSeqDefEQ data()[155] 4.375s passed
lenOfSeqDefEQ data()[156] 4.366s passed
seqConcatWithSeqEmpty1 data()[157] 4.408s passed
seqConcatWithSeqEmpty2 data()[158] 4.428s passed
seqReverseOfSeqEmpty data()[159] 4.465s passed
div_one data()[15] 4.424s passed
subSeqComplete data()[160] 4.442s passed
subSeqTailR data()[161] 4.451s passed
subSeqTailL data()[162] 4.425s passed
subSeqTailEQR data()[163] 4.419s passed
subSeqTailEQL data()[164] 4.363s passed
seqDef_split data()[165] 4.449s passed
seqDef_induction_upper data()[166] 4.456s passed
seqDef_induction_upper_concrete data()[167] 4.473s passed
seqDef_induction_lower data()[168] 4.458s passed
seqDef_induction_lower_concrete data()[169] 4.467s passed
jdiv_one data()[16] 4.473s passed
seqDef_split_in_three data()[170] 4.744s passed
seqDef_empty data()[171] 4.420s passed
seqDef_one_summand data()[172] 4.342s passed
seqDef_lower_equals_upper data()[173] 4.405s passed
seqDefOfSeq data()[174] 4.491s passed
seqSelfDefinitionEQ2 data()[175] 4.469s passed
indexOfSeqSingleton data()[176] 4.486s passed
indexOfSeqConcatFirst data()[177] 4.454s passed
indexOfSeqConcatSecond data()[178] 4.537s passed
indexOfSeqSub data()[179] 4.514s passed
div_zero data()[17] 4.487s passed
lenOfArray2seq data()[180] 4.488s passed
getAnyOfArray2seq data()[181] 4.490s passed
getOfArray2seq data()[182] 4.391s passed
getAnyOfNPermInv data()[183] 4.543s passed
seqNPermRange data()[184] 4.596s passed
seqPermTrans data()[185] 4.812s passed
seqPermRefl data()[186] 5.151s passed
seqPermSplit data()[187] 5.022s passed
seqNPermRight data()[188] 5.006s passed
seqPermFromSwap data()[189] 4.725s passed
divResZero1 data()[18] 4.475s passed
seqPermTransAlt0 data()[190] 4.414s passed
seqPermTransAlt1 data()[191] 4.466s passed
seqPermTransAlt2 data()[192] 4.380s passed
seqPermTransAlt3 data()[193] 4.449s passed
schiffl_lemma_2 data()[194] 26.545s passed
schiffl_thm_1 data()[195] 5.485s passed
eqSameSeq data()[196] 4.453s passed
divResZero2 data()[19] 4.534s passed
eqTermCut data()[1] 5.173s passed
divResOne1 data()[20] 4.505s passed
divResOne2 data()[21] 4.475s passed
div_cancel1 data()[22] 4.465s passed
div_cancel2 data()[23] 4.403s passed
divAddMultDenom data()[24] 4.511s passed
divMinus data()[25] 4.494s passed
divMinusDenom data()[26] 4.473s passed
divLeastDPos data()[27] 4.409s passed
divLeastDNeg data()[28] 4.421s passed
divGreatestDPos data()[29] 4.411s passed
equivAllRight data()[2] 4.911s passed
divGreatestDNeg data()[30] 4.438s passed
divIncreasingPos data()[31] 4.389s passed
divIncreasingNeg data()[32] 4.522s passed
jdiv_zero data()[33] 4.453s passed
jdivPulloutMinusNum data()[34] 4.415s passed
jdivPulloutMinusDenom data()[35] 4.465s passed
jdiv_uniquePosPos data()[36] 4.406s passed
jdiv_uniquePosNeg data()[37] 4.432s passed
jdiv_uniqueNegPos data()[38] 4.430s passed
jdiv_uniqueNegNeg data()[39] 4.439s passed
irrflConcrete1 data()[3] 4.798s passed
jdivMultDenom1 data()[40] 4.441s passed
jdivMultDenom2 data()[41] 4.395s passed
mod_geZero data()[42] 4.339s passed
mod_lessDenom data()[43] 4.448s passed
jmod_NumPos data()[44] 4.373s passed
jmod_NumNeg data()[45] 4.399s passed
jmod_geZero data()[46] 4.320s passed
jmodNumZero data()[47] 4.370s passed
jmod_pulloutminusNum data()[48] 4.365s passed
jmod_pulloutminusDenom data()[49] 4.370s passed
irrflConcrete2 data()[4] 4.718s passed
jmodUnique1 data()[50] 4.597s passed
jmodUnique2 data()[51] 4.697s passed
intDivRem data()[52] 4.366s passed
jmodjmod data()[53] 4.527s passed
jmodDivisible data()[54] 4.418s passed
jmodDivisibleRep data()[55] 4.389s passed
jdivAddMultDenom data()[56] 4.735s passed
jmodAltZero data()[57] 4.465s passed
jmodAddMultDenomZero data()[58] 4.404s passed
polyDiv_zero data()[59] 4.428s passed
cancel_gtPos data()[5] 4.709s passed
polyMod_ltdivDenom data()[60] 4.421s passed
bsum_empty data()[61] 4.303s passed
bsum_induction_upper data()[62] 4.388s passed
bsum_induction_lower data()[63] 4.479s passed
bsum_num_of_bounds data()[64] 4.406s passed
bsum_num_of_bounds2 data()[65] 4.446s passed
bsum_induction_upper2 data()[66] 4.319s passed
bsum_induction_upper_concrete data()[67] 4.388s passed
bsum_induction_upper_concrete_2 data()[68] 4.405s passed
bsum_induction_upper2_concrete data()[69] 4.371s passed
cancel_gtNeg data()[6] 4.561s passed
bsum_induction_lower_concrete data()[70] 4.336s passed
bsum_induction_lower2 data()[71] 4.338s passed
bsum_induction_lower2_concrete data()[72] 4.342s passed
bsum_positive data()[73] 4.456s passed
bsum_upper_bound data()[74] 4.453s passed
bsum_lower_bound data()[75] 4.483s passed
bsum_positive_lower_bound_element data()[76] 4.424s passed
bsum_sub_same_index data()[77] 4.450s passed
bsum_less_same_index data()[78] 4.433s passed
bsum_equal_except_one_index data()[79] 4.367s passed
moduloIntIsInInt data()[7] 4.495s passed
bsum_num_of_is_max data()[80] 4.460s passed
bsum_num_of_is_max2 data()[81] 4.442s passed
bsum_num_of_is_max3 data()[82] 4.398s passed
bsum_num_of_is_max4 data()[83] 4.412s passed
bsum_num_of_lt_max data()[84] 4.419s passed
bsum_num_of_lt_max2 data()[85] 4.442s passed
bsum_num_of_lt_max3 data()[86] 4.372s passed
bsum_num_of_lt_max4 data()[87] 4.429s passed
bsum_num_of_gt0 data()[88] 4.392s passed
bsum_num_of_gt0_alt data()[89] 4.405s passed
moduloLongIsInLong data()[8] 4.499s passed
bsum_add_concrete data()[90] 4.390s passed
bprod_all_positive data()[91] 4.415s passed
bprod_split data()[92] 4.449s passed
powConcrete0 data()[93] 4.367s passed
powConcrete1 data()[94] 4.341s passed
powSplitFactor data()[95] 4.319s passed
powAdd data()[96] 4.392s passed
powMono data()[97] 4.360s passed
powMonoConcrete data()[98] 4.341s passed
powMonoConcreteRight data()[99] 4.322s passed
moduloShortIsInShort data()[9] 4.504s 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.