Package de.uka.ilkd.key.proof.proverules
|
0%
successful |
Failed tests
- ProveRulesTest. powPositive
- ProveRulesTest. powPositiveConcrete
- ProveRulesTest. powGeq1Concrete
- ProveRulesTest. pow2InIntLower
- ProveRulesTest. pow2InIntUpper
- ProveRulesTest. logSelfConcrete
- ProveRulesTest. log1Concrete
- ProveRulesTest. logProduct
- ProveRulesTest. logTimesBaseConcrete
- ProveRulesTest. logProdIdentity
- ProveRulesTest. moduloByteIsInByte
- ProveRulesTest. logProdIdentityConcrete
- ProveRulesTest. logPowIdentity
- ProveRulesTest. logPowIdentityConcrete
- ProveRulesTest. logPositive
- ProveRulesTest. logPositiveConcrete
- ProveRulesTest. logMono
- ProveRulesTest. logMonoConcrete
- ProveRulesTest. powLogLess
- ProveRulesTest. powLogMore2
- ProveRulesTest. logLessThanPow
- ProveRulesTest. moduloCharIsInChar
- ProveRulesTest. logLessThanPowConcrete
- ProveRulesTest. logSqueeze
- ProveRulesTest. ifthenelse_equals
- ProveRulesTest. ifthenelse_equals_1
- ProveRulesTest. ifthenelse_equals_2
- ProveRulesTest. disjointWithSingleton1
- ProveRulesTest. disjointWithSingleton2
- ProveRulesTest. disjointArrayRanges
- ProveRulesTest. disjointArrayRangeAllFields1
- ProveRulesTest. disjointArrayRangeAllFields2
- ProveRulesTest. div_unique1
- ProveRulesTest. seqSelfDefinition
- ProveRulesTest. seqOutsideValue
- ProveRulesTest. castedGetAny
- ProveRulesTest. seqGetAlphaCast
- ProveRulesTest. getOfSeqSingleton
- ProveRulesTest. getOfSeqSingletonConcrete
- ProveRulesTest. getOfSeqConcat
- ProveRulesTest. getOfSeqSub
- ProveRulesTest. getOfSeqReverse
- ProveRulesTest. lenOfSeqEmpty
- ProveRulesTest. div_unique2
- ProveRulesTest. lenOfSeqSingleton
- ProveRulesTest. lenOfSeqConcat
- ProveRulesTest. lenOfSeqSub
- ProveRulesTest. lenOfSeqReverse
- ProveRulesTest. equalityToSeqGetAndSeqLenLeft
- ProveRulesTest. equalityToSeqGetAndSeqLenRight
- ProveRulesTest. getOfSeqSingletonEQ
- ProveRulesTest. getOfSeqConcatEQ
- ProveRulesTest. getOfSeqSubEQ
- ProveRulesTest. getOfSeqReverseEQ
- ProveRulesTest. div_exists
- ProveRulesTest. lenOfSeqEmptyEQ
- ProveRulesTest. lenOfSeqSingletonEQ
- ProveRulesTest. lenOfSeqConcatEQ
- ProveRulesTest. lenOfSeqSubEQ
- ProveRulesTest. lenOfSeqReverseEQ
- ProveRulesTest. getOfSeqDefEQ
- ProveRulesTest. lenOfSeqDefEQ
- ProveRulesTest. seqConcatWithSeqEmpty1
- ProveRulesTest. seqConcatWithSeqEmpty2
- ProveRulesTest. seqReverseOfSeqEmpty
- ProveRulesTest. div_one
- ProveRulesTest. subSeqComplete
- ProveRulesTest. subSeqTailR
- ProveRulesTest. subSeqTailL
- ProveRulesTest. subSeqTailEQR
- ProveRulesTest. subSeqTailEQL
- ProveRulesTest. seqDef_split
- ProveRulesTest. seqDef_induction_upper
- ProveRulesTest. seqDef_induction_upper_concrete
- ProveRulesTest. seqDef_induction_lower
- ProveRulesTest. seqDef_induction_lower_concrete
- ProveRulesTest. jdiv_one
- ProveRulesTest. seqDef_split_in_three
- ProveRulesTest. seqDef_empty
- ProveRulesTest. seqDef_one_summand
- ProveRulesTest. seqDef_lower_equals_upper
- ProveRulesTest. seqDefOfSeq
- ProveRulesTest. seqSelfDefinitionEQ2
- ProveRulesTest. indexOfSeqSingleton
- ProveRulesTest. indexOfSeqConcatFirst
- ProveRulesTest. indexOfSeqConcatSecond
- ProveRulesTest. indexOfSeqSub
- ProveRulesTest. div_zero
- ProveRulesTest. lenOfArray2seq
- ProveRulesTest. getAnyOfArray2seq
- ProveRulesTest. getOfArray2seq
- ProveRulesTest. getAnyOfNPermInv
- ProveRulesTest. seqNPermRange
- ProveRulesTest. seqPermTrans
- ProveRulesTest. seqPermRefl
- ProveRulesTest. seqPermSplit
- ProveRulesTest. seqNPermRight
- ProveRulesTest. seqPermFromSwap
- ProveRulesTest. divResZero1
- ProveRulesTest. seqPermTransAlt0
- ProveRulesTest. seqPermTransAlt1
- ProveRulesTest. seqPermTransAlt2
- ProveRulesTest. seqPermTransAlt3
- ProveRulesTest. seqPermForall
- ProveRulesTest. seqPermExists
- ProveRulesTest. schiffl_lemma_2
- ProveRulesTest. schiffl_thm_1
- ProveRulesTest. eqSameSeq
- ProveRulesTest. divResZero2
- ProveRulesTest. eqTermCut
- ProveRulesTest. divResOne1
- ProveRulesTest. divResOne2
- ProveRulesTest. div_cancel1
- ProveRulesTest. div_cancel2
- ProveRulesTest. divAddMultDenom
- ProveRulesTest. divMinus
- ProveRulesTest. divMinusDenom
- ProveRulesTest. divLeastDPos
- ProveRulesTest. divLeastDNeg
- ProveRulesTest. divGreatestDPos
- ProveRulesTest. equivAllRight
- ProveRulesTest. divGreatestDNeg
- ProveRulesTest. divIncreasingPos
- ProveRulesTest. divIncreasingNeg
- ProveRulesTest. jdiv_zero
- ProveRulesTest. jdivPulloutMinusNum
- ProveRulesTest. jdivPulloutMinusDenom
- ProveRulesTest. jdiv_uniquePosPos
- ProveRulesTest. jdiv_uniquePosNeg
- ProveRulesTest. jdiv_uniqueNegPos
- ProveRulesTest. jdiv_uniqueNegNeg
- ProveRulesTest. irrflConcrete1
- ProveRulesTest. jdivMultDenom1
- ProveRulesTest. jdivMultDenom2
- ProveRulesTest. mod_geZero
- ProveRulesTest. mod_lessDenom
- ProveRulesTest. jmod_NumPos
- ProveRulesTest. jmod_NumNeg
- ProveRulesTest. jmod_geZero
- ProveRulesTest. jmodNumZero
- ProveRulesTest. jmod_pulloutminusNum
- ProveRulesTest. jmod_pulloutminusDenom
- ProveRulesTest. irrflConcrete2
- ProveRulesTest. jmodUnique1
- ProveRulesTest. jmodUnique2
- ProveRulesTest. intDivRem
- ProveRulesTest. jmodjmod
- ProveRulesTest. jmodDivisible
- ProveRulesTest. jmodDivisibleRep
- ProveRulesTest. jdivAddMultDenom
- ProveRulesTest. jmodAltZero
- ProveRulesTest. jmodAddMultDenomZero
- ProveRulesTest. polyDiv_zero
- ProveRulesTest. cancel_gtPos
- ProveRulesTest. polyMod_ltdivDenom
- ProveRulesTest. bsum_empty
- ProveRulesTest. bsum_induction_upper
- ProveRulesTest. bsum_induction_lower
- ProveRulesTest. bsum_num_of_bounds
- ProveRulesTest. bsum_num_of_bounds2
- ProveRulesTest. bsum_induction_upper2
- ProveRulesTest. bsum_induction_upper_concrete
- ProveRulesTest. bsum_induction_upper_concrete_2
- ProveRulesTest. bsum_induction_upper2_concrete
- ProveRulesTest. cancel_gtNeg
- ProveRulesTest. bsum_induction_lower_concrete
- ProveRulesTest. bsum_induction_lower2
- ProveRulesTest. bsum_induction_lower2_concrete
- ProveRulesTest. bsum_positive
- ProveRulesTest. bsum_upper_bound
- ProveRulesTest. bsum_lower_bound
- ProveRulesTest. bsum_positive_lower_bound_element
- ProveRulesTest. bsum_sub_same_index
- ProveRulesTest. bsum_less_same_index
- ProveRulesTest. bsum_equal_except_one_index
- ProveRulesTest. moduloIntIsInInt
- ProveRulesTest. bsum_num_of_is_max
- ProveRulesTest. bsum_num_of_is_max2
- ProveRulesTest. bsum_num_of_is_max3
- ProveRulesTest. bsum_num_of_is_max4
- ProveRulesTest. bsum_num_of_lt_max
- ProveRulesTest. bsum_num_of_lt_max2
- ProveRulesTest. bsum_num_of_lt_max3
- ProveRulesTest. bsum_num_of_lt_max4
- ProveRulesTest. bsum_num_of_gt0
- ProveRulesTest. bsum_num_of_gt0_alt
- ProveRulesTest. moduloLongIsInLong
- ProveRulesTest. bsum_add_concrete
- ProveRulesTest. bprod_all_positive
- ProveRulesTest. bprod_split
- ProveRulesTest. powConcrete0
- ProveRulesTest. powConcrete1
- ProveRulesTest. powSplitFactor
- ProveRulesTest. powAdd
- ProveRulesTest. powMono
- ProveRulesTest. powMonoConcrete
- ProveRulesTest. powMonoConcreteRight
- ProveRulesTest. moduloShortIsInShort
Classes
| Class | Tests | Failures | Ignored | Duration | Success rate |
|---|---|---|---|---|---|
| ProveRulesTest | 198 | 198 | 0 | 12m36.22s | 0% |