From 3da15e716c1b7131d4d96acd540dee70cc61906c Mon Sep 17 00:00:00 2001
From: ravi <ravi.kandhadai@epfl.ch>
Date: Wed, 23 Mar 2016 11:39:53 +0100
Subject: [PATCH] Adding a regression test suite for lazy evaluation

---
 results/21-jan/Conqueue.out                   | 294 ------------------
 results/21-jan/Esop.out                       |  47 ---
 results/21-jan/MsortBU.out                    | 138 --------
 results/21-jan/Num.out                        | 285 -----------------
 results/21-jan/NumRep.out                     |   0
 results/21-jan/RDQ.out                        | 282 -----------------
 results/21-jan/RTQ.out                        | 102 ------
 results/21-jan/Sort.out                       |  75 -----
 src/main/scala/leon/GlobalOptions.scala       |   7 +-
 .../engine/InferInvariantsPhase.scala         |   3 +
 .../templateSolvers/NLTemplateSolver.scala    |   2 +-
 .../laziness/LazinessEliminationPhase.scala   |  28 +-
 .../leon/laziness/LazyVerificationPhase.scala |  21 +-
 .../orb/lazy/withconst/SortingnConcat.scala   |  82 +++++
 .../lazy/withconst/WeightedScheduling.scala   | 104 +++++++
 .../regression/orb/lazy/withorb/Concat.scala  |  77 +++++
 .../orb/lazy/withorb/SortingnConcat.scala     |  74 +++++
 .../orb/lazy/withorb/WeightedScheduling.scala | 133 ++++++++
 .../orb/LazyEvalRegressionSuite.scala         |  60 ++++
 .../regression/orb/OrbRegressionSuite.scala   |   2 +-
 .../withconst/SortingnConcat.scala            |  18 +-
 21 files changed, 582 insertions(+), 1252 deletions(-)
 delete mode 100644 results/21-jan/Conqueue.out
 delete mode 100644 results/21-jan/Esop.out
 delete mode 100644 results/21-jan/MsortBU.out
 delete mode 100644 results/21-jan/Num.out
 delete mode 100644 results/21-jan/NumRep.out
 delete mode 100644 results/21-jan/RDQ.out
 delete mode 100644 results/21-jan/RTQ.out
 delete mode 100644 results/21-jan/Sort.out
 create mode 100644 src/test/resources/regression/orb/lazy/withconst/SortingnConcat.scala
 create mode 100644 src/test/resources/regression/orb/lazy/withconst/WeightedScheduling.scala
 create mode 100644 src/test/resources/regression/orb/lazy/withorb/Concat.scala
 create mode 100644 src/test/resources/regression/orb/lazy/withorb/SortingnConcat.scala
 create mode 100644 src/test/resources/regression/orb/lazy/withorb/WeightedScheduling.scala
 create mode 100644 src/test/scala/leon/regression/orb/LazyEvalRegressionSuite.scala

diff --git a/results/21-jan/Conqueue.out b/results/21-jan/Conqueue.out
deleted file mode 100644
index 52b99b93d..000000000
--- a/results/21-jan/Conqueue.out
+++ /dev/null
@@ -1,294 +0,0 @@
-[[33mWarning [0m] warning: there were 33 feature warnings; re-run with -feature for details
-[[34m  Info  [0m] Output written on leon.out
-[[34m  Info  [0m] Output written on leon.out
-[[34m  Info  [0m] Output written on leon.out
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for zeroPreceedsLazy4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for zeroPreceedsLazy4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for zeroPreceedsSuf4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for zeroPreceedsSuf4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for concreteUntil4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for concreteUntil4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for isConcrete4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for isConcrete4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for schedulesProperty4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for schedulesProperty4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for schedulesProperty4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for strongSchedsProp4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for strongSchedsProp4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for pushUntilCarry4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for pushUntilCarry4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for pushLeft4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call pushLeftLazy4[T](ys, xs, scr6._2))' VC for pushLeft4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for pushLeft4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for pushLeftLazy4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for pushLeftLazy4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for pushLeftLazy4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for PushLeftLazy@pushLeftLazyLem1 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for PushLeftLazy@pushLeftLazyLem1 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for PushLeftLazy@pushLeftLazyLem1 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (postcondition)' VC for pushLeftLazyPreMonotone1 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (match exhaustiveness)' VC for pushLeftLazyPreMonotone1 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for pushLeftLazyLemma4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call pushLeftLazyLemma4[T](CC[T](head, ys), r ...)' VC for pushLeftLazyLemma4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call pushLeftLazy4[T](ys, xs, a84._2))' VC for pushLeftLazyLemma4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for pushLeftLazyLemma4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for pushLeftLazyLemma4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for pushLeftLazyLemma4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for pushLeftWrapper4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call pushLeft4[T](ys, w.queue, st@))' VC for pushLeftWrapper4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for pushLeftWrapper4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for Pay4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for Pay4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for Pay4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for schedMonotone4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call schedMonotone4[T](st1, st2, tail, pushUn ...)' VC for schedMonotone4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for schedMonotone4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for schedMonotone4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (postcondition)' VC for concreteMonotone4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (match exhaustiveness)' VC for concreteMonotone4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (postcondition)' VC for concUntilMonotone4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (match exhaustiveness)' VC for concUntilMonotone4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for suffix4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for suffix4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for properSuffix4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for properSuffix4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (postcondition)' VC for suffixTrans4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (match exhaustiveness)' VC for suffixTrans4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (match exhaustiveness)' VC for suffixTrans4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for suffixTrans4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for suffixDisequality4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call suffixDisequality4[T](rear39, sufRear3))' VC for suffixDisequality4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for suffixDisequality4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (postcondition)' VC for suffixCompose4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (match exhaustiveness)' VC for suffixCompose4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (postcondition)' VC for concreteUntilIsSuffix4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (match exhaustiveness)' VC for concreteUntilIsSuffix4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (postcondition)' VC for concUntilExtenLemma4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (match exhaustiveness)' VC for concUntilExtenLemma4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (match exhaustiveness)' VC for concUntilExtenLemma4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for concUntilExtenLemma4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (postcondition)' VC for concUntilConcreteExten4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (match exhaustiveness)' VC for concUntilConcreteExten4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (postcondition)' VC for concUntilCompose4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (match exhaustiveness)' VC for concUntilCompose4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (postcondition)' VC for zeroPredSufConcreteUntilLemma4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (match exhaustiveness)' VC for zeroPredSufConcreteUntilLemma4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (postcondition)' VC for concreteZeroPredLemma4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (match exhaustiveness)' VC for concreteZeroPredLemma4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for suffixZeroLemma4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call suffixZeroLemma4[T](tail17, suf, suf2))' VC for suffixZeroLemma4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for suffixZeroLemma4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for pushLeftAndPay4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call pushLeftWrapper4[T](ys, w, st@))' VC for pushLeftAndPay4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call Pay4[T](q236, x$39._1._2, x$39._2))' VC for pushLeftAndPay4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for pushLeftAndPay4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for isEmpty9 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for level5 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for level5 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for isSpine5 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for isSpine5 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for isTip5 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for valid5 @?:?...
-[[34m  Info  [0m]  => 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 ║
-╚═══════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════╝
-[[34m  Info  [0m] Output written on leon.out
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for pushLeft-time @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for pushLeftLazy-time @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for pushLeftWrapper-time @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for Pay-time @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for pushLeftAndPay-time @?:?...
-[[34m  Info  [0m]  => 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 ║
-╚════════════════════════════════════════════════════════════════════════════════════════════╝
diff --git a/results/21-jan/Esop.out b/results/21-jan/Esop.out
deleted file mode 100644
index 4578488b9..000000000
--- a/results/21-jan/Esop.out
+++ /dev/null
@@ -1,47 +0,0 @@
-[[34m  Info  [0m] Output written on leon.out
-[[34m  Info  [0m] Output written on leon.out
-[[34m  Info  [0m] Output written on leon.out
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for zipWith4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for zipWith4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for nextFib4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for fibStream4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for nthFib4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call nthFib4(n - BigInt(1), tail9, scr3._2))' VC for nthFib4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for nthFib4 @?:?...
-[[34m  Info  [0m]  => 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 ║
-╚═══════════════════════════════════════════════════════════════════════════════════════════════════════════════════╝
-[[34m  Info  [0m] Output written on leon.out
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for zipWith-time @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for nextFib-time @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for nthFib-time @?:?...
-[[34m  Info  [0m]  => 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 ║
-╚════════════════════════════════════════════════════════════════════════════════════════════╝
diff --git a/results/21-jan/MsortBU.out b/results/21-jan/MsortBU.out
deleted file mode 100644
index 6f2dda6dd..000000000
--- a/results/21-jan/MsortBU.out
+++ /dev/null
@@ -1,138 +0,0 @@
-[[33mWarning [0m] warning: there were 5 feature warnings; re-run with -feature for details
-[[34m  Info  [0m] Output written on leon.out
-[[34m  Info  [0m] Output written on leon.out
-[[34m  Info  [0m] Output written on leon.out
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for ssize4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for pairs4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call pairs4(rest, st@))' VC for pairs4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for pairs4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for constructMergeTree4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call pairs4(l, st@))' VC for constructMergeTree4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call constructMergeTree4(a77._1, a77._2))' VC for constructMergeTree4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for constructMergeTree4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for merge4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for merge4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for merge4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for Merge@pairsLem1 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call pairs4(rest, st@))' VC for Merge@pairsLem1 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for Merge@mergeLem2 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for Merge@mergeLem3 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (postcondition)' VC for mergePreMonotone1 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for IListToLList4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for IListToLList4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for mergeSort4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call constructMergeTree4(IListToLList4(l), st ...)' VC for mergeSort4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for mergeSort4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for mergeSort4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for firstMin4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for firstMin4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for size19 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for size19 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for size20 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for size20 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for size21 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for size21 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for valid5 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for valid5 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for fullSize5 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for fullSize5 @?:?...
-[[34m  Info  [0m]  => 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 ║
-╚═════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════╝
-[[34m  Info  [0m] Output written on leon.out
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for pairs-time @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for constructMergeTree-time @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for merge-time @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for IListToLList-time @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for mergeSort-time @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for firstMin-time @?:?...
-[[34m  Info  [0m]  => 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 ║
-╚════════════════════════════════════════════════════════════════════════════════════════════╝
diff --git a/results/21-jan/Num.out b/results/21-jan/Num.out
deleted file mode 100644
index d5744962b..000000000
--- a/results/21-jan/Num.out
+++ /dev/null
@@ -1,285 +0,0 @@
-[[33mWarning [0m] warning: there were 33 feature warnings; re-run with -feature for details
-[[34m  Info  [0m] Output written on leon.out
-[[34m  Info  [0m] Output written on leon.out
-[[34m  Info  [0m] Output written on leon.out
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for zeroPreceedsLazy4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for zeroPreceedsLazy4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for zeroPreceedsSuf4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for zeroPreceedsSuf4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for concreteUntil4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for concreteUntil4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for isConcrete4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for isConcrete4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for schedulesProperty4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for schedulesProperty4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for schedulesProperty4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for strongSchedsProp4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for strongSchedsProp4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for pushUntilCarry4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for pushUntilCarry4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for inc4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call incLazy4(xs, scr6._2))' VC for inc4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for inc4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for incLazy4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for incLazy4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for incLazy4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for IncLazy@incLazyLem1 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for IncLazy@incLazyLem1 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for IncLazy@incLazyLem1 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (postcondition)' VC for incLazyPreMonotone1 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (match exhaustiveness)' VC for incLazyPreMonotone1 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for incLazyLemma4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call incLazyLemma4[<untyped>](rear30, suf, st ...)' VC for incLazyLemma4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call incLazy4(xs, a83._2))' VC for incLazyLemma4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for incLazyLemma4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for incLazyLemma4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for incLazyLemma4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for incNum4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call inc4(w.digs, st@))' VC for incNum4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for incNum4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for Pay4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for Pay4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for Pay4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for schedMonotone4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call schedMonotone4[<untyped>](st1, st2, tail ...)' VC for schedMonotone4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for schedMonotone4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for schedMonotone4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (postcondition)' VC for concreteMonotone4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (match exhaustiveness)' VC for concreteMonotone4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (postcondition)' VC for concUntilMonotone4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (match exhaustiveness)' VC for concUntilMonotone4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for suffix4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for suffix4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for properSuffix4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for properSuffix4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (postcondition)' VC for suffixTrans4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (match exhaustiveness)' VC for suffixTrans4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (match exhaustiveness)' VC for suffixTrans4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for suffixTrans4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for suffixDisequality4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call suffixDisequality4[<untyped>](rear39, su ...)' VC for suffixDisequality4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for suffixDisequality4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (postcondition)' VC for suffixCompose4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (match exhaustiveness)' VC for suffixCompose4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (postcondition)' VC for concreteUntilIsSuffix4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (match exhaustiveness)' VC for concreteUntilIsSuffix4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (postcondition)' VC for concUntilExtenLemma4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (match exhaustiveness)' VC for concUntilExtenLemma4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (match exhaustiveness)' VC for concUntilExtenLemma4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for concUntilExtenLemma4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (postcondition)' VC for concUntilConcreteExten4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (match exhaustiveness)' VC for concUntilConcreteExten4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (postcondition)' VC for concUntilCompose4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (match exhaustiveness)' VC for concUntilCompose4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (postcondition)' VC for zeroPredSufConcreteUntilLemma4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (match exhaustiveness)' VC for zeroPredSufConcreteUntilLemma4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (postcondition)' VC for concreteZeroPredLemma4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (match exhaustiveness)' VC for concreteZeroPredLemma4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for suffixZeroLemma4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call suffixZeroLemma4[<untyped>](tail17, suf, ...)' VC for suffixZeroLemma4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for suffixZeroLemma4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for incAndPay4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call incNum4[<untyped>](w, st@))' VC for incAndPay4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call Pay4[<untyped>](q175, x$218._1._2, x$218 ...)' VC for incAndPay4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for incAndPay4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for isSpine5 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for isSpine5 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for isTip5 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for valid5 @?:?...
-[[34m  Info  [0m]  => 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 ║
-╚═══════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════╝
-[[34m  Info  [0m] Output written on leon.out
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for inc-time @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for incLazy-time @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for incNum-time @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for Pay-time @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for incAndPay-time @?:?...
-[[34m  Info  [0m]  => 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 ║
-╚════════════════════════════════════════════════════════════════════════════════════════════╝
diff --git a/results/21-jan/NumRep.out b/results/21-jan/NumRep.out
deleted file mode 100644
index e69de29bb..000000000
diff --git a/results/21-jan/RDQ.out b/results/21-jan/RDQ.out
deleted file mode 100644
index d6ed9e932..000000000
--- a/results/21-jan/RDQ.out
+++ /dev/null
@@ -1,282 +0,0 @@
-[[33mWarning [0m] warning: there were 15 feature warnings; re-run with -feature for details
-[[34m  Info  [0m] Output written on leon.out
-[[34m  Info  [0m] Output written on leon.out
-[[34m  Info  [0m] Output written on leon.out
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for isConcrete4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for isConcrete4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for revAppend4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call revAppend4[T](tail21, EagerStream[T](SCo ...)' VC for revAppend4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for revAppend4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for drop6 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call drop6[T](n - BigInt(1), tail22, scr11._2 ...)' VC for drop6 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for drop6 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for take6 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call take6[T](n - BigInt(1), tail23, scr12._2 ...)' VC for take6 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for take6 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for takeLazy4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for takeLazy4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for rotateRev4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call revAppend4[T](f, a, scr14._2))' VC for rotateRev4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call drop6[T](BigInt(2), f, scr14._2))' VC for rotateRev4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call take6[T](BigInt(2), f, a108._2))' VC for rotateRev4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call revAppend4[T](a109._1, a, a109._2))' VC for rotateRev4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for rotateRev4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for rotateDrop4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call drop6[T](i, f, rval2._2))' VC for rotateDrop4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call rotateRev4[T](r, a113._1, EagerStream[T] ...)' VC for rotateDrop4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call drop6[T](BigInt(2), f, rval2._2))' VC for rotateDrop4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for rotateDrop4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for TakeLazy@takeLazyLem1 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for RotateRev@rotateRevLem1 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call drop6[T](BigInt(2), f, scr14._2))' VC for RotateRev@rotateRevLem1 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call take6[T](BigInt(2), f, a108._2))' VC for RotateRev@rotateRevLem1 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call revAppend4[T](a109._1, a, a109._2))' VC for RotateRev@rotateRevLem1 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for RotateDrop@rotateDropLem1 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call drop6[T](BigInt(2), f, rval2._2))' VC for RotateDrop@rotateDropLem1 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (postcondition)' VC for takeLazyPreMonotone1 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (match exhaustiveness)' VC for takeLazyPreMonotone1 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for firstUneval4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for firstUneval4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for createQueue4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call rotateDrop4[T](r, i, f, st@))' VC for createQueue4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call takeLazy4[T](i, f, nr4._2))' VC for createQueue4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call rotateDrop4[T](f, j, r, st@))' VC for createQueue4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call takeLazy4[T](j, r, nf7._2))' VC for createQueue4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'division by zero' VC for createQueue4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'division by zero' VC for createQueue4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for force4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for force4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for forceTwice4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call force4[T](q.sf, q.f, q.r, q.sr, st@))' VC for forceTwice4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call force4[T](a118._1, q.f, q.r, q.sr, a118. ...)' VC for forceTwice4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call force4[T](q.sr, q.r, q.f, nsf6._1, nsf6. ...)' VC for forceTwice4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call force4[T](a119._1, q.r, q.f, nsf6._1, a1 ...)' VC for forceTwice4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for empty6 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for cons4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call force4[T](q.sf, q.f, q.r, q.sr, st@))' VC for cons4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call force4[T](q.sr, q.r, q.f, nsf7._1, nsf7. ...)' VC for cons4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call createQueue4[T](EagerStream[T](SCons[T]( ...)' VC for cons4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for tail29 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call force4[T](q.f, q.sf, q.r, q.sr, st@))' VC for tail29 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call tailSub4[T](q, scr17._2))' VC for tail29 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for tail29 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for tailSub4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call forceTwice4[T](q, scr18._2))' VC for tailSub4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call createQueue4[T](nf8, q.lenf - BigInt(1), ...)' VC for tailSub4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for tailSub4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for tailSub4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for reverse6 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (postcondition)' VC for funeCompose4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (precond. (call funeCompose-VCTact[T](tail, st1, st2)))' VC for funeCompose4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (match exhaustiveness)' VC for funeCompose4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for funeMonotone4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call funeCompose4[T](l1, st1, st2))' VC for funeMonotone4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call funeCompose4[T](l2, st1, st2))' VC for funeMonotone4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'precond. (call funeMonotone4[T](tail28, l2, st1, st2, s ...)' VC for funeMonotone4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for funeMonotone4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for size9 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for size9 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for isEmpty11 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for valid5 @?:?...
-[[34m  Info  [0m]  => 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 ║
-╚═══════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════════╝
-[[34m  Info  [0m] Output written on leon.out
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for revAppend-time @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for drop-time @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for take-time @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for takeLazy-time @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for rotateRev-time @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for rotateDrop-time @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for createQueue-time @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for force-time @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for cons-time @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for tail-time @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for tailSub-time @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for reverse-time @?:?...
-[[34m  Info  [0m]  => 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 ║
-╚════════════════════════════════════════════════════════════════════════════════════════════╝
diff --git a/results/21-jan/RTQ.out b/results/21-jan/RTQ.out
deleted file mode 100644
index 3631da364..000000000
--- a/results/21-jan/RTQ.out
+++ /dev/null
@@ -1,102 +0,0 @@
-[[33mWarning [0m] warning: there were 8 feature warnings; re-run with -feature for details
-[[34m  Info  [0m] Output written on leon.out
-[[34m  Info  [0m] Output written on leon.out
-[[34m  Info  [0m] Output written on leon.out
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for ssize4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for isConcrete4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for isConcrete4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for rotate6 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for rotate6 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for firstUnevaluated4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for firstUnevaluated4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for enqueue4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for enqueue4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for dequeue4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for dequeue4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for dequeue4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for Rotate@rotateLem1 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for Rotate@enqueueLem1 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for Rotate@dequeueLem1 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (postcondition)' VC for rotatePreMonotone1 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'tact (match exhaustiveness)' VC for rotatePreMonotone1 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for isEmpty14 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for isEmpty14 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for isCons5 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for isCons5 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for size9 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for size9 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for isEmpty15 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for valid5 @?:?...
-[[34m  Info  [0m]  => 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 ║
-╚═══════════════════════════════════════════════════════════════════════════════════════════════╝
-[[34m  Info  [0m] Output written on leon.out
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for rotate-time @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for enqueue-time @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for dequeue-time @?:?...
-[[34m  Info  [0m]  => 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 ║
-╚════════════════════════════════════════════════════════════════════════════════════════════╝
diff --git a/results/21-jan/Sort.out b/results/21-jan/Sort.out
deleted file mode 100644
index 62e69eb0d..000000000
--- a/results/21-jan/Sort.out
+++ /dev/null
@@ -1,75 +0,0 @@
-[[33mWarning [0m] warning: there was one feature warning; re-run with -feature for details
-[[34m  Info  [0m] Output written on leon.out
-[[34m  Info  [0m] Output written on leon.out
-[[34m  Info  [0m] Output written on leon.out
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for ssize4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for pullMin4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for pullMin4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for pullMin4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for sort4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for sort4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for concat4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for concat4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for secondMin4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for secondMin4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for secondMin4 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for size14 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for size14 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for size15 @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'match exhaustiveness' VC for size15 @?:?...
-[[34m  Info  [0m]  => 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 ║
-╚════════════════════════════════════════════════════════════════════════════════════════════╝
-[[34m  Info  [0m] Output written on leon.out
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for pullMin-time @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for sort-time @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for concat-time @?:?...
-[[34m  Info  [0m]  => VALID
-[[34m  Info  [0m]  - Now considering 'postcondition' VC for secondMin-time @?:?...
-[[34m  Info  [0m]  => 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 ║
-╚════════════════════════════════════════════════════════════════════════════════════════════╝
diff --git a/src/main/scala/leon/GlobalOptions.scala b/src/main/scala/leon/GlobalOptions.scala
index 9632926a6..9c5df4adb 100644
--- a/src/main/scala/leon/GlobalOptions.scala
+++ b/src/main/scala/leon/GlobalOptions.scala
@@ -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
   )
 }
diff --git a/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala b/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala
index e6c62ee93..e5866f5ee 100644
--- a/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala
+++ b/src/main/scala/leon/invariant/engine/InferInvariantsPhase.scala
@@ -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
   }
 }
diff --git a/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala b/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala
index 7a5dd39a9..79448c7c5 100644
--- a/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala
+++ b/src/main/scala/leon/invariant/templateSolvers/NLTemplateSolver.scala
@@ -33,7 +33,7 @@ import PredicateUtil._
 import SolverUtil._
 
 object NLTemplateSolver {
-  val verbose = true
+  val verbose = false
 }
 
 class NLTemplateSolver(ctx: InferenceContext, program: Program,
diff --git a/src/main/scala/leon/laziness/LazinessEliminationPhase.scala b/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
index 847dc3d06..9501f2dc3 100644
--- a/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
+++ b/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
@@ -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)
   }
 
   /**
diff --git a/src/main/scala/leon/laziness/LazyVerificationPhase.scala b/src/main/scala/leon/laziness/LazyVerificationPhase.scala
index b72bf59f7..fd063f9d7 100644
--- a/src/main/scala/leon/laziness/LazyVerificationPhase.scala
+++ b/src/main/scala/leon/laziness/LazyVerificationPhase.scala
@@ -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 =
diff --git a/src/test/resources/regression/orb/lazy/withconst/SortingnConcat.scala b/src/test/resources/regression/orb/lazy/withconst/SortingnConcat.scala
new file mode 100644
index 000000000..1899c30b6
--- /dev/null
+++ b/src/test/resources/regression/orb/lazy/withconst/SortingnConcat.scala
@@ -0,0 +1,82 @@
+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)*/
+}
diff --git a/src/test/resources/regression/orb/lazy/withconst/WeightedScheduling.scala b/src/test/resources/regression/orb/lazy/withconst/WeightedScheduling.scala
new file mode 100644
index 000000000..e640bd79e
--- /dev/null
+++ b/src/test/resources/regression/orb/lazy/withconst/WeightedScheduling.scala
@@ -0,0 +1,104 @@
+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))
+}
diff --git a/src/test/resources/regression/orb/lazy/withorb/Concat.scala b/src/test/resources/regression/orb/lazy/withorb/Concat.scala
new file mode 100644
index 000000000..b9653b522
--- /dev/null
+++ b/src/test/resources/regression/orb/lazy/withorb/Concat.scala
@@ -0,0 +1,77 @@
+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)
+  }
+}
diff --git a/src/test/resources/regression/orb/lazy/withorb/SortingnConcat.scala b/src/test/resources/regression/orb/lazy/withorb/SortingnConcat.scala
new file mode 100644
index 000000000..0f4c1151b
--- /dev/null
+++ b/src/test/resources/regression/orb/lazy/withorb/SortingnConcat.scala
@@ -0,0 +1,74 @@
+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 + ?)
+}
diff --git a/src/test/resources/regression/orb/lazy/withorb/WeightedScheduling.scala b/src/test/resources/regression/orb/lazy/withorb/WeightedScheduling.scala
new file mode 100644
index 000000000..fc254279b
--- /dev/null
+++ b/src/test/resources/regression/orb/lazy/withorb/WeightedScheduling.scala
@@ -0,0 +1,133 @@
+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))
+  }
+}
diff --git a/src/test/scala/leon/regression/orb/LazyEvalRegressionSuite.scala b/src/test/scala/leon/regression/orb/LazyEvalRegressionSuite.scala
new file mode 100644
index 000000000..580af747f
--- /dev/null
+++ b/src/test/scala/leon/regression/orb/LazyEvalRegressionSuite.scala
@@ -0,0 +1,60 @@
+/* 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"))
+    }
+  }
+}
diff --git a/src/test/scala/leon/regression/orb/OrbRegressionSuite.scala b/src/test/scala/leon/regression/orb/OrbRegressionSuite.scala
index 6c46aeb34..5bc2255db 100644
--- a/src/test/scala/leon/regression/orb/OrbRegressionSuite.scala
+++ b/src/test/scala/leon/regression/orb/OrbRegressionSuite.scala
@@ -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)
diff --git a/testcases/lazy-datastructures/withconst/SortingnConcat.scala b/testcases/lazy-datastructures/withconst/SortingnConcat.scala
index 20a62b828..1899c30b6 100644
--- a/testcases/lazy-datastructures/withconst/SortingnConcat.scala
+++ b/testcases/lazy-datastructures/withconst/SortingnConcat.scala
@@ -1,8 +1,8 @@
-import leon.lazyeval._
-import leon.lang._
-import leon.annotation._
-import leon.instrumentation._
-//import leon.invariant._
+import leon._
+import lazyeval._
+import lang._
+import annotation._
+import instrumentation._
 
 object SortingnConcat {
 
@@ -14,9 +14,9 @@ object SortingnConcat {
       }
     } ensuring (_ >= 0)
   }
-  case class SCons(x: BigInt, tail: $[LList]) extends LList
+  case class SCons(x: BigInt, tail: Lazy[LList]) extends LList
   case class SNil() extends LList
-  def ssize(l: $[LList]): BigInt = (l*).size
+  def ssize(l: Lazy[LList]): BigInt = (l*).size
 
   sealed abstract class List {
     def size: BigInt = this match {
@@ -57,7 +57,7 @@ object SortingnConcat {
     }
   } ensuring(res => time <= 15)
 
-  def secondMin(l: $[LList]) : BigInt = {
+  def secondMin(l: Lazy[LList]) : BigInt = {
     l.value match {
       case SCons(x, xs) =>
         xs.value match {
@@ -69,7 +69,7 @@ object SortingnConcat {
   } ensuring (_ => time <= 30 * ssize(l) + 40)
 
   /* Orb can prove this
-   * def kthMin(l: $[LList], k: BigInt): BigInt = {
+   * def kthMin(l: Lazy[LList], k: BigInt): BigInt = {
     require(k >= 1)
     l.value match {
       case SCons(x, xs) =>
-- 
GitLab