Skip to content
Snippets Groups Projects
Commit 3da15e71 authored by ravi's avatar ravi
Browse files

Adding a regression test suite for lazy evaluation

parent 62be822d
Branches
Tags
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 573 additions and 1243 deletions
results/21-jan/Conqueue.out deleted 100644 → 0
+ 0
− 294
View file @ 62be822d
[Warning ] warning: there were 33 feature warnings; re-run with -feature for details
[ Info ] Output written on leon.out
[ Info ] Output written on leon.out
[ Info ] Output written on leon.out
[ Info ] - Now considering 'postcondition' VC for zeroPreceedsLazy4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for zeroPreceedsLazy4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for zeroPreceedsSuf4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for zeroPreceedsSuf4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for concreteUntil4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for concreteUntil4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for isConcrete4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for isConcrete4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for schedulesProperty4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for schedulesProperty4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for schedulesProperty4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for strongSchedsProp4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for strongSchedsProp4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for pushUntilCarry4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for pushUntilCarry4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for pushLeft4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call pushLeftLazy4[T](ys, xs, scr6._2))' VC for pushLeft4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for pushLeft4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for pushLeftLazy4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for pushLeftLazy4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for pushLeftLazy4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for PushLeftLazy@pushLeftLazyLem1 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for PushLeftLazy@pushLeftLazyLem1 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for PushLeftLazy@pushLeftLazyLem1 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (postcondition)' VC for pushLeftLazyPreMonotone1 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (match exhaustiveness)' VC for pushLeftLazyPreMonotone1 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for pushLeftLazyLemma4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call pushLeftLazyLemma4[T](CC[T](head, ys), r ...)' VC for pushLeftLazyLemma4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call pushLeftLazy4[T](ys, xs, a84._2))' VC for pushLeftLazyLemma4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for pushLeftLazyLemma4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for pushLeftLazyLemma4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for pushLeftLazyLemma4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for pushLeftWrapper4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call pushLeft4[T](ys, w.queue, st@))' VC for pushLeftWrapper4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for pushLeftWrapper4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for Pay4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for Pay4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for Pay4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for schedMonotone4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call schedMonotone4[T](st1, st2, tail, pushUn ...)' VC for schedMonotone4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for schedMonotone4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for schedMonotone4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (postcondition)' VC for concreteMonotone4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (match exhaustiveness)' VC for concreteMonotone4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (postcondition)' VC for concUntilMonotone4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (match exhaustiveness)' VC for concUntilMonotone4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for suffix4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for suffix4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for properSuffix4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for properSuffix4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (postcondition)' VC for suffixTrans4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (match exhaustiveness)' VC for suffixTrans4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (match exhaustiveness)' VC for suffixTrans4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for suffixTrans4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for suffixDisequality4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call suffixDisequality4[T](rear39, sufRear3))' VC for suffixDisequality4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for suffixDisequality4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (postcondition)' VC for suffixCompose4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (match exhaustiveness)' VC for suffixCompose4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (postcondition)' VC for concreteUntilIsSuffix4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (match exhaustiveness)' VC for concreteUntilIsSuffix4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (postcondition)' VC for concUntilExtenLemma4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (match exhaustiveness)' VC for concUntilExtenLemma4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (match exhaustiveness)' VC for concUntilExtenLemma4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for concUntilExtenLemma4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (postcondition)' VC for concUntilConcreteExten4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (match exhaustiveness)' VC for concUntilConcreteExten4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (postcondition)' VC for concUntilCompose4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (match exhaustiveness)' VC for concUntilCompose4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (postcondition)' VC for zeroPredSufConcreteUntilLemma4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (match exhaustiveness)' VC for zeroPredSufConcreteUntilLemma4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (postcondition)' VC for concreteZeroPredLemma4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (match exhaustiveness)' VC for concreteZeroPredLemma4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for suffixZeroLemma4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call suffixZeroLemma4[T](tail17, suf, suf2))' VC for suffixZeroLemma4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for suffixZeroLemma4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for pushLeftAndPay4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call pushLeftWrapper4[T](ys, w, st@))' VC for pushLeftAndPay4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call Pay4[T](q236, x$39._1._2, x$39._2))' VC for pushLeftAndPay4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for pushLeftAndPay4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for isEmpty9 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for level5 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for level5 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for isSpine5 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for isSpine5 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for isTip5 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for valid5 @?:?...
[ Info ] => VALID
┌──────────────────────┐
╔═╡ Verification Summary ╞══════════════════════════════════════════════════════════════════════════════════════════════════════════════╗
║ └──────────────────────┘ ║
║ Conqueue.Pay match exhaustiveness ?:? valid U:smt-z3 0.066 ║
║ Conqueue.Pay match exhaustiveness ?:? valid U:smt-z3 0.011 ║
║ Conqueue.Pay postcondition ?:? valid U:smt-z3 1.663 ║
║ Conqueue.PushLeftLazy@pushLeftLazyLem match exhaustiveness ?:? valid U:smt-z3 0.011 ║
║ Conqueue.PushLeftLazy@pushLeftLazyLem match exhaustiveness ?:? valid U:smt-z3 0.017 ║
║ Conqueue.PushLeftLazy@pushLeftLazyLem postcondition ?:? valid U:smt-z3 0.145 ║
║ Conqueue.concUntilCompose tact (match exhaustiveness) ?:? valid U:smt-z3 0.009 ║
║ Conqueue.concUntilCompose tact (postcondition) ?:? valid U:smt-z3 0.050 ║
║ Conqueue.concUntilConcreteExten tact (match exhaustiveness) ?:? valid U:smt-z3 0.011 ║
║ Conqueue.concUntilConcreteExten tact (postcondition) ?:? valid U:smt-z3 0.063 ║
║ Conqueue.concUntilExtenLemma match exhaustiveness ?:? valid U:smt-z3 0.013 ║
║ Conqueue.concUntilExtenLemma tact (match exhaustiveness) ?:? valid U:smt-z3 0.010 ║
║ Conqueue.concUntilExtenLemma tact (match exhaustiveness) ?:? valid U:smt-z3 0.013 ║
║ Conqueue.concUntilExtenLemma tact (postcondition) ?:? valid U:smt-z3 0.059 ║
║ Conqueue.concUntilMonotone tact (match exhaustiveness) ?:? valid U:smt-z3 0.013 ║
║ Conqueue.concUntilMonotone tact (postcondition) ?:? valid U:smt-z3 0.057 ║
║ Conqueue.concreteMonotone tact (match exhaustiveness) ?:? valid U:smt-z3 0.010 ║
║ Conqueue.concreteMonotone tact (postcondition) ?:? valid U:smt-z3 0.067 ║
║ Conqueue.concreteUntil match exhaustiveness ?:? valid U:smt-z3 0.020 ║
║ Conqueue.concreteUntil postcondition ?:? valid U:smt-z3 0.034 ║
║ Conqueue.concreteUntilIsSuffix tact (match exhaustiveness) ?:? valid U:smt-z3 0.009 ║
║ Conqueue.concreteUntilIsSuffix tact (postcondition) ?:? valid U:smt-z3 0.049 ║
║ Conqueue.concreteZeroPredLemma tact (match exhaustiveness) ?:? valid U:smt-z3 0.010 ║
║ Conqueue.concreteZeroPredLemma tact (postcondition) ?:? valid U:smt-z3 0.040 ║
║ Conqueue.isConcrete match exhaustiveness ?:? valid U:smt-z3 0.019 ║
║ Conqueue.isConcrete postcondition ?:? valid U:smt-z3 0.026 ║
║ Conc.isEmpty postcondition ?:? valid U:smt-z3 0.007 ║
║ ConQ.isSpine match exhaustiveness ?:? valid U:smt-z3 0.009 ║
║ ConQ.isSpine postcondition ?:? valid U:smt-z3 0.009 ║
║ ConQ.isTip postcondition ?:? valid U:smt-z3 0.010 ║
║ Conc.level match exhaustiveness ?:? valid U:smt-z3 0.008 ║
║ Conc.level postcondition ?:? valid U:smt-z3 0.042 ║
║ Conqueue.properSuffix match exhaustiveness ?:? valid U:smt-z3 0.012 ║
║ Conqueue.properSuffix postcondition ?:? valid U:smt-z3 0.050 ║
║ Conqueue.pushLeft match exhaustiveness ?:? valid U:smt-z3 0.017 ║
║ Conqueue.pushLeft postcondition ?:? valid U:smt-z3 0.327 ║
║ Conqueue.pushLeft precond. (call pushLeftLazy4[T](ys, xs, scr6._2)) ?:? valid U:smt-z3 0.144 ║
║ Conqueue.pushLeftAndPay match exhaustiveness ?:? valid U:smt-z3 0.007 ║
║ Conqueue.pushLeftAndPay postcondition ?:? valid U:smt-z3 0.225 ║
║ Conqueue.pushLeftAndPay precond. (call Pay4[T](q236, x$39._1._2, x$39._2)) ?:? valid U:smt-z3 0.111 ║
║ Conqueue.pushLeftAndPay precond. (call pushLeftWrapper4[T](ys, w, st@)) ?:? valid U:smt-z3 0.042 ║
║ Conqueue.pushLeftLazy match exhaustiveness ?:? valid U:smt-z3 0.073 ║
║ Conqueue.pushLeftLazy match exhaustiveness ?:? valid U:smt-z3 0.015 ║
║ Conqueue.pushLeftLazy postcondition ?:? valid U:smt-z3 4.156 ║
║ Conqueue.pushLeftLazyLemma match exhaustiveness ?:? valid U:smt-z3 0.212 ║
║ Conqueue.pushLeftLazyLemma match exhaustiveness ?:? valid U:smt-z3 0.014 ║
║ Conqueue.pushLeftLazyLemma match exhaustiveness ?:? valid U:smt-z3 0.015 ║
║ Conqueue.pushLeftLazyLemma postcondition ?:? valid U:smt-z3 0.235 ║
║ Conqueue.pushLeftLazyLemma precond. (call pushLeftLazy4[T](ys, xs, a84._2)) ?:? valid U:smt-z3 0.143 ║
║ Conqueue.pushLeftLazyLemma precond. (call pushLeftLazyLemma4[T](CC[T](head, ys), r ...) ?:? valid U:smt-z3 0.076 ║
║ Conqueue.pushLeftLazyPreMonotone tact (match exhaustiveness) ?:? valid U:smt-z3 0.014 ║
║ Conqueue.pushLeftLazyPreMonotone tact (postcondition) ?:? valid U:smt-z3 0.077 ║
║ Conqueue.pushLeftWrapper match exhaustiveness ?:? valid U:smt-z3 0.013 ║
║ Conqueue.pushLeftWrapper postcondition ?:? valid U:smt-cvc4 27.287 ║
║ Conqueue.pushLeftWrapper precond. (call pushLeft4[T](ys, w.queue, st@)) ?:? valid U:smt-z3 0.055 ║
║ Conqueue.pushUntilCarry match exhaustiveness ?:? valid U:smt-z3 0.021 ║
║ Conqueue.pushUntilCarry postcondition ?:? valid U:smt-z3 0.025 ║
║ Conqueue.schedMonotone match exhaustiveness ?:? valid U:smt-z3 0.015 ║
║ Conqueue.schedMonotone match exhaustiveness ?:? valid U:smt-z3 0.020 ║
║ Conqueue.schedMonotone postcondition ?:? valid U:smt-z3 0.112 ║
║ Conqueue.schedMonotone precond. (call schedMonotone4[T](st1, st2, tail, pushUn ...) ?:? valid U:smt-z3 0.088 ║
║ Conqueue.schedulesProperty match exhaustiveness ?:? valid U:smt-z3 0.020 ║
║ Conqueue.schedulesProperty match exhaustiveness ?:? valid U:smt-z3 0.012 ║
║ Conqueue.schedulesProperty postcondition ?:? valid U:smt-z3 0.033 ║
║ Conqueue.strongSchedsProp match exhaustiveness ?:? valid U:smt-z3 0.014 ║
║ Conqueue.strongSchedsProp postcondition ?:? valid U:smt-z3 0.024 ║
║ Conqueue.suffix match exhaustiveness ?:? valid U:smt-z3 0.011 ║
║ Conqueue.suffix postcondition ?:? valid U:smt-z3 0.011 ║
║ Conqueue.suffixCompose tact (match exhaustiveness) ?:? valid U:smt-z3 0.010 ║
║ Conqueue.suffixCompose tact (postcondition) ?:? valid U:smt-z3 0.081 ║
║ Conqueue.suffixDisequality match exhaustiveness ?:? valid U:smt-z3 0.015 ║
║ Conqueue.suffixDisequality postcondition ?:? valid U:smt-z3 0.070 ║
║ Conqueue.suffixDisequality precond. (call suffixDisequality4[T](rear39, sufRear3)) ?:? valid U:smt-z3 0.068 ║
║ Conqueue.suffixTrans match exhaustiveness ?:? valid U:smt-z3 0.011 ║
║ Conqueue.suffixTrans tact (match exhaustiveness) ?:? valid U:smt-z3 0.010 ║
║ Conqueue.suffixTrans tact (match exhaustiveness) ?:? valid U:smt-z3 0.013 ║
║ Conqueue.suffixTrans tact (postcondition) ?:? valid U:smt-z3 0.079 ║
║ Conqueue.suffixZeroLemma match exhaustiveness ?:? valid U:smt-z3 0.014 ║
║ Conqueue.suffixZeroLemma postcondition ?:? valid U:smt-z3 0.086 ║
║ Conqueue.suffixZeroLemma precond. (call suffixZeroLemma4[T](tail17, suf, suf2)) ?:? valid U:smt-z3 0.073 ║
║ Queue.valid postcondition ?:? valid U:smt-z3 0.015 ║
║ Conqueue.zeroPreceedsLazy match exhaustiveness ?:? valid U:smt-z3 0.034 ║
║ Conqueue.zeroPreceedsLazy postcondition ?:? valid U:smt-z3 0.126 ║
║ Conqueue.zeroPreceedsSuf match exhaustiveness ?:? valid U:smt-z3 0.028 ║
║ Conqueue.zeroPreceedsSuf postcondition ?:? valid U:smt-z3 0.040 ║
║ Conqueue.zeroPredSufConcreteUntilLemma tact (match exhaustiveness) ?:? valid U:smt-z3 0.010 ║
║ Conqueue.zeroPredSufConcreteUntilLemma tact (postcondition) ?:? valid U:smt-z3 0.062 ║
╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
║ total: 87 valid: 87 invalid: 0 unknown 0 37.151 ║
╚═══════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════╝
[ Info ] Output written on leon.out
[ Info ] - Now considering 'postcondition' VC for pushLeft-time @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for pushLeftLazy-time @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for pushLeftWrapper-time @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for Pay-time @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for pushLeftAndPay-time @?:?...
[ Info ] => VALID
Resource Verification Results:
┌──────────────────────┐
╔═╡ Verification Summary ╞═══════════════════════════════════════════════════════════════════╗
║ └──────────────────────┘ ║
║ Conqueue.Pay-time postcondition ?:? valid U:smt-z3 2.380 ║
║ Conqueue.pushLeft-time postcondition ?:? valid U:smt-z3 0.151 ║
║ Conqueue.pushLeftAndPay-time postcondition ?:? valid U:smt-z3 0.229 ║
║ Conqueue.pushLeftLazy-time postcondition ?:? valid U:smt-z3 0.209 ║
║ Conqueue.pushLeftWrapper-time postcondition ?:? valid U:smt-z3 0.204 ║
╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
║ total: 5 valid: 5 invalid: 0 unknown 0 3.173 ║
╚════════════════════════════════════════════════════════════════════════════════════════════╝
results/21-jan/Esop.out deleted 100644 → 0
+ 0
− 47
View file @ 62be822d
[ Info ] Output written on leon.out
[ Info ] Output written on leon.out
[ Info ] Output written on leon.out
[ Info ] - Now considering 'postcondition' VC for zipWith4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for zipWith4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for nextFib4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for fibStream4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for nthFib4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call nthFib4(n - BigInt(1), tail9, scr3._2))' VC for nthFib4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for nthFib4 @?:?...
[ Info ] => VALID
┌──────────────────────┐
╔═╡ Verification Summary ╞══════════════════════════════════════════════════════════════════════════════════════════╗
║ └──────────────────────┘ ║
║ Esop15Benchmarks.fibStream postcondition ?:? valid U:smt-z3 0.027 ║
║ Esop15Benchmarks.nextFib postcondition ?:? valid U:smt-z3 0.035 ║
║ Esop15Benchmarks.nthFib match exhaustiveness ?:? valid U:smt-z3 0.020 ║
║ Esop15Benchmarks.nthFib postcondition ?:? valid U:smt-z3 0.098 ║
║ Esop15Benchmarks.nthFib precond. (call nthFib4(n - BigInt(1), tail9, scr3._2)) ?:? valid U:smt-z3 0.021 ║
║ Esop15Benchmarks.zipWith match exhaustiveness ?:? valid U:smt-z3 0.023 ║
║ Esop15Benchmarks.zipWith postcondition ?:? valid U:smt-z3 0.197 ║
╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
║ total: 7 valid: 7 invalid: 0 unknown 0 0.421 ║
╚═══════════════════════════════════════════════════════════════════════════════════════════════════════════════════╝
[ Info ] Output written on leon.out
[ Info ] - Now considering 'postcondition' VC for zipWith-time @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for nextFib-time @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for nthFib-time @?:?...
[ Info ] => VALID
Resource Verification Results:
┌──────────────────────┐
╔═╡ Verification Summary ╞═══════════════════════════════════════════════════════════════════╗
║ └──────────────────────┘ ║
║ Esop15Benchmarks.nextFib-time postcondition ?:? valid U:smt-z3 0.039 ║
║ Esop15Benchmarks.nthFib-time postcondition ?:? valid U:smt-z3 0.143 ║
║ Esop15Benchmarks.zipWith-time postcondition ?:? valid U:smt-z3 0.106 ║
╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
║ total: 3 valid: 3 invalid: 0 unknown 0 0.288 ║
╚════════════════════════════════════════════════════════════════════════════════════════════╝
results/21-jan/MsortBU.out deleted 100644 → 0
+ 0
− 138
View file @ 62be822d
[Warning ] warning: there were 5 feature warnings; re-run with -feature for details
[ Info ] Output written on leon.out
[ Info ] Output written on leon.out
[ Info ] Output written on leon.out
[ Info ] - Now considering 'postcondition' VC for ssize4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for pairs4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call pairs4(rest, st@))' VC for pairs4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for pairs4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for constructMergeTree4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call pairs4(l, st@))' VC for constructMergeTree4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call constructMergeTree4(a77._1, a77._2))' VC for constructMergeTree4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for constructMergeTree4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for merge4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for merge4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for merge4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for Merge@pairsLem1 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call pairs4(rest, st@))' VC for Merge@pairsLem1 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for Merge@mergeLem2 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for Merge@mergeLem3 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (postcondition)' VC for mergePreMonotone1 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for IListToLList4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for IListToLList4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for mergeSort4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call constructMergeTree4(IListToLList4(l), st ...)' VC for mergeSort4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for mergeSort4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for mergeSort4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for firstMin4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for firstMin4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for size19 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for size19 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for size20 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for size20 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for size21 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for size21 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for valid5 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for valid5 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for fullSize5 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for fullSize5 @?:?...
[ Info ] => VALID
┌──────────────────────┐
╔═╡ Verification Summary ╞════════════════════════════════════════════════════════════════════════════════════════════════════════════╗
║ └──────────────────────┘ ║
║ BottomUpMergeSort.IListToLList match exhaustiveness ?:? valid U:smt-z3 0.009 ║
║ BottomUpMergeSort.IListToLList postcondition ?:? valid U:smt-cvc4 1.025 ║
║ BottomUpMergeSort.Merge@mergeLem postcondition ?:? valid U:smt-z3 0.056 ║
║ BottomUpMergeSort.Merge@mergeLem postcondition ?:? valid U:smt-z3 0.062 ║
║ BottomUpMergeSort.Merge@pairsLem postcondition ?:? valid U:smt-z3 0.198 ║
║ BottomUpMergeSort.Merge@pairsLem precond. (call pairs4(rest, st@)) ?:? valid U:smt-z3 0.021 ║
║ BottomUpMergeSort.constructMergeTree match exhaustiveness ?:? valid U:smt-z3 0.013 ║
║ BottomUpMergeSort.constructMergeTree postcondition ?:? valid U:smt-z3 0.174 ║
║ BottomUpMergeSort.constructMergeTree precond. (call constructMergeTree4(a77._1, a77._2)) ?:? valid U:smt-z3 0.034 ║
║ BottomUpMergeSort.constructMergeTree precond. (call pairs4(l, st@)) ?:? valid U:smt-z3 0.014 ║
║ BottomUpMergeSort.firstMin match exhaustiveness ?:? valid U:smt-z3 0.297 ║
║ BottomUpMergeSort.firstMin postcondition ?:? valid U:smt-z3 0.335 ║
║ LList.fullSize match exhaustiveness ?:? valid U:smt-z3 0.009 ║
║ LList.fullSize postcondition ?:? valid U:smt-z3 0.030 ║
║ BottomUpMergeSort.merge match exhaustiveness ?:? valid U:smt-z3 0.022 ║
║ BottomUpMergeSort.merge match exhaustiveness ?:? valid U:smt-z3 0.017 ║
║ BottomUpMergeSort.merge postcondition ?:? valid U:smt-cvc4 1.813 ║
║ BottomUpMergeSort.mergePreMonotone tact (postcondition) ?:? valid U:smt-z3 0.015 ║
║ BottomUpMergeSort.mergeSort match exhaustiveness ?:? valid U:smt-z3 0.148 ║
║ BottomUpMergeSort.mergeSort match exhaustiveness ?:? valid U:smt-z3 0.008 ║
║ BottomUpMergeSort.mergeSort postcondition ?:? valid U:smt-z3 0.315 ║
║ BottomUpMergeSort.mergeSort precond. (call constructMergeTree4(IListToLList4(l), st ...) ?:? valid U:smt-z3 0.017 ║
║ BottomUpMergeSort.pairs match exhaustiveness ?:? valid U:smt-z3 0.015 ║
║ BottomUpMergeSort.pairs postcondition ?:? valid U:smt-z3 0.779 ║
║ BottomUpMergeSort.pairs precond. (call pairs4(rest, st@)) ?:? valid U:smt-z3 0.035 ║
║ LList.size match exhaustiveness ?:? valid U:smt-z3 0.011 ║
║ IList.size match exhaustiveness ?:? valid U:smt-z3 0.008 ║
║ IStream.size match exhaustiveness ?:? valid U:smt-z3 0.009 ║
║ LList.size postcondition ?:? valid U:smt-z3 0.017 ║
║ IList.size postcondition ?:? valid U:smt-z3 0.012 ║
║ IStream.size postcondition ?:? valid U:smt-z3 0.015 ║
║ BottomUpMergeSort.ssize postcondition ?:? valid U:smt-z3 0.572 ║
║ LList.valid match exhaustiveness ?:? valid U:smt-z3 0.013 ║
║ LList.valid postcondition ?:? valid U:smt-z3 0.013 ║
╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
║ total: 34 valid: 34 invalid: 0 unknown 0 6.131 ║
╚═════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════╝
[ Info ] Output written on leon.out
[ Info ] - Now considering 'postcondition' VC for pairs-time @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for constructMergeTree-time @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for merge-time @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for IListToLList-time @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for mergeSort-time @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for firstMin-time @?:?...
[ Info ] => VALID
Resource Verification Results:
┌──────────────────────┐
╔═╡ Verification Summary ╞═══════════════════════════════════════════════════════════════════╗
║ └──────────────────────┘ ║
║ BottomUpMergeSort.IListToLList-time postcondition ?:? valid U:smt-z3 0.026 ║
║ BottomUpMergeSort.constructMergeTree-time postcondition ?:? valid U:smt-z3 0.401 ║
║ BottomUpMergeSort.firstMin-time postcondition ?:? valid U:smt-z3 0.717 ║
║ BottomUpMergeSort.merge-time postcondition ?:? valid U:smt-z3 0.560 ║
║ BottomUpMergeSort.mergeSort-time postcondition ?:? valid U:smt-z3 0.433 ║
║ BottomUpMergeSort.pairs-time postcondition ?:? valid U:smt-z3 0.077 ║
╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
║ total: 6 valid: 6 invalid: 0 unknown 0 2.214 ║
╚════════════════════════════════════════════════════════════════════════════════════════════╝
results/21-jan/Num.out deleted 100644 → 0
+ 0
− 285
View file @ 62be822d
[Warning ] warning: there were 33 feature warnings; re-run with -feature for details
[ Info ] Output written on leon.out
[ Info ] Output written on leon.out
[ Info ] Output written on leon.out
[ Info ] - Now considering 'postcondition' VC for zeroPreceedsLazy4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for zeroPreceedsLazy4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for zeroPreceedsSuf4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for zeroPreceedsSuf4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for concreteUntil4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for concreteUntil4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for isConcrete4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for isConcrete4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for schedulesProperty4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for schedulesProperty4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for schedulesProperty4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for strongSchedsProp4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for strongSchedsProp4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for pushUntilCarry4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for pushUntilCarry4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for inc4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call incLazy4(xs, scr6._2))' VC for inc4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for inc4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for incLazy4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for incLazy4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for incLazy4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for IncLazy@incLazyLem1 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for IncLazy@incLazyLem1 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for IncLazy@incLazyLem1 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (postcondition)' VC for incLazyPreMonotone1 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (match exhaustiveness)' VC for incLazyPreMonotone1 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for incLazyLemma4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call incLazyLemma4[<untyped>](rear30, suf, st ...)' VC for incLazyLemma4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call incLazy4(xs, a83._2))' VC for incLazyLemma4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for incLazyLemma4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for incLazyLemma4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for incLazyLemma4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for incNum4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call inc4(w.digs, st@))' VC for incNum4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for incNum4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for Pay4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for Pay4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for Pay4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for schedMonotone4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call schedMonotone4[<untyped>](st1, st2, tail ...)' VC for schedMonotone4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for schedMonotone4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for schedMonotone4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (postcondition)' VC for concreteMonotone4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (match exhaustiveness)' VC for concreteMonotone4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (postcondition)' VC for concUntilMonotone4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (match exhaustiveness)' VC for concUntilMonotone4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for suffix4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for suffix4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for properSuffix4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for properSuffix4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (postcondition)' VC for suffixTrans4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (match exhaustiveness)' VC for suffixTrans4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (match exhaustiveness)' VC for suffixTrans4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for suffixTrans4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for suffixDisequality4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call suffixDisequality4[<untyped>](rear39, su ...)' VC for suffixDisequality4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for suffixDisequality4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (postcondition)' VC for suffixCompose4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (match exhaustiveness)' VC for suffixCompose4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (postcondition)' VC for concreteUntilIsSuffix4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (match exhaustiveness)' VC for concreteUntilIsSuffix4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (postcondition)' VC for concUntilExtenLemma4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (match exhaustiveness)' VC for concUntilExtenLemma4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (match exhaustiveness)' VC for concUntilExtenLemma4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for concUntilExtenLemma4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (postcondition)' VC for concUntilConcreteExten4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (match exhaustiveness)' VC for concUntilConcreteExten4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (postcondition)' VC for concUntilCompose4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (match exhaustiveness)' VC for concUntilCompose4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (postcondition)' VC for zeroPredSufConcreteUntilLemma4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (match exhaustiveness)' VC for zeroPredSufConcreteUntilLemma4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (postcondition)' VC for concreteZeroPredLemma4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (match exhaustiveness)' VC for concreteZeroPredLemma4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for suffixZeroLemma4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call suffixZeroLemma4[<untyped>](tail17, suf, ...)' VC for suffixZeroLemma4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for suffixZeroLemma4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for incAndPay4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call incNum4[<untyped>](w, st@))' VC for incAndPay4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call Pay4[<untyped>](q175, x$218._1._2, x$218 ...)' VC for incAndPay4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for incAndPay4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for isSpine5 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for isSpine5 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for isTip5 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for valid5 @?:?...
[ Info ] => VALID
┌──────────────────────┐
╔═╡ Verification Summary ╞══════════════════════════════════════════════════════════════════════════════════════════════════════════════════════╗
║ └──────────────────────┘ ║
║ LazyNumericalRep.IncLazy@incLazyLem match exhaustiveness ?:? valid U:smt-z3 0.016 ║
║ LazyNumericalRep.IncLazy@incLazyLem match exhaustiveness ?:? valid U:smt-z3 0.010 ║
║ LazyNumericalRep.IncLazy@incLazyLem postcondition ?:? valid U:smt-z3 0.119 ║
║ LazyNumericalRep.Pay match exhaustiveness ?:? valid U:smt-z3 0.063 ║
║ LazyNumericalRep.Pay match exhaustiveness ?:? valid U:smt-z3 0.011 ║
║ LazyNumericalRep.Pay postcondition ?:? valid U:smt-z3 1.498 ║
║ LazyNumericalRep.concUntilCompose tact (match exhaustiveness) ?:? valid U:smt-z3 0.008 ║
║ LazyNumericalRep.concUntilCompose tact (postcondition) ?:? valid U:smt-z3 0.066 ║
║ LazyNumericalRep.concUntilConcreteExten tact (match exhaustiveness) ?:? valid U:smt-z3 0.014 ║
║ LazyNumericalRep.concUntilConcreteExten tact (postcondition) ?:? valid U:smt-z3 0.046 ║
║ LazyNumericalRep.concUntilExtenLemma match exhaustiveness ?:? valid U:smt-z3 0.012 ║
║ LazyNumericalRep.concUntilExtenLemma tact (match exhaustiveness) ?:? valid U:smt-z3 0.011 ║
║ LazyNumericalRep.concUntilExtenLemma tact (match exhaustiveness) ?:? valid U:smt-z3 0.014 ║
║ LazyNumericalRep.concUntilExtenLemma tact (postcondition) ?:? valid U:smt-z3 0.066 ║
║ LazyNumericalRep.concUntilMonotone tact (match exhaustiveness) ?:? valid U:smt-z3 0.009 ║
║ LazyNumericalRep.concUntilMonotone tact (postcondition) ?:? valid U:smt-z3 0.040 ║
║ LazyNumericalRep.concreteMonotone tact (match exhaustiveness) ?:? valid U:smt-z3 0.009 ║
║ LazyNumericalRep.concreteMonotone tact (postcondition) ?:? valid U:smt-z3 0.049 ║
║ LazyNumericalRep.concreteUntil match exhaustiveness ?:? valid U:smt-z3 0.027 ║
║ LazyNumericalRep.concreteUntil postcondition ?:? valid U:smt-z3 0.029 ║
║ LazyNumericalRep.concreteUntilIsSuffix tact (match exhaustiveness) ?:? valid U:smt-z3 0.010 ║
║ LazyNumericalRep.concreteUntilIsSuffix tact (postcondition) ?:? valid U:smt-z3 0.067 ║
║ LazyNumericalRep.concreteZeroPredLemma tact (match exhaustiveness) ?:? valid U:smt-z3 0.009 ║
║ LazyNumericalRep.concreteZeroPredLemma tact (postcondition) ?:? valid U:smt-z3 0.054 ║
║ LazyNumericalRep.inc match exhaustiveness ?:? valid U:smt-z3 0.013 ║
║ LazyNumericalRep.inc postcondition ?:? valid U:smt-z3 0.250 ║
║ LazyNumericalRep.inc precond. (call incLazy4(xs, scr6._2)) ?:? valid U:smt-z3 0.122 ║
║ LazyNumericalRep.incAndPay match exhaustiveness ?:? valid U:smt-z3 0.007 ║
║ LazyNumericalRep.incAndPay postcondition ?:? valid U:smt-z3 0.158 ║
║ LazyNumericalRep.incAndPay precond. (call Pay4[<untyped>](q175, x$218._1._2, x$218 ...) ?:? valid U:smt-z3 0.113 ║
║ LazyNumericalRep.incAndPay precond. (call incNum4[<untyped>](w, st@)) ?:? valid U:smt-z3 0.032 ║
║ LazyNumericalRep.incLazy match exhaustiveness ?:? valid U:smt-z3 0.017 ║
║ LazyNumericalRep.incLazy match exhaustiveness ?:? valid U:smt-z3 0.062 ║
║ LazyNumericalRep.incLazy postcondition ?:? valid U:smt-cvc4 4.550 ║
║ LazyNumericalRep.incLazyLemma match exhaustiveness ?:? valid U:smt-z3 0.186 ║
║ LazyNumericalRep.incLazyLemma match exhaustiveness ?:? valid U:smt-z3 0.013 ║
║ LazyNumericalRep.incLazyLemma match exhaustiveness ?:? valid U:smt-z3 0.019 ║
║ LazyNumericalRep.incLazyLemma postcondition ?:? valid U:smt-z3 0.214 ║
║ LazyNumericalRep.incLazyLemma precond. (call incLazy4(xs, a83._2)) ?:? valid U:smt-z3 0.133 ║
║ LazyNumericalRep.incLazyLemma precond. (call incLazyLemma4[<untyped>](rear30, suf, st ...) ?:? valid U:smt-z3 0.082 ║
║ LazyNumericalRep.incLazyPreMonotone tact (match exhaustiveness) ?:? valid U:smt-z3 0.013 ║
║ LazyNumericalRep.incLazyPreMonotone tact (postcondition) ?:? valid U:smt-z3 0.079 ║
║ LazyNumericalRep.incNum match exhaustiveness ?:? valid U:smt-z3 0.016 ║
║ LazyNumericalRep.incNum postcondition ?:? valid U:smt-cvc4 19.158 ║
║ LazyNumericalRep.incNum precond. (call inc4(w.digs, st@)) ?:? valid U:smt-z3 0.043 ║
║ LazyNumericalRep.isConcrete match exhaustiveness ?:? valid U:smt-z3 0.017 ║
║ LazyNumericalRep.isConcrete postcondition ?:? valid U:smt-z3 0.031 ║
║ NumStream.isSpine match exhaustiveness ?:? valid U:smt-z3 0.008 ║
║ NumStream.isSpine postcondition ?:? valid U:smt-z3 0.008 ║
║ NumStream.isTip postcondition ?:? valid U:smt-z3 0.008 ║
║ LazyNumericalRep.properSuffix match exhaustiveness ?:? valid U:smt-z3 0.012 ║
║ LazyNumericalRep.properSuffix postcondition ?:? valid U:smt-z3 0.055 ║
║ LazyNumericalRep.pushUntilCarry match exhaustiveness ?:? valid U:smt-z3 0.018 ║
║ LazyNumericalRep.pushUntilCarry postcondition ?:? valid U:smt-z3 0.024 ║
║ LazyNumericalRep.schedMonotone match exhaustiveness ?:? valid U:smt-z3 0.015 ║
║ LazyNumericalRep.schedMonotone match exhaustiveness ?:? valid U:smt-z3 0.017 ║
║ LazyNumericalRep.schedMonotone postcondition ?:? valid U:smt-z3 0.093 ║
║ LazyNumericalRep.schedMonotone precond. (call schedMonotone4[<untyped>](st1, st2, tail ...) ?:? valid U:smt-z3 0.079 ║
║ LazyNumericalRep.schedulesProperty match exhaustiveness ?:? valid U:smt-z3 0.012 ║
║ LazyNumericalRep.schedulesProperty match exhaustiveness ?:? valid U:smt-z3 0.020 ║
║ LazyNumericalRep.schedulesProperty postcondition ?:? valid U:smt-z3 0.045 ║
║ LazyNumericalRep.strongSchedsProp match exhaustiveness ?:? valid U:smt-z3 0.013 ║
║ LazyNumericalRep.strongSchedsProp postcondition ?:? valid U:smt-z3 0.023 ║
║ LazyNumericalRep.suffix match exhaustiveness ?:? valid U:smt-z3 0.011 ║
║ LazyNumericalRep.suffix postcondition ?:? valid U:smt-z3 0.010 ║
║ LazyNumericalRep.suffixCompose tact (match exhaustiveness) ?:? valid U:smt-z3 0.010 ║
║ LazyNumericalRep.suffixCompose tact (postcondition) ?:? valid U:smt-z3 0.079 ║
║ LazyNumericalRep.suffixDisequality match exhaustiveness ?:? valid U:smt-z3 0.012 ║
║ LazyNumericalRep.suffixDisequality postcondition ?:? valid U:smt-z3 0.067 ║
║ LazyNumericalRep.suffixDisequality precond. (call suffixDisequality4[<untyped>](rear39, su ...) ?:? valid U:smt-z3 0.049 ║
║ LazyNumericalRep.suffixTrans match exhaustiveness ?:? valid U:smt-z3 0.017 ║
║ LazyNumericalRep.suffixTrans tact (match exhaustiveness) ?:? valid U:smt-z3 0.009 ║
║ LazyNumericalRep.suffixTrans tact (match exhaustiveness) ?:? valid U:smt-z3 0.016 ║
║ LazyNumericalRep.suffixTrans tact (postcondition) ?:? valid U:smt-z3 0.070 ║
║ LazyNumericalRep.suffixZeroLemma match exhaustiveness ?:? valid U:smt-z3 0.011 ║
║ LazyNumericalRep.suffixZeroLemma postcondition ?:? valid U:smt-z3 0.082 ║
║ LazyNumericalRep.suffixZeroLemma precond. (call suffixZeroLemma4[<untyped>](tail17, suf, ...) ?:? valid U:smt-z3 0.067 ║
║ Number.valid postcondition ?:? valid U:smt-z3 0.009 ║
║ LazyNumericalRep.zeroPreceedsLazy match exhaustiveness ?:? valid U:smt-z3 0.037 ║
║ LazyNumericalRep.zeroPreceedsLazy postcondition ?:? valid U:smt-z3 0.270 ║
║ LazyNumericalRep.zeroPreceedsSuf match exhaustiveness ?:? valid U:smt-z3 0.027 ║
║ LazyNumericalRep.zeroPreceedsSuf postcondition ?:? valid U:smt-z3 0.035 ║
║ LazyNumericalRep.zeroPredSufConcreteUntilLemma tact (match exhaustiveness) ?:? valid U:smt-z3 0.011 ║
║ LazyNumericalRep.zeroPredSufConcreteUntilLemma tact (postcondition) ?:? valid U:smt-z3 0.067 ║
╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
║ total: 84 valid: 84 invalid: 0 unknown 0 29.001 ║
╚═══════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════╝
[ Info ] Output written on leon.out
[ Info ] - Now considering 'postcondition' VC for inc-time @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for incLazy-time @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for incNum-time @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for Pay-time @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for incAndPay-time @?:?...
[ Info ] => VALID
Resource Verification Results:
┌──────────────────────┐
╔═╡ Verification Summary ╞═══════════════════════════════════════════════════════════════════╗
║ └──────────────────────┘ ║
║ LazyNumericalRep.Pay-time postcondition ?:? valid U:smt-z3 0.230 ║
║ LazyNumericalRep.inc-time postcondition ?:? valid U:smt-z3 0.135 ║
║ LazyNumericalRep.incAndPay-time postcondition ?:? valid U:smt-z3 0.200 ║
║ LazyNumericalRep.incLazy-time postcondition ?:? valid U:smt-z3 0.153 ║
║ LazyNumericalRep.incNum-time postcondition ?:? valid U:smt-z3 0.230 ║
╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
║ total: 5 valid: 5 invalid: 0 unknown 0 0.948 ║
╚════════════════════════════════════════════════════════════════════════════════════════════╝
results/21-jan/NumRep.out deleted 100644 → 0
+ 0
− 0
View file @ 62be822d
results/21-jan/RDQ.out deleted 100644 → 0
+ 0
− 282
View file @ 62be822d
[Warning ] warning: there were 15 feature warnings; re-run with -feature for details
[ Info ] Output written on leon.out
[ Info ] Output written on leon.out
[ Info ] Output written on leon.out
[ Info ] - Now considering 'postcondition' VC for isConcrete4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for isConcrete4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for revAppend4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call revAppend4[T](tail21, EagerStream[T](SCo ...)' VC for revAppend4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for revAppend4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for drop6 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call drop6[T](n - BigInt(1), tail22, scr11._2 ...)' VC for drop6 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for drop6 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for take6 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call take6[T](n - BigInt(1), tail23, scr12._2 ...)' VC for take6 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for take6 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for takeLazy4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for takeLazy4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for rotateRev4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call revAppend4[T](f, a, scr14._2))' VC for rotateRev4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call drop6[T](BigInt(2), f, scr14._2))' VC for rotateRev4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call take6[T](BigInt(2), f, a108._2))' VC for rotateRev4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call revAppend4[T](a109._1, a, a109._2))' VC for rotateRev4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for rotateRev4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for rotateDrop4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call drop6[T](i, f, rval2._2))' VC for rotateDrop4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call rotateRev4[T](r, a113._1, EagerStream[T] ...)' VC for rotateDrop4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call drop6[T](BigInt(2), f, rval2._2))' VC for rotateDrop4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for rotateDrop4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for TakeLazy@takeLazyLem1 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for RotateRev@rotateRevLem1 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call drop6[T](BigInt(2), f, scr14._2))' VC for RotateRev@rotateRevLem1 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call take6[T](BigInt(2), f, a108._2))' VC for RotateRev@rotateRevLem1 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call revAppend4[T](a109._1, a, a109._2))' VC for RotateRev@rotateRevLem1 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for RotateDrop@rotateDropLem1 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call drop6[T](BigInt(2), f, rval2._2))' VC for RotateDrop@rotateDropLem1 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (postcondition)' VC for takeLazyPreMonotone1 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (match exhaustiveness)' VC for takeLazyPreMonotone1 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for firstUneval4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for firstUneval4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for createQueue4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call rotateDrop4[T](r, i, f, st@))' VC for createQueue4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call takeLazy4[T](i, f, nr4._2))' VC for createQueue4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call rotateDrop4[T](f, j, r, st@))' VC for createQueue4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call takeLazy4[T](j, r, nf7._2))' VC for createQueue4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'division by zero' VC for createQueue4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'division by zero' VC for createQueue4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for force4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for force4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for forceTwice4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call force4[T](q.sf, q.f, q.r, q.sr, st@))' VC for forceTwice4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call force4[T](a118._1, q.f, q.r, q.sr, a118. ...)' VC for forceTwice4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call force4[T](q.sr, q.r, q.f, nsf6._1, nsf6. ...)' VC for forceTwice4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call force4[T](a119._1, q.r, q.f, nsf6._1, a1 ...)' VC for forceTwice4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for empty6 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for cons4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call force4[T](q.sf, q.f, q.r, q.sr, st@))' VC for cons4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call force4[T](q.sr, q.r, q.f, nsf7._1, nsf7. ...)' VC for cons4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call createQueue4[T](EagerStream[T](SCons[T]( ...)' VC for cons4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for tail29 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call force4[T](q.f, q.sf, q.r, q.sr, st@))' VC for tail29 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call tailSub4[T](q, scr17._2))' VC for tail29 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for tail29 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for tailSub4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call forceTwice4[T](q, scr18._2))' VC for tailSub4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call createQueue4[T](nf8, q.lenf - BigInt(1), ...)' VC for tailSub4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for tailSub4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for tailSub4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for reverse6 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (postcondition)' VC for funeCompose4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (precond. (call funeCompose-VCTact[T](tail, st1, st2)))' VC for funeCompose4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (match exhaustiveness)' VC for funeCompose4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for funeMonotone4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call funeCompose4[T](l1, st1, st2))' VC for funeMonotone4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call funeCompose4[T](l2, st1, st2))' VC for funeMonotone4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'precond. (call funeMonotone4[T](tail28, l2, st1, st2, s ...)' VC for funeMonotone4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for funeMonotone4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for size9 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for size9 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for isEmpty11 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for valid5 @?:?...
[ Info ] => VALID
┌──────────────────────┐
╔═╡ Verification Summary ╞══════════════════════════════════════════════════════════════════════════════════════════════════════════════╗
║ └──────────────────────┘ ║
║ RealTimeDeque.RotateDrop@rotateDropLem postcondition ?:? valid U:smt-z3 0.192 ║
║ RealTimeDeque.RotateDrop@rotateDropLem precond. (call drop6[T](BigInt(2), f, rval2._2)) ?:? valid U:smt-z3 0.159 ║
║ RealTimeDeque.RotateRev@rotateRevLem postcondition ?:? valid U:smt-cvc4 0.554 ║
║ RealTimeDeque.RotateRev@rotateRevLem precond. (call drop6[T](BigInt(2), f, scr14._2)) ?:? valid U:smt-z3 0.211 ║
║ RealTimeDeque.RotateRev@rotateRevLem precond. (call revAppend4[T](a109._1, a, a109._2)) ?:? valid U:smt-z3 0.257 ║
║ RealTimeDeque.RotateRev@rotateRevLem precond. (call take6[T](BigInt(2), f, a108._2)) ?:? valid U:smt-z3 0.097 ║
║ RealTimeDeque.TakeLazy@takeLazyLem postcondition ?:? valid U:smt-z3 0.124 ║
║ RealTimeDeque.cons postcondition ?:? valid U:smt-z3 0.210 ║
║ RealTimeDeque.cons precond. (call createQueue4[T](EagerStream[T](SCons[T]( ...) ?:? valid U:smt-z3 0.196 ║
║ RealTimeDeque.cons precond. (call force4[T](q.sf, q.f, q.r, q.sr, st@)) ?:? valid U:smt-z3 0.098 ║
║ RealTimeDeque.cons precond. (call force4[T](q.sr, q.r, q.f, nsf7._1, nsf7. ...) ?:? valid U:smt-z3 0.146 ║
║ RealTimeDeque.createQueue division by zero ?:? valid U:smt-z3 0.014 ║
║ RealTimeDeque.createQueue division by zero ?:? valid U:smt-z3 0.013 ║
║ RealTimeDeque.createQueue postcondition ?:? valid U:smt-z3 6.033 ║
║ RealTimeDeque.createQueue precond. (call rotateDrop4[T](f, j, r, st@)) ?:? valid U:smt-z3 0.138 ║
║ RealTimeDeque.createQueue precond. (call rotateDrop4[T](r, i, f, st@)) ?:? valid U:smt-z3 0.120 ║
║ RealTimeDeque.createQueue precond. (call takeLazy4[T](i, f, nr4._2)) ?:? valid U:smt-z3 0.143 ║
║ RealTimeDeque.createQueue precond. (call takeLazy4[T](j, r, nf7._2)) ?:? valid U:smt-z3 0.133 ║
║ RealTimeDeque.drop match exhaustiveness ?:? valid U:smt-z3 0.013 ║
║ RealTimeDeque.drop postcondition ?:? valid U:smt-z3 0.104 ║
║ RealTimeDeque.drop precond. (call drop6[T](n - BigInt(1), tail22, scr11._2 ...) ?:? valid U:smt-z3 0.141 ║
║ RealTimeDeque.empty postcondition ?:? valid U:smt-z3 0.009 ║
║ RealTimeDeque.firstUneval match exhaustiveness ?:? valid U:smt-z3 0.011 ║
║ RealTimeDeque.firstUneval postcondition ?:? valid U:smt-z3 0.136 ║
║ RealTimeDeque.force match exhaustiveness ?:? valid U:smt-z3 0.011 ║
║ RealTimeDeque.force postcondition ?:? valid U:smt-z3 0.200 ║
║ RealTimeDeque.forceTwice postcondition ?:? valid U:smt-z3 0.174 ║
║ RealTimeDeque.forceTwice precond. (call force4[T](a118._1, q.f, q.r, q.sr, a118. ...) ?:? valid U:smt-z3 0.122 ║
║ RealTimeDeque.forceTwice precond. (call force4[T](a119._1, q.r, q.f, nsf6._1, a1 ...) ?:? valid U:smt-z3 0.192 ║
║ RealTimeDeque.forceTwice precond. (call force4[T](q.sf, q.f, q.r, q.sr, st@)) ?:? valid U:smt-z3 0.090 ║
║ RealTimeDeque.forceTwice precond. (call force4[T](q.sr, q.r, q.f, nsf6._1, nsf6. ...) ?:? valid U:smt-z3 0.180 ║
║ RealTimeDeque.funeCompose tact (match exhaustiveness) ?:? valid U:smt-z3 0.015 ║
║ RealTimeDeque.funeCompose tact (postcondition) ?:? valid U:smt-z3 0.080 ║
║ RealTimeDeque.funeCompose tact (precond. (call funeCompose-VCTact[T](tail, st1, st2))) ?:? valid U:smt-z3 0.013 ║
║ RealTimeDeque.funeMonotone match exhaustiveness ?:? valid U:smt-z3 0.015 ║
║ RealTimeDeque.funeMonotone postcondition ?:? valid U:smt-z3 0.101 ║
║ RealTimeDeque.funeMonotone precond. (call funeCompose4[T](l1, st1, st2)) ?:? valid U:smt-z3 0.010 ║
║ RealTimeDeque.funeMonotone precond. (call funeCompose4[T](l2, st1, st2)) ?:? valid U:smt-z3 0.010 ║
║ RealTimeDeque.funeMonotone precond. (call funeMonotone4[T](tail28, l2, st1, st2, s ...) ?:? valid U:smt-z3 0.119 ║
║ RealTimeDeque.isConcrete match exhaustiveness ?:? valid U:smt-z3 0.025 ║
║ RealTimeDeque.isConcrete postcondition ?:? valid U:smt-z3 0.127 ║
║ Queue.isEmpty postcondition ?:? valid U:smt-z3 0.014 ║
║ RealTimeDeque.revAppend match exhaustiveness ?:? valid U:smt-z3 0.011 ║
║ RealTimeDeque.revAppend postcondition ?:? valid U:smt-z3 3.212 ║
║ RealTimeDeque.revAppend precond. (call revAppend4[T](tail21, EagerStream[T](SCo ...) ?:? valid U:smt-cvc4 3.497 ║
║ RealTimeDeque.reverse postcondition ?:? valid U:smt-z3 0.043 ║
║ RealTimeDeque.rotateDrop match exhaustiveness ?:? valid U:smt-z3 0.013 ║
║ RealTimeDeque.rotateDrop postcondition ?:? valid U:smt-z3 5.993 ║
║ RealTimeDeque.rotateDrop precond. (call drop6[T](BigInt(2), f, rval2._2)) ?:? valid U:smt-z3 0.135 ║
║ RealTimeDeque.rotateDrop precond. (call drop6[T](i, f, rval2._2)) ?:? valid U:smt-z3 0.134 ║
║ RealTimeDeque.rotateDrop precond. (call rotateRev4[T](r, a113._1, EagerStream[T] ...) ?:? valid U:smt-cvc4 13.052 ║
║ RealTimeDeque.rotateRev match exhaustiveness ?:? valid U:smt-z3 0.012 ║
║ RealTimeDeque.rotateRev postcondition ?:? valid U:smt-cvc4 26.796 ║
║ RealTimeDeque.rotateRev precond. (call drop6[T](BigInt(2), f, scr14._2)) ?:? valid U:smt-cvc4 0.188 ║
║ RealTimeDeque.rotateRev precond. (call revAppend4[T](a109._1, a, a109._2)) ?:? valid U:smt-z3 0.328 ║
║ RealTimeDeque.rotateRev precond. (call revAppend4[T](f, a, scr14._2)) ?:? valid U:smt-z3 0.069 ║
║ RealTimeDeque.rotateRev precond. (call take6[T](BigInt(2), f, a108._2)) ?:? valid U:smt-z3 0.069 ║
║ Stream.size match exhaustiveness ?:? valid U:smt-z3 0.009 ║
║ Stream.size postcondition ?:? valid U:smt-z3 0.030 ║
║ RealTimeDeque.tail match exhaustiveness ?:? valid U:smt-z3 0.008 ║
║ RealTimeDeque.tail postcondition ?:? valid U:smt-z3 0.128 ║
║ RealTimeDeque.tail precond. (call force4[T](q.f, q.sf, q.r, q.sr, st@)) ?:? valid U:smt-z3 0.098 ║
║ RealTimeDeque.tail precond. (call tailSub4[T](q, scr17._2)) ?:? valid U:smt-z3 1.410 ║
║ RealTimeDeque.tailSub match exhaustiveness ?:? valid U:smt-z3 0.008 ║
║ RealTimeDeque.tailSub match exhaustiveness ?:? valid U:smt-z3 0.012 ║
║ RealTimeDeque.tailSub postcondition ?:? valid U:smt-z3 4.914 ║
║ RealTimeDeque.tailSub precond. (call createQueue4[T](nf8, q.lenf - BigInt(1), ...) ?:? valid U:smt-z3 9.632 ║
║ RealTimeDeque.tailSub precond. (call forceTwice4[T](q, scr18._2)) ?:? valid U:smt-z3 0.200 ║
║ RealTimeDeque.take match exhaustiveness ?:? valid U:smt-z3 0.013 ║
║ RealTimeDeque.take postcondition ?:? valid U:smt-z3 0.111 ║
║ RealTimeDeque.take precond. (call take6[T](n - BigInt(1), tail23, scr12._2 ...) ?:? valid U:smt-z3 0.180 ║
║ RealTimeDeque.takeLazy match exhaustiveness ?:? valid U:smt-z3 0.051 ║
║ RealTimeDeque.takeLazy postcondition ?:? valid U:smt-z3 0.534 ║
║ RealTimeDeque.takeLazyPreMonotone tact (match exhaustiveness) ?:? valid U:smt-z3 0.010 ║
║ RealTimeDeque.takeLazyPreMonotone tact (postcondition) ?:? valid U:smt-z3 0.046 ║
║ Queue.valid postcondition ?:? valid U:smt-z3 0.024 ║
╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
║ total: 76 valid: 76 invalid: 0 unknown 0 81.720 ║
╚═══════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════╝
[ Info ] Output written on leon.out
[ Info ] - Now considering 'postcondition' VC for revAppend-time @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for drop-time @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for take-time @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for takeLazy-time @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for rotateRev-time @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for rotateDrop-time @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for createQueue-time @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for force-time @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for cons-time @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for tail-time @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for tailSub-time @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for reverse-time @?:?...
[ Info ] => VALID
Resource Verification Results:
┌──────────────────────┐
╔═╡ Verification Summary ╞═══════════════════════════════════════════════════════════════════╗
║ └──────────────────────┘ ║
║ RealTimeDeque.cons-time postcondition ?:? valid U:smt-z3 0.221 ║
║ RealTimeDeque.createQueue-time postcondition ?:? valid U:smt-z3 0.232 ║
║ RealTimeDeque.drop-time postcondition ?:? valid U:smt-z3 0.088 ║
║ RealTimeDeque.force-time postcondition ?:? valid U:smt-z3 0.236 ║
║ RealTimeDeque.revAppend-time postcondition ?:? valid U:smt-z3 0.116 ║
║ RealTimeDeque.reverse-time postcondition ?:? valid U:smt-z3 0.010 ║
║ RealTimeDeque.rotateDrop-time postcondition ?:? valid U:smt-cvc4 5.778 ║
║ RealTimeDeque.rotateRev-time postcondition ?:? valid U:smt-z3 0.175 ║
║ RealTimeDeque.tail-time postcondition ?:? valid U:smt-z3 2.948 ║
║ RealTimeDeque.tailSub-time postcondition ?:? valid U:smt-z3 0.168 ║
║ RealTimeDeque.take-time postcondition ?:? valid U:smt-z3 0.096 ║
║ RealTimeDeque.takeLazy-time postcondition ?:? valid U:smt-z3 0.075 ║
╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
║ total: 12 valid: 12 invalid: 0 unknown 0 10.143 ║
╚════════════════════════════════════════════════════════════════════════════════════════════╝
results/21-jan/RTQ.out deleted 100644 → 0
+ 0
− 102
View file @ 62be822d
[Warning ] warning: there were 8 feature warnings; re-run with -feature for details
[ Info ] Output written on leon.out
[ Info ] Output written on leon.out
[ Info ] Output written on leon.out
[ Info ] - Now considering 'postcondition' VC for ssize4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for isConcrete4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for isConcrete4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for rotate6 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for rotate6 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for firstUnevaluated4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for firstUnevaluated4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for enqueue4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for enqueue4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for dequeue4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for dequeue4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for dequeue4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for Rotate@rotateLem1 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for Rotate@enqueueLem1 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for Rotate@dequeueLem1 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (postcondition)' VC for rotatePreMonotone1 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'tact (match exhaustiveness)' VC for rotatePreMonotone1 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for isEmpty14 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for isEmpty14 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for isCons5 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for isCons5 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for size9 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for size9 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for isEmpty15 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for valid5 @?:?...
[ Info ] => VALID
┌──────────────────────┐
╔═╡ Verification Summary ╞══════════════════════════════════════════════════════════════════════╗
║ └──────────────────────┘ ║
║ RealTimeQueue.Rotate@dequeueLem postcondition ?:? valid U:smt-z3 0.456 ║
║ RealTimeQueue.Rotate@enqueueLem postcondition ?:? valid U:smt-z3 0.217 ║
║ RealTimeQueue.Rotate@rotateLem postcondition ?:? valid U:smt-z3 0.069 ║
║ RealTimeQueue.dequeue match exhaustiveness ?:? valid U:smt-z3 0.015 ║
║ RealTimeQueue.dequeue match exhaustiveness ?:? valid U:smt-z3 0.090 ║
║ RealTimeQueue.dequeue postcondition ?:? valid U:smt-z3 4.931 ║
║ RealTimeQueue.enqueue match exhaustiveness ?:? valid U:smt-z3 0.012 ║
║ RealTimeQueue.enqueue postcondition ?:? valid U:smt-z3 3.215 ║
║ RealTimeQueue.firstUnevaluated match exhaustiveness ?:? valid U:smt-z3 0.013 ║
║ RealTimeQueue.firstUnevaluated postcondition ?:? valid U:smt-z3 0.418 ║
║ RealTimeQueue.isConcrete match exhaustiveness ?:? valid U:smt-z3 0.027 ║
║ RealTimeQueue.isConcrete postcondition ?:? valid U:smt-z3 0.098 ║
║ Stream.isCons match exhaustiveness ?:? valid U:smt-z3 0.018 ║
║ Stream.isCons postcondition ?:? valid U:smt-z3 0.019 ║
║ Stream.isEmpty match exhaustiveness ?:? valid U:smt-z3 0.011 ║
║ Queue.isEmpty postcondition ?:? valid U:smt-z3 0.010 ║
║ Stream.isEmpty postcondition ?:? valid U:smt-z3 0.009 ║
║ RealTimeQueue.rotate match exhaustiveness ?:? valid U:smt-z3 0.069 ║
║ RealTimeQueue.rotate postcondition ?:? valid U:smt-cvc4 129.792 ║
║ RealTimeQueue.rotatePreMonotone tact (match exhaustiveness) ?:? valid U:smt-z3 0.011 ║
║ RealTimeQueue.rotatePreMonotone tact (postcondition) ?:? valid U:smt-z3 0.025 ║
║ Stream.size match exhaustiveness ?:? valid U:smt-z3 0.009 ║
║ Stream.size postcondition ?:? valid U:smt-z3 0.026 ║
║ RealTimeQueue.ssize postcondition ?:? valid U:smt-z3 0.599 ║
║ Queue.valid postcondition ?:? valid U:smt-z3 0.013 ║
╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
║ total: 25 valid: 25 invalid: 0 unknown 0 140.172 ║
╚═══════════════════════════════════════════════════════════════════════════════════════════════╝
[ Info ] Output written on leon.out
[ Info ] - Now considering 'postcondition' VC for rotate-time @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for enqueue-time @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for dequeue-time @?:?...
[ Info ] => VALID
Resource Verification Results:
┌──────────────────────┐
╔═╡ Verification Summary ╞═══════════════════════════════════════════════════════════════════╗
║ └──────────────────────┘ ║
║ RealTimeQueue.dequeue-time postcondition ?:? valid U:smt-z3 0.394 ║
║ RealTimeQueue.enqueue-time postcondition ?:? valid U:smt-z3 0.160 ║
║ RealTimeQueue.rotate-time postcondition ?:? valid U:smt-z3 0.078 ║
╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
║ total: 3 valid: 3 invalid: 0 unknown 0 0.632 ║
╚════════════════════════════════════════════════════════════════════════════════════════════╝
results/21-jan/Sort.out deleted 100644 → 0
+ 0
− 75
View file @ 62be822d
[Warning ] warning: there was one feature warning; re-run with -feature for details
[ Info ] Output written on leon.out
[ Info ] Output written on leon.out
[ Info ] Output written on leon.out
[ Info ] - Now considering 'postcondition' VC for ssize4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for pullMin4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for pullMin4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for pullMin4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for sort4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for sort4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for concat4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for concat4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for secondMin4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for secondMin4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for secondMin4 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for size14 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for size14 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for size15 @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'match exhaustiveness' VC for size15 @?:?...
[ Info ] => VALID
┌──────────────────────┐
╔═╡ Verification Summary ╞═══════════════════════════════════════════════════════════════════╗
║ └──────────────────────┘ ║
║ SortingnConcat.concat match exhaustiveness ?:? valid U:smt-z3 0.011 ║
║ SortingnConcat.concat postcondition ?:? valid U:smt-z3 0.032 ║
║ SortingnConcat.pullMin match exhaustiveness ?:? valid U:smt-z3 0.011 ║
║ SortingnConcat.pullMin match exhaustiveness ?:? valid U:smt-z3 0.021 ║
║ SortingnConcat.pullMin postcondition ?:? valid U:smt-z3 0.107 ║
║ SortingnConcat.secondMin match exhaustiveness ?:? valid U:smt-z3 0.018 ║
║ SortingnConcat.secondMin match exhaustiveness ?:? valid U:smt-z3 0.021 ║
║ SortingnConcat.secondMin postcondition ?:? valid U:smt-z3 0.065 ║
║ List.size match exhaustiveness ?:? valid U:smt-z3 0.010 ║
║ LList.size match exhaustiveness ?:? valid U:smt-z3 0.011 ║
║ LList.size postcondition ?:? valid U:smt-z3 0.027 ║
║ List.size postcondition ?:? valid U:smt-z3 0.012 ║
║ SortingnConcat.sort match exhaustiveness ?:? valid U:smt-z3 0.011 ║
║ SortingnConcat.sort postcondition ?:? valid U:smt-z3 0.220 ║
║ SortingnConcat.ssize postcondition ?:? valid U:smt-z3 0.096 ║
╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
║ total: 15 valid: 15 invalid: 0 unknown 0 0.673 ║
╚════════════════════════════════════════════════════════════════════════════════════════════╝
[ Info ] Output written on leon.out
[ Info ] - Now considering 'postcondition' VC for pullMin-time @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for sort-time @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for concat-time @?:?...
[ Info ] => VALID
[ Info ] - Now considering 'postcondition' VC for secondMin-time @?:?...
[ Info ] => VALID
Resource Verification Results:
┌──────────────────────┐
╔═╡ Verification Summary ╞═══════════════════════════════════════════════════════════════════╗
║ └──────────────────────┘ ║
║ SortingnConcat.concat-time postcondition ?:? valid U:smt-z3 0.026 ║
║ SortingnConcat.pullMin-time postcondition ?:? valid U:smt-z3 0.052 ║
║ SortingnConcat.secondMin-time postcondition ?:? valid U:smt-z3 0.305 ║
║ SortingnConcat.sort-time postcondition ?:? valid U:smt-z3 0.055 ║
╟┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄┄╢
║ total: 4 valid: 4 invalid: 0 unknown 0 0.438 ║
╚════════════════════════════════════════════════════════════════════════════════════════════╝
src/main/scala/leon/GlobalOptions.scala
+ 5
− 2
View file @ 3da15e71
......@@ -22,7 +22,9 @@ object GlobalOptions extends LeonComponent {
val optXLang = LeonFlagOptionDef("xlang", "Support for extra program constructs (imperative,...)", false)
val optWatch = LeonFlagOptionDef("watch", "Rerun pipeline when file changes", false)
val optSilent = LeonFlagOptionDef("silent", "Do not display progress messages or results to the console", false)
val optFunctions = new LeonOptionDef[Seq[String]] {
val name = "functions"
val description = "Only consider functions f1, f2, ..."
......@@ -78,6 +80,7 @@ object GlobalOptions extends LeonComponent {
optSelectedSolvers,
optDebug,
optWatch,
optTimeout
optTimeout,
optSilent
)
}
src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala
+ 3
− 0
View file @ 3da15e71
......@@ -34,6 +34,9 @@ object InferInvariantsPhase extends SimpleLeonPhase[Program, InferenceReport] {
val inferctx = new InferenceContext(program, ctx)
val report = (new InferenceEngine(inferctx)).runWithTimeout()
//println("Final Program: \n" +PrettyPrinter.apply(InferenceReportUtil.pushResultsToInput(inferctx, report.conditions)))
if(!ctx.findOption(GlobalOptions.optSilent).getOrElse(false)) {
println("Inference Result: \n"+report.summaryString)
}
report
}
}
src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala
+ 1
− 1
View file @ 3da15e71
......@@ -33,7 +33,7 @@ import PredicateUtil._
import SolverUtil._
object NLTemplateSolver {
val verbose = true
val verbose = false
}
class NLTemplateSolver(ctx: InferenceContext, program: Program,
......
src/main/scala/leon/laziness/LazinessEliminationPhase.scala
+ 16
− 12
View file @ 3da15e71
......@@ -10,12 +10,12 @@ import purescala.ExprOps._
import LazinessUtil._
import LazyVerificationPhase._
import utils._
import java.io.
_
import java.io._
import invariant.engine.InferenceReport
/**
* TODO: Function names are assumed to be small case. Fix this!!
*/
object LazinessEliminationPhase extends TransformationPhase {
object LazinessEliminationPhase extends SimpleLeonPhase[Program, LazyVerificationReport] {
val dumpInputProg = false
val dumpLiftProg = false
val dumpProgramWithClosures = false
......@@ -40,7 +40,7 @@ object LazinessEliminationPhase extends TransformationPhase {
/**
* TODO: add inlining annotations for optimization.
*/
def apply(ctx: LeonContext, prog: Program): Program = {
def apply(ctx: LeonContext, prog: Program): LazyVerificationReport = {
if (dumpInputProg)
println("Input prog: \n" + ScalaPrinter.apply(prog))
......@@ -74,8 +74,10 @@ object LazinessEliminationPhase extends TransformationPhase {
prettyPrintProgramToFile(progWOInstSpecs, ctx, "-woinst")
val checkCtx = contextForChecks(ctx)
if (!skipStateVerification)
checkSpecifications(progWOInstSpecs, checkCtx)
val stateVeri =
if (!skipStateVerification)
Some(checkSpecifications(progWOInstSpecs, checkCtx))
else None
// instrument the program for resources (note: we avoid checking preconditions again here)
val instrumenter = new LazyInstrumenter(InliningPhase.apply(ctx, typeCorrectProg), ctx, closureFactory)
......@@ -83,11 +85,12 @@ object LazinessEliminationPhase extends TransformationPhase {
if (dumpInstrumentedProgram)
prettyPrintProgramToFile(instProg, ctx, "-withinst", uniqueIds = true)
// check specifications (to be moved to a different phase)
if (!skipResourceVerification)
checkInstrumentationSpecs(instProg, checkCtx,
checkCtx.findOption(LazinessEliminationPhase.optUseOrb).getOrElse(false))
// dump stats
val resourceVeri =
if (!skipResourceVerification)
Some(checkInstrumentationSpecs(instProg, checkCtx,
checkCtx.findOption(LazinessEliminationPhase.optUseOrb).getOrElse(false)))
else None
// dump stats if enabled
if (ctx.findOption(GlobalOptions.optBenchmark).getOrElse(false)) {
val modid = prog.units.find(_.isMainUnit).get.id
val filename = modid + "-stats.txt"
......@@ -97,7 +100,8 @@ object LazinessEliminationPhase extends TransformationPhase {
ctx.reporter.info("Stats dumped to file: " + filename)
pw.close()
}
instProg
// return a report
new LazyVerificationReport(stateVeri, resourceVeri)
}
/**
......
src/main/scala/leon/laziness/LazyVerificationPhase.scala
+ 17
− 4
View file @ 3da15e71
......@@ -20,6 +20,14 @@ object LazyVerificationPhase {
val debugInstVCs = false
val debugInferProgram = false
class LazyVerificationReport(val stateVerification: Option[VerificationReport],
val resourceVeri: Option[VerificationReport]) {
def inferReport= resourceVeri match {
case Some(inf: InferenceReport) => Some(inf)
case _ => None
}
}
def removeInstrumentationSpecs(p: Program): Program = {
def hasInstVar(e: Expr) = {
exists { e => InstUtil.InstTypes.exists(i => i.isInstVariable(e)) }(e)
......@@ -66,7 +74,7 @@ object LazyVerificationPhase {
Stats.updateCounterStats(withcvc.map(_._2.timeMs.getOrElse(0L)).sum, "CVC4-Time", "CVC4SolvedVCs")
}
def checkSpecifications(prog: Program, checkCtx: LeonContext) {
def checkSpecifications(prog: Program, checkCtx: LeonContext): VerificationReport = {
// convert 'axiom annotation to library
prog.definedFunctions.foreach { fd =>
if (fd.annotations.contains("axiom"))
......@@ -75,10 +83,13 @@ object LazyVerificationPhase {
val report = VerificationPhase.apply(checkCtx, prog)
// collect stats
collectCumulativeStats(report)
println(report.summaryString)
if(!checkCtx.findOption(GlobalOptions.optSilent).getOrElse(false)) {
println(report.summaryString)
}
report
}
def checkInstrumentationSpecs(p: Program, checkCtx: LeonContext, useOrb: Boolean) = {
def checkInstrumentationSpecs(p: Program, checkCtx: LeonContext, useOrb: Boolean): VerificationReport = {
p.definedFunctions.foreach { fd =>
if (fd.annotations.contains("axiom"))
fd.addFlag(Annotation("library", Seq()))
......@@ -106,7 +117,9 @@ object LazyVerificationPhase {
collectCumulativeStats(rep)
rep
}
println("Resource Verification Results: \n" + rep.summaryString)
if (!checkCtx.findOption(GlobalOptions.optSilent).getOrElse(false))
println("Resource Verification Results: \n" + rep.summaryString)
rep
}
def accessesSecondRes(e: Expr, resid: Identifier): Boolean =
......
src/test/resources/regression/orb/lazy/withconst/SortingnConcat.scala 0 → 100644
+ 82
− 0
View file @ 3da15e71
import leon._
import lazyeval._
import lang._
import annotation._
import instrumentation._
object SortingnConcat {
sealed abstract class LList {
def size: BigInt = {
this match {
case SNil() => BigInt(0)
case SCons(x, t) => 1 + ssize(t)
}
} ensuring (_ >= 0)
}
case class SCons(x: BigInt, tail: Lazy[LList]) extends LList
case class SNil() extends LList
def ssize(l: Lazy[LList]): BigInt = (l*).size
sealed abstract class List {
def size: BigInt = this match {
case Cons(_, xs) => 1 + xs.size
case _ => BigInt(0)
}
}
case class Cons(x: BigInt, tail: List) extends List
case class Nil() extends List
def pullMin(l: List): List = {
l match {
case Nil() => l
case Cons(x, xs) =>
pullMin(xs) match {
case Nil() => Cons(x, Nil())
case nxs @ Cons(y, ys) =>
if (x <= y) Cons(x, nxs)
else Cons(y, Cons(x, ys))
}
}
} ensuring (res => res.size == l.size && time <= 15 * l.size + 2)
def sort(l: List): LList = {
pullMin(l) match {
case Cons(x, xs) =>
// here, x is the minimum
SCons(x, $(sort(xs))) // sorts lazily only if needed
case _ =>
SNil()
}
} ensuring (res => res.size == l.size && time <= 15 * l.size + 20)
def concat(l1: List, l2: LList) : LList = {
l1 match {
case Cons(x, xs) => SCons(x, $(concat(xs, l2)))
case Nil() => SNil()
}
} ensuring(res => time <= 15)
def secondMin(l: Lazy[LList]) : BigInt = {
l.value match {
case SCons(x, xs) =>
xs.value match {
case SCons(y, ys) => y
case SNil() => x
}
case SNil() => BigInt(0)
}
} ensuring (_ => time <= 30 * ssize(l) + 40)
/* Orb can prove this
* def kthMin(l: Lazy[LList], k: BigInt): BigInt = {
require(k >= 1)
l.value match {
case SCons(x, xs) =>
if (k == 1) x
else
kthMin(xs, k - 1)
case SNil() => BigInt(0) // None[BigInt]
}
} ensuring (_ => time <= 15 * k * ssize(l) + 20 * k + 20)*/
}
src/test/resources/regression/orb/lazy/withconst/WeightedScheduling.scala 0 → 100644
+ 104
− 0
View file @ 3da15e71
import leon._
import leon.mem._
import leon.lang._
import leon.annotation._
import leon.instrumentation._
//import leon.invariant._
object WeightedSched {
sealed abstract class IList {
def size: BigInt = {
this match {
case Cons(_, tail) => 1 + tail.size
case Nil() => BigInt(0)
}
} ensuring(_ >= 0)
}
case class Cons(x: BigInt, tail: IList) extends IList
case class Nil() extends IList
/**
* array of jobs
* (a) each job has a start time, finish time, and weight
* (b) Jobs are sorted in ascending order of finish times
*/
@ignore
var jobs = Array[(BigInt, BigInt, BigInt)]()
/**
* A precomputed mapping from each job i to the previous job j it is compatible with.
*/
@ignore
var p = Array[Int]()
@extern
def jobInfo(i: BigInt) = {
jobs(i.toInt)
} ensuring(_ => time <= 1)
@extern
def prevCompatibleJob(i: BigInt) = {
BigInt(p(i.toInt))
} ensuring(res => res >=0 && res < i && time <= 1)
@inline
def max(x: BigInt, y: BigInt) = if (x >= y) x else y
def depsEval(i: BigInt) = i == 0 || (i > 0 && allEval(i-1))
def allEval(i: BigInt): Boolean = {
require(i >= 0)
sched(i).isCached &&
(if (i == 0) true
else allEval(i - 1))
}
@traceInduct
def evalMono(i: BigInt, st1: Set[Mem[BigInt]], st2: Set[Mem[BigInt]]) = {
require(i >= 0)
(st1.subsetOf(st2) && (allEval(i) withState st1)) ==> (allEval(i) withState st2)
} holds
@traceInduct
def evalLem(x: BigInt, y: BigInt) = {
require(x >= 0 && y >= 0)
(x <= y && allEval(y)) ==> allEval(x)
} holds
@invstate
@memoize
def sched(jobIndex: BigInt): BigInt = {
require(depsEval(jobIndex) &&
(jobIndex == 0 || evalLem(prevCompatibleJob(jobIndex), jobIndex-1)))
val (st, fn, w) = jobInfo(jobIndex)
if(jobIndex == 0) w
else {
// we may either include the head job or not:
// if we include the head job, we have to skip every job that overlaps with it
val tailValue = sched(jobIndex - 1)
val prevCompatVal = sched(prevCompatibleJob(jobIndex))
max(w + prevCompatVal, tailValue)
}
} ensuring(_ => time <= 100)
def invoke(jobIndex: BigInt) = {
require(depsEval(jobIndex))
sched(jobIndex)
} ensuring (res => {
val in = inState[BigInt]
val out = outState[BigInt]
(jobIndex == 0 || evalMono(jobIndex-1, in, out)) &&
time <= 150
})
def schedBU(jobi: BigInt): IList = {
require(jobi >= 0)
if(jobi == 0) {
Cons(invoke(jobi), Nil())
} else {
val tailRes = schedBU(jobi-1)
Cons(invoke(jobi), tailRes)
}
} ensuring(_ => allEval(jobi) &&
time <= 200 * (jobi + 1))
}
src/test/resources/regression/orb/lazy/withorb/Concat.scala 0 → 100644
+ 77
− 0
View file @ 3da15e71
package withOrb
import leon._
import lazyeval._
import lazyeval.Lazy._
import lang._
import annotation._
import instrumentation._
import collection._
import invariant._
object Concat {
sealed abstract class LList[T] {
def size: BigInt = {
this match {
case SNil() => BigInt(0)
case SCons(x, t) => 1 + ssize(t)
}
} ensuring (_ >= 0)
}
case class SCons[T](x: T, tail: Lazy[LList[T]]) extends LList[T]
case class SNil[T]() extends LList[T]
def ssize[T](l: Lazy[LList[T]]): BigInt = (l*).size
def concat[T](l1: List[T], l2: List[T]): LList[T] = {
l1 match {
case Cons(x, xs) => SCons(x, $(concat(xs, l2)))
case Nil() => SNil[T]()
}
} ensuring { _ => time <= ? }
def kthElem[T](l: Lazy[LList[T]], k: BigInt): Option[T] = {
require(k >= 0)
l.value match {
case SCons(x, xs) =>
if (k == 0) Some(x)
else
kthElem(xs, k - 1)
case SNil() => None[T]
}
} ensuring (_ => time <= ? * k + ?)
def concatnSelect[T](l1: List[T], l2: List[T], k: BigInt): Option[T] = {
require(k >= 0)
kthElem($(concat(l1, l2)), k)
} ensuring (_ => time <= ? * k + ?)
@ignore
def main(args: Array[String]) = {
import stats._
println("Running concat test...")
val length = 1000000
val k = 10
val iterCount = 10
val l1 = (0 until length).foldRight(List[BigInt]()) {
case (i, acc) => i :: acc
}
val l2 = (0 until length).foldRight(List[BigInt]()) {
case (i, acc) => 2 * i :: acc
}
println("Created inputs, starting operations...")
def iterate[T](op: => BigInt) = {
var res = BigInt(0)
var i = iterCount
while (i > 0) {
res = op
i -= 1
}
res
}
val elem1 = timed { iterate((l1 ++ l2)(k)) } { t => println(s"Eager Concat completed in ${t / 1000.0} sec") }
println(s"$k th element of concatenated list: $elem1")
val elem2 = timed { iterate(concatnSelect(l1, l2, k).get) } { t => println(s"Lazy ConcatnSelect completed in ${t / 1000.0} sec") }
println(s"$k th element of concatenated list: $elem2")
assert(elem1 == elem2)
}
}
src/test/resources/regression/orb/lazy/withorb/SortingnConcat.scala 0 → 100644
+ 74
− 0
View file @ 3da15e71
package withOrb
import leon._
import lazyeval._
import lang._
import annotation._
import instrumentation._
import invariant._
object SortingnConcat {
// TODO: making this parametric will break many things. Fix them
sealed abstract class LList {
def size: BigInt = {
this match {
case SNil() => BigInt(0)
case SCons(x, t) => 1 + ssize(t)
}
} ensuring (_ >= 0)
}
case class SCons(x: BigInt, tail: Lazy[LList]) extends LList
case class SNil() extends LList
def ssize(l: Lazy[LList]): BigInt = (l*).size
sealed abstract class List {
def size: BigInt = this match {
case Cons(_, xs) => 1 + xs.size
case _ => BigInt(0)
}
}
case class Cons(x: BigInt, tail: List) extends List
case class Nil() extends List
def pullMin(l: List): List = {
l match {
case Nil() => l
case Cons(x, xs) =>
pullMin(xs) match {
case Nil() => Cons(x, Nil())
case nxs @ Cons(y, ys) =>
if (x <= y) Cons(x, nxs)
else Cons(y, Cons(x, ys))
}
}
} ensuring (res => res.size == l.size && time <= ? * l.size + ?)
def sort(l: List): LList = {
pullMin(l) match {
case Cons(x, xs) =>
// here, x is the minimum
SCons(x, $(sort(xs))) // sorts lazily only if needed
case _ =>
SNil()
}
} ensuring (res => res.size == l.size && time <= ? * l.size + ?)
def concat(l1: List, l2: LList) : LList = {
l1 match {
case Cons(x, xs) => SCons(x, $(concat(xs, l2)))
case Nil() => SNil()
}
} ensuring(res => time <= ?)
def kthMin(l: Lazy[LList], k: BigInt): BigInt = {
require(k >= 1)
l.value match {
case SCons(x, xs) =>
if (k == 1) x
else
kthMin(xs, k - 1)
case SNil() => BigInt(0)
}
} ensuring (_ => time <= ? * (k * ssize(l)) + ? * k + ?)
}
src/test/resources/regression/orb/lazy/withorb/WeightedScheduling.scala 0 → 100644
+ 133
− 0
View file @ 3da15e71
package orb
import leon._
import mem._
import lang._
import annotation._
import instrumentation._
import invariant._
object WeightedSched {
sealed abstract class IList {
def size: BigInt = {
this match {
case Cons(_, tail) => 1 + tail.size
case Nil() => BigInt(0)
}
} ensuring (_ >= 0)
}
case class Cons(x: BigInt, tail: IList) extends IList
case class Nil() extends IList
/**
* array of jobs
* (a) each job has a start time, finish time, and weight
* (b) Jobs are sorted in ascending order of finish times
* The first job should be (0,0,0) so that it acts as sentinel of every other job
*/
@ignore
var jobs = Array[(BigInt, BigInt, BigInt)]()
/**
* A precomputed mapping from each job i to the previous job j it is compatible with.
* The value of the first index could be anything.
*/
@ignore
var p = Array[Int]()
@extern
def jobInfo(i: BigInt) = {
jobs(i.toInt)
} ensuring (_ => time <= 1)
@extern
def prevCompatibleJob(i: BigInt) = {
BigInt(p(i.toInt))
} ensuring (res => res >= 0 && res < i && time <= 1)
@inline
def max(x: BigInt, y: BigInt) = if (x >= y) x else y
def depsEval(i: BigInt) = i == 0 || (i > 0 && allEval(i - 1))
def allEval(i: BigInt): Boolean = {
require(i >= 0)
sched(i).isCached &&
(if (i == 0) true
else allEval(i - 1))
}
@traceInduct
def evalMono(i: BigInt, st1: Set[Mem[BigInt]], st2: Set[Mem[BigInt]]) = {
require(i >= 0)
(st1.subsetOf(st2) && (allEval(i) withState st1)) ==> (allEval(i) withState st2)
} holds
@traceInduct
def evalLem(x: BigInt, y: BigInt) = {
require(x >= 0 && y >= 0)
(x <= y && allEval(y)) ==> allEval(x)
} holds
@invisibleBody
@invstate
@memoize
def sched(jobIndex: BigInt): BigInt = {
require(depsEval(jobIndex) &&
(jobIndex == 0 || evalLem(prevCompatibleJob(jobIndex), jobIndex - 1)))
val (st, fn, w) = jobInfo(jobIndex)
if (jobIndex == 0) w
else {
// we may either include the head job or not:
// if we include the head job, we have to skip every job that overlaps with it
val tailValue = sched(jobIndex - 1)
val prevCompatVal = sched(prevCompatibleJob(jobIndex))
max(w + prevCompatVal, tailValue)
}
} ensuring (_ => time <= ?)
@invisibleBody
def invoke(jobIndex: BigInt) = {
require(depsEval(jobIndex))
sched(jobIndex)
} ensuring (res => {
val in = inState[BigInt]
val out = outState[BigInt]
(jobIndex == 0 || evalMono(jobIndex - 1, in, out)) &&
time <= ?
})
@invisibleBody
def schedBU(jobi: BigInt): IList = {
require(jobi >= 0)
if (jobi == 0) {
Cons(invoke(jobi), Nil())
} else {
val tailRes = schedBU(jobi - 1)
Cons(invoke(jobi), tailRes)
}
} ensuring (_ => allEval(jobi) &&
time <= ? * (jobi + 1))
@ignore
def main(args: Array[String]) {
// note: we can run only one test in each run as the cache needs to be cleared between the tests,
// which is not currently supported by the api's (note: the methods access a mutable field)
test1()
//test2()
}
@ignore
def test1() {
jobs = Array((0, 0, 0), (1, 2, 5), (3, 4, 2), (3, 8, 5), (6, 7, 10), (8, 11, 11), (10, 13, 20))
p = Array(0 /* anything */ , 0, 1, 1, 2, 4, 4)
println("Schedule for 5 jobs of set 1: " + schedBU(6))
}
@ignore
def test2() {
jobs = Array((0, 0, 0), (1, 3, 5), (3, 4, 2), (3, 8, 5), (6, 7, 10), (8, 11, 11), (10, 13, 20))
p = Array(0 /* anything */ , 0, 0, 0, 2, 4, 4)
println("Schedule for 5 jobs of set 2: " + schedBU(6))
}
}
src/test/scala/leon/regression/orb/LazyEvalRegressionSuite.scala 0 → 100644
+ 60
− 0
View file @ 3da15e71
/* Copyright 2009-2016 EPFL, Lausanne */
package leon.regression.orb
import leon.test._
import leon._
import purescala.Definitions._
import invariant.engine._
import transformations._
import laziness._
import verification._
import java.io.File
class LazyEvalRegressionSuite extends LeonRegressionSuite {
private def forEachFileIn(path: String)(block: File => Unit) {
val fs = filesInResourceDir(path, _.endsWith(".scala"))
for (f <- fs) {
block(f)
}
}
private def testLazyVerification(f: File, ctx: LeonContext) {
val beginPipe = leon.frontends.scalac.ExtractionPhase andThen
new leon.utils.PreprocessingPhase
val (ctx2, program) = beginPipe.run(ctx, f.getAbsolutePath :: Nil)
val processPipe = LazinessEliminationPhase
val (ctx3, report) = processPipe.run(ctx2, program)
report.stateVerification match {
case None => fail(s"No state verification report found!")
case Some(rep) =>
val fails = rep.vrs.collect{ case (vc, vr) if !vr.isValid => vc }
if (!fails.isEmpty)
fail(s"State verification failed for functions ${fails.map(_.fd).mkString("\n")}")
}
report.resourceVeri match {
case None => fail(s"No resource verification report found!")
case Some(rep: VerificationReport) =>
val fails = rep.vrs.collect{ case (vc, vr) if !vr.isValid => vc }
if (!fails.isEmpty)
fail(s"Resource verification failed for functions ${fails.map(_.fd).mkString("\n")}")
case Some(rep: InferenceReport) =>
val fails = rep.conditions.filterNot(_.prettyInv.isDefined)
if (!fails.isEmpty)
fail(s"Inference failed for functions ${fails.map(_.fd).mkString("\n")}")
}
}
forEachFileIn("regression/orb/lazy/withconst") { f =>
test("Lazy evaluation w/o Orb: " + f.getName) {
testLazyVerification(f, createLeonContext("--lazy", "--silent", "--timeout=30"))
}
}
forEachFileIn("regression/orb/lazy/withorb") { f =>
test("Lazy evaluation with Orb: " + f.getName) {
testLazyVerification(f, createLeonContext("--lazy", "--useOrb", "--silent", "--vcTimeout=15", "--timeout=30"))
}
}
}
src/test/scala/leon/regression/orb/OrbRegressionSuite.scala
+ 1
− 1
View file @ 3da15e71
......@@ -19,7 +19,7 @@ class OrbRegressionSuite extends LeonRegressionSuite {
}
private def testInference(f: File, bound: Option[Int] = None) {
val ctx = createLeonContext("--inferInv", "--vcTimeout=3", "--solvers=smt-z3")
val ctx = createLeonContext("--inferInv", "--vcTimeout=3", "--solvers=smt-z3", "--silent")
val beginPipe = leon.frontends.scalac.ExtractionPhase andThen
new leon.utils.PreprocessingPhase
val (ctx2, program) = beginPipe.run(ctx, f.getAbsolutePath :: Nil)
......
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment