diff --git a/library/lazy/package.scala b/library/lazy/package.scala
index 6e47d8be74cb89c69ba52c42a30d6203692df09a..d706f0ec3d55902f8d0d5695b7bda08670560849 100644
--- a/library/lazy/package.scala
+++ b/library/lazy/package.scala
@@ -9,11 +9,27 @@ import scala.language.implicitConversions
 @library
 object $ {
   def apply[T](f: => T) = new $(Unit => f)
+  def eager[T](x: => T) = new $(Unit => x)
+  /**
+   * implicit conversion from eager evaluation to lazy evaluation
+   */
+  @inline //inlining call-by-name here
+  implicit def eagerToLazy[T](x: T) = eager(x)
 }
 
 @library
 case class $[T](f: Unit => T) { // leon does not support call by name as of now
-  lazy val value = f(())
-  def *  = f(())
-  def isEvaluated = true // for now this is a dummy function, but it will be made sound when leon supports mutable fields.
+  @extern
+  lazy val value = {
+    val x = f(())
+    eval = true
+    x
+  }
+  def * = f(())
+
+  @ignore
+  var eval = false // is this thread safe ?
+
+  @extern
+  def isEvaluated = eval
 }
diff --git a/src/main/scala/leon/invariant/datastructure/Graph.scala b/src/main/scala/leon/invariant/datastructure/Graph.scala
index 484f04668c08a6b02f8acfd2db12b343e4b4c303..e4dc9daf94a8516b1f95d108cbff2b97df34803b 100644
--- a/src/main/scala/leon/invariant/datastructure/Graph.scala
+++ b/src/main/scala/leon/invariant/datastructure/Graph.scala
@@ -52,10 +52,10 @@ class DirectedGraph[T] {
     else BFSReachRecur(src)
   }
 
-  def BFSReachables(src: T): Set[T] = {
+  def BFSReachables(srcs: Seq[T]): Set[T] = {
     var queue = List[T]()
     var visited = Set[T]()
-    visited += src
+    visited ++= srcs.toSet
 
     def BFSReachRecur(cur: T): Unit = {
       if (adjlist.contains(cur)) {
@@ -73,7 +73,7 @@ class DirectedGraph[T] {
       }
     }
 
-    BFSReachRecur(src)
+    srcs.foreach{src => BFSReachRecur(src) }
     visited
   }
 
@@ -150,6 +150,17 @@ class DirectedGraph[T] {
     state.components
   }
 
+  /**
+   * Reverses the direction of the edges in the graph
+   */
+  def reverse : DirectedGraph[T] = {
+    val revg = new DirectedGraph[T]()
+    adjlist.foreach{
+      case (src, dests) =>
+        dests.foreach { revg.addEdge(_, src) }
+    }
+    revg
+  }
 }
 
 class UndirectedGraph[T] extends DirectedGraph[T] {
diff --git a/src/main/scala/leon/invariant/util/CallGraph.scala b/src/main/scala/leon/invariant/util/CallGraph.scala
index 57ec6c38b9f539b3ab6ee312821c5b22d2644b5b..fafa24c6c56a47d38220e93a8e1dd8d34916177a 100644
--- a/src/main/scala/leon/invariant/util/CallGraph.scala
+++ b/src/main/scala/leon/invariant/util/CallGraph.scala
@@ -18,6 +18,7 @@ import invariant.datastructure._
  */
 class CallGraph {
   val graph = new DirectedGraph[FunDef]()
+  lazy val reverseCG = graph.reverse
 
   def addFunction(fd: FunDef) = graph.addNode(fd)
 
@@ -31,7 +32,19 @@ class CallGraph {
   }
 
   def transitiveCallees(src: FunDef): Set[FunDef] = {
-    graph.BFSReachables(src)
+    graph.BFSReachables(Seq(src))
+  }
+
+  def transitiveCallers(dest: FunDef) : Set[FunDef] = {
+    reverseCG.BFSReachables(Seq(dest))
+  }
+
+  def transitiveCallees(srcs: Seq[FunDef]): Set[FunDef] = {
+    graph.BFSReachables(srcs)
+  }
+
+  def transitiveCallers(dests: Seq[FunDef]) : Set[FunDef] = {
+    reverseCG.BFSReachables(dests)
   }
 
   def isRecursive(fd: FunDef): Boolean = {
diff --git a/src/main/scala/leon/invariant/util/TreeUtil.scala b/src/main/scala/leon/invariant/util/TreeUtil.scala
index 35533957da60b7169790cad75c5b674b36edc820..c6f5c70efa03fc352cb2f7b41034ec2ee1878a18 100644
--- a/src/main/scala/leon/invariant/util/TreeUtil.scala
+++ b/src/main/scala/leon/invariant/util/TreeUtil.scala
@@ -185,6 +185,44 @@ object ProgramUtil {
     newprog
   }
 
+  def updatePost(funToPost: Map[FunDef, Lambda], prog: Program,
+      uniqueIdDisplay: Boolean = true, excludeLibrary: Boolean = true): Program = {
+
+    val funMap = functionsWOFields(prog.definedFunctions).foldLeft(Map[FunDef, FunDef]()) {
+      case (accMap, fd) if fd.isTheoryOperation || fd.isLibrary =>
+        accMap + (fd -> fd)
+      case (accMap, fd) => {
+        val freshId = FreshIdentifier(fd.id.name, fd.returnType, uniqueIdDisplay)
+        val newfd = new FunDef(freshId, fd.tparams, fd.params, fd.returnType)
+        accMap.updated(fd, newfd)
+      }
+    }
+    val mapExpr = mapFunctionsInExpr(funMap) _
+    for ((from, to) <- funMap) {
+      to.fullBody = if (!funToPost.contains(from)) {
+        mapExpr(from.fullBody)
+      } else {
+        val newpost = funToPost(from)
+        mapExpr {
+          from.fullBody match {
+            case Ensuring(body, post) =>
+              Ensuring(body, newpost) // replace the old post with new post
+            case body =>
+              Ensuring(body, newpost)
+          }
+        }
+      }
+      //copy annotations
+      from.flags.foreach(to.addFlag(_))
+    }
+    val newprog = copyProgram(prog, (defs: Seq[Definition]) => defs.map {
+      case fd: FunDef if funMap.contains(fd) =>
+        funMap(fd)
+      case d => d
+    })
+    newprog
+  }
+
   def functionByName(nm: String, prog: Program) = {
     prog.definedFunctions.find(fd => fd.id.name == nm)
   }
diff --git a/src/main/scala/leon/laziness/LazinessEliminationPhase.scala b/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
index dcc5d830a20b16f78ef74b6008ceb60f70ce4643..5425760483dd4275bde55ec502ba8454a14f54ed 100644
--- a/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
+++ b/src/main/scala/leon/laziness/LazinessEliminationPhase.scala
@@ -22,6 +22,9 @@ import java.io.FileWriter
 import java.io.BufferedWriter
 import scala.util.matching.Regex
 import leon.purescala.PrettyPrinter
+import leon.solvers._
+import leon.solvers.z3._
+import leon.transformations._
 import leon.LeonContext
 import leon.LeonOptionDef
 import leon.Main
@@ -29,32 +32,48 @@ import leon.TransformationPhase
 import LazinessUtil._
 import invariant.datastructure._
 import invariant.util.ProgramUtil._
+import purescala.Constructors._
+import leon.verification._
+import PredicateUtil._
 
 object LazinessEliminationPhase extends TransformationPhase {
   val debugLifting = false
+  val dumpInputProg = false
+  val dumpLiftProg = false
   val dumpProgramWithClosures = false
   val dumpTypeCorrectProg = false
   val dumpProgWithPreAsserts = true
+  val dumpProgWOInstSpecs = false
   val dumpInstrumentedProgram = false
   val debugSolvers = false
-
   val skipVerification = false
   val prettyPrint = false
+  val debugInstVCs = false
 
   val name = "Laziness Elimination Phase"
   val description = "Coverts a program that uses lazy construct" +
     " to a program that does not use lazy constructs"
 
+  // options that control behavior
+  val optRefEquality = LeonFlagOptionDef("useRefEquality", "Uses reference equality which memoizing closures", false)
+
   /**
    * TODO: enforce that the specs do not create lazy closures
    * TODO: we are forced to make an assumption that lazy ops takes as type parameters only those
    * type parameters of their return type and not more. (enforce this)
    * TODO: Check that lazy types are not nested
+   * TODO: expose in/out state to the user level, so that they can be used in specs
+   * For now using lazyinv annotation
    */
   def apply(ctx: LeonContext, prog: Program): Program = {
 
+    if (dumpInputProg)
+      println("Input prog: \n" + ScalaPrinter.apply(prog))
     val nprog = liftLazyExpressions(prog)
-    val progWithClosures = (new LazyClosureConverter(nprog, new LazyClosureFactory(nprog))).apply
+    if(dumpLiftProg)
+      println("After lifting expressions: \n" + ScalaPrinter.apply(nprog))
+
+    val progWithClosures = (new LazyClosureConverter(nprog, ctx, new LazyClosureFactory(nprog))).apply
     if (dumpProgramWithClosures)
       println("After closure conversion: \n" + ScalaPrinter.apply(progWithClosures))
 
@@ -69,14 +88,24 @@ object LazinessEliminationPhase extends TransformationPhase {
       prettyPrintProgramToFile(progWithPre, ctx)
     }
 
-    // instrument the program for resources
-    val instProg = (new LazyInstrumenter(progWithPre)).apply
-    if (dumpInstrumentedProgram)
+    // verify the contracts that do not use resources
+    val progWOInstSpecs = removeInstrumentationSpecs(progWithPre)
+    if (dumpProgWOInstSpecs) {
+      println("After removing instrumentation specs: \n" + ScalaPrinter.apply(progWOInstSpecs))
+    }
+    if (!skipVerification)
+      checkSpecifications(progWOInstSpecs)
+
+    // instrument the program for resources (note: we avoid checking preconditions again here)
+    val instProg = (new LazyInstrumenter(typeCorrectProg)).apply
+    if (dumpInstrumentedProgram){
       println("After instrumentation: \n" + ScalaPrinter.apply(instProg))
+      prettyPrintProgramToFile(instProg, ctx)
+    }
 
     // check specifications (to be moved to a different phase)
     if (!skipVerification)
-      checkSpecifications(instProg)
+      checkInstrumentationSpecs(instProg)
     if (prettyPrint)
       prettyPrintProgramToFile(instProg, ctx)
     instProg
@@ -103,6 +132,7 @@ object LazinessEliminationPhase extends TransformationPhase {
       md.definedFunctions.foreach {
         case fd if fd.hasBody && !fd.isLibrary =>
           val nbody = simplePostTransform {
+            // is the arugment of lazy invocation not a function ?
             case finv @ FunctionInvocation(lazytfd, Seq(arg)) if isLazyInvocation(finv)(prog) && !arg.isInstanceOf[FunctionInvocation] =>
               val freevars = variablesOf(arg).toList
               val tparams = freevars.map(_.getType) flatMap getTypeParameters distinct
@@ -122,32 +152,54 @@ object LazinessEliminationPhase extends TransformationPhase {
               FunctionInvocation(lazytfd, Seq(FunctionInvocation(TypedFunDef(argfun, tparams),
                 freevars.map(_.toVariable))))
 
+            // is the argument of eager invocation not a variable ?
+            case finv @ FunctionInvocation(TypedFunDef(fd, _), Seq(arg)) if isEagerInvocation(finv)(prog) && !arg.isInstanceOf[Variable] =>
+              val rootType = bestRealType(arg.getType)
+              val freshid = FreshIdentifier("t", rootType)
+              Let(freshid, arg, FunctionInvocation(TypedFunDef(fd, Seq(rootType)), Seq(freshid.toVariable)))
+
             case FunctionInvocation(TypedFunDef(fd, targs), args) if fdmap.contains(fd) =>
               FunctionInvocation(TypedFunDef(fdmap(fd), targs), args)
             case e => e
 
           }(fd.fullBody) // TODO: specs should not create lazy closures. enforce this
+          //println(s"New body of $fd: $nbody")
           fdmap(fd).fullBody = nbody
         case _ => ;
       }
     }
+    val repProg = copyProgram(prog, (defs: Seq[Definition]) => defs.map {
+      case fd: FunDef => fdmap.getOrElse(fd, fd)
+      case d          => d
+    })
     val nprog =
       if (!newfuns.isEmpty) {
-        val repProg = copyProgram(prog, (defs: Seq[Definition]) => defs.map {
-          case fd: FunDef => fdmap.getOrElse(fd, fd)
-          case d          => d
-        })
         val modToNewDefs = newfuns.values.groupBy(_._2).map { case (k, v) => (k, v.map(_._1)) }.toMap
         appendDefsToModules(repProg, modToNewDefs)
       } else
-        prog
+        repProg
     if (debugLifting)
       println("After lifiting arguments of lazy constructors: \n" + ScalaPrinter.apply(nprog))
     nprog
   }
 
-  import leon.solvers._
-  import leon.solvers.z3._
+  def removeInstrumentationSpecs(p: Program): Program = {
+    def hasInstVar(e: Expr) = {
+      exists { e => InstUtil.InstTypes.exists(i => i.isInstVariable(e)) }(e)
+    }
+    val newPosts = p.definedFunctions.collect {
+      case fd if fd.postcondition.exists { exists(hasInstVar) } =>
+        // remove the conjuncts that use instrumentation vars
+        val Lambda(resdef, pbody) = fd.postcondition.get
+        val npost = pbody match {
+          case And(args) =>
+            PredicateUtil.createAnd(args.filterNot(hasInstVar))
+          case e => Util.tru
+        }
+        (fd -> Lambda(resdef, npost))
+    }.toMap
+    ProgramUtil.updatePost(newPosts, p) //note: this will not update libraries
+  }
 
   def checkSpecifications(prog: Program) {
     // convert 'axiom annotation to library
@@ -155,37 +207,66 @@ object LazinessEliminationPhase extends TransformationPhase {
       if (fd.annotations.contains("axiom"))
         fd.addFlag(Annotation("library", Seq()))
     }
-    val functions = Seq() // Seq("--functions=rotate-time")
+    val functions = Seq() //Seq("--functions=rotate")
     val solverOptions = if (debugSolvers) Seq("--debug=solver") else Seq()
-    val ctx = Main.processOptions(Seq("--solvers=smt-cvc4,smt-z3") ++ solverOptions ++ functions)
+    val ctx = Main.processOptions(Seq("--solvers=smt-cvc4,smt-z3", "--assumepre") ++ solverOptions ++ functions)
     val report = VerificationPhase.apply(ctx, prog)
     println(report.summaryString)
-    /*val timeout = 10
-    val rep = ctx.reporter
-     * val fun = prog.definedFunctions.find(_.id.name == "firstUnevaluated").get
-    // create a verification context.
-    val solver = new FairZ3Solver(ctx, prog) with TimeoutSolver
-    val solverF = new TimeoutSolverFactory(SolverFactory(() => solver), timeout * 1000)
-    val vctx = VerificationContext(ctx, prog, solverF, rep)
-    val vc = (new DefaultTactic(vctx)).generatePostconditions(fun)(0)
-    val s = solverF.getNewSolver()
+  }
+
+  def checkInstrumentationSpecs(p: Program) = {
+    p.definedFunctions.foreach { fd =>
+      if (fd.annotations.contains("axiom"))
+        fd.addFlag(Annotation("library", Seq()))
+    }
+    val solverOptions = if (debugSolvers) Seq("--debug=solver") else Seq()
+    val ctx = Main.processOptions(Seq("--solvers=smt-cvc4,smt-z3", "--assumepre") ++ solverOptions)
+
+    //(a) create vcs
+    // Note: we only need to check specs involving instvars since others were checked before.
+    // Moreover, we can add other specs as assumptions since (A => B) ^ ((A ^ B) => C) => A => B ^ C
+    //checks if the expression uses res._2 which corresponds to instvars after instrumentation
+    def accessesSecondRes(e: Expr, resid: Identifier): Boolean =
+        exists(_ == TupleSelect(resid.toVariable, 2))(e)
+
+    val vcs = p.definedFunctions.collect {
+      // skipping verification of uninterpreted functions
+      case fd if !fd.isLibrary && fd.hasBody && fd.postcondition.exists{post =>
+        val Lambda(Seq(resdef), pbody) =  post
+        accessesSecondRes(pbody, resdef.id)
+      } =>
+        val Lambda(Seq(resdef), pbody) = fd.postcondition.get
+        val (instPost, assumptions) = pbody match {
+          case And(args) =>
+            val (instSpecs, rest) = args.partition(accessesSecondRes(_, resdef.id))
+            (createAnd(instSpecs), createAnd(rest))
+          case e => (e, Util.tru)
+        }
+        val vc = implies(createAnd(Seq(fd.precOrTrue, assumptions)),
+            application(Lambda(Seq(resdef), instPost), Seq(fd.body.get)))
+        if(debugInstVCs)
+          println(s"VC for function ${fd.id} : "+vc)
+        VC(vc, fd, VCKinds.Postcondition)
+    }
+    //(b) create a verification context
+    val timeout: Option[Long] = None
+    val reporter = ctx.reporter
+    // Solvers selection and validation
+    val baseSolverF = SolverFactory.getFromSettings(ctx, p)
+    val solverF = timeout match {
+      case Some(sec) =>
+        baseSolverF.withTimeout(sec / 1000)
+      case None =>
+        baseSolverF
+    }
+    val vctx = VerificationContext(ctx, p, solverF, reporter)
+    //(c) check the vcs
     try {
-      rep.info(s" - Now considering '${vc.kind}' VC for ${vc.fd.id} @${vc.getPos}...")
-      val tStart = System.currentTimeMillis
-      s.assertVC(vc)
-      val satResult = s.check
-      val dt = System.currentTimeMillis - tStart
-      val res = satResult match {
-        case None =>
-          rep.info("Cannot prove or disprove specifications")
-        case Some(false) =>
-          rep.info("Valid")
-        case Some(true) =>
-          println("Invalid - counter-example: " + s.getModel)
-      }
+      val veriRep = VerificationPhase.checkVCs(vctx, vcs)
+      println("Resource Verification Results: \n" + veriRep.summaryString)
     } finally {
-      s.free()
-    }*/
+      solverF.shutdown()
+    }
   }
 
   /**
@@ -259,7 +340,7 @@ object LazinessEliminationPhase extends TransformationPhase {
   }*/
   // Expressions for testing solvers
   // a test expression
-    /*val tparam =
+  /*val tparam =
     val dummyFunDef = new FunDef(FreshIdentifier("i"),Seq(), Seq(), IntegerType)
     val eq = Equals(FunctionInvocation(TypedFunDef(dummyFunDef, Seq()), Seq()), InfiniteIntegerLiteral(0))
     import solvers._
diff --git a/src/main/scala/leon/laziness/LazinessUtil.scala b/src/main/scala/leon/laziness/LazinessUtil.scala
index e30671b1263b97d88ff5d0ea62e4696fd594464d..a2c2338ca2ba00e84e234f3ebb933753f29e64b1 100644
--- a/src/main/scala/leon/laziness/LazinessUtil.scala
+++ b/src/main/scala/leon/laziness/LazinessUtil.scala
@@ -39,7 +39,8 @@ object LazinessUtil {
     try {
       new File(outputFolder).mkdir()
     } catch {
-      case _: java.io.IOException => ctx.reporter.fatalError("Could not create directory " + outputFolder)
+      case _: java.io.IOException =>
+        ctx.reporter.fatalError("Could not create directory " + outputFolder)
     }
 
     for (u <- p.units if u.isMainUnit) {
@@ -65,6 +66,13 @@ object LazinessUtil {
       false
   }
 
+  def isEagerInvocation(e: Expr)(implicit p: Program): Boolean = e match {
+    case FunctionInvocation(TypedFunDef(fd, _), Seq(_)) =>
+      fullName(fd)(p) == "leon.lazyeval.$.eager"
+    case _ =>
+      false
+  }
+
   def isEvaluatedInvocation(e: Expr)(implicit p: Program): Boolean = e match {
     case FunctionInvocation(TypedFunDef(fd, _), Seq(_)) =>
       fullName(fd)(p) == "leon.lazyeval.$.isEvaluated"
@@ -146,7 +154,7 @@ object LazinessUtil {
    * and those that return a new state.
    * TODO: implement backwards BFS by reversing the graph
    */
-  def funsNeedingnReturningState(prog: Program) = {
+  /*def funsNeedingnReturningState(prog: Program) = {
     val cg = CallGraphUtil.constructCallGraph(prog, false, true)
     var needRoots = Set[FunDef]()
     var retRoots = Set[FunDef]()
@@ -171,7 +179,7 @@ object LazinessUtil {
     val funsRetStates = prog.definedFunctions.filterNot(fd =>
       cg.transitiveCallees(fd).toSet.intersect(retRoots).isEmpty).toSet
     (funsNeedStates, funsRetStates)
-  }
+  }*/
 
   def freshenTypeArguments(tpe: TypeTree): TypeTree = {
     tpe match {
diff --git a/src/main/scala/leon/laziness/LazyClosureConverter.scala b/src/main/scala/leon/laziness/LazyClosureConverter.scala
index 868d4bfeb390ec2b3085629ef78075ba463e086d..f4c81eb3d81c9a8d34f2ed27556ab42ec5fcaa23 100644
--- a/src/main/scala/leon/laziness/LazyClosureConverter.scala
+++ b/src/main/scala/leon/laziness/LazyClosureConverter.scala
@@ -26,6 +26,7 @@ import leon.Main
 import leon.TransformationPhase
 import LazinessUtil._
 import invariant.util.ProgramUtil._
+import purescala.TypeOps._
 
 /**
  * (a) add state to every function in the program
@@ -34,12 +35,15 @@ import invariant.util.ProgramUtil._
  * (d) replace isEvaluated with currentState.contains()
  * (e) replace accesses to $.value with calls to dispatch with current state
  */
-class LazyClosureConverter(p: Program, closureFactory: LazyClosureFactory) {
+class LazyClosureConverter(p: Program, ctx: LeonContext, closureFactory: LazyClosureFactory) {
   val debug = false
   // flags
   val removeRecursionViaEval = false
+  val useRefEquality = ctx.findOption(LazinessEliminationPhase.optRefEquality).getOrElse(false)
 
-  val (funsNeedStates, funsRetStates) = funsNeedingnReturningState(p)
+  val funsManager = new LazyFunctionsManager(p)
+  val funsNeedStates = funsManager.funsNeedStates
+  val funsRetStates = funsManager.funsRetStates
   val tnames = closureFactory.lazyTypeNames
 
   // create a mapping from functions to new functions
@@ -83,8 +87,8 @@ class LazyClosureConverter(p: Program, closureFactory: LazyClosureFactory) {
    * A set of uninterpreted functions that may be used as targets
    * of closures in the eval functions, for efficiency reasons.
    */
-  lazy val uninterpretedTargets = funMap.map {
-    case (k, v) =>
+  lazy val uninterpretedTargets = funMap.collect {
+    case (k, v) if closureFactory.isLazyOp(k) =>
       val ufd = new FunDef(FreshIdentifier(v.id.name, v.id.getType, true),
         v.tparams, v.params, v.returnType)
       (k -> ufd)
@@ -142,7 +146,7 @@ class LazyClosureConverter(p: Program, closureFactory: LazyClosureFactory) {
    * the call-sites.
    */
   val evalFunctions = tnames.map { tname =>
-    val tpe = /*freshenTypeArguments(*/closureFactory.lazyType(tname)//)
+    val tpe = /*freshenTypeArguments(*/ closureFactory.lazyType(tname) //)
     val absdef = closureFactory.absClosureType(tname)
     val cdefs = closureFactory.closures(tname)
 
@@ -177,13 +181,12 @@ class LazyClosureConverter(p: Program, closureFactory: LazyClosureFactory) {
 
       //(a) construct the value component
       val stArgs =
-        if (funsNeedStates(op)){
+        if (funsNeedStates(op)) {
           // Note: it is important to use uninterpreted state here for 2 reasons:
           // (a) to eliminate dependency on state for the result value
           // (b) to avoid inconsistencies when using a fixed state such as empty state
           Seq(getUninterpretedState(tname, tparams))
-        }
-        else Seq()
+        } else Seq()
       //println(s"invoking function $targetFun with args $args")
       val invoke = FunctionInvocation(TypedFunDef(targetFun, tparams), args ++ stArgs) // we assume that the type parameters of lazy ops are same as absdefs
       val invPart = if (funsRetStates(op)) {
@@ -193,14 +196,24 @@ class LazyClosureConverter(p: Program, closureFactory: LazyClosureFactory) {
       //(b) construct the state component
       val stPart = if (funsRetStates(op)) {
         val stInvoke = FunctionInvocation(TypedFunDef(targetFun, tparams),
-           args ++ (if (funsNeedStates(op)) Seq(param2.toVariable) else Seq()))
+          args ++ (if (funsNeedStates(op)) Seq(param2.toVariable) else Seq()))
         TupleSelect(stInvoke, 2)
       } else param2.toVariable
       val newst = SetUnion(stPart, FiniteSet(Set(binder.toVariable), stType.base))
       val rhs = Tuple(Seq(invPart, newst))
       MatchCase(pattern, None, rhs)
     }
-    dfun.body = Some(MatchExpr(param1.toVariable, bodyMatchCases))
+    // create a new match case for eager evaluation
+    val eagerCase = {
+      val eagerDef = closureFactory.eagerClosure(tname)
+      val ctype = CaseClassType(eagerDef, tparams)
+      val binder = FreshIdentifier("t", ctype)
+      // create a body of the match
+      val valPart = CaseClassSelector(ctype, binder.toVariable, eagerDef.fields(0).id)
+      val rhs = Tuple(Seq(valPart, param2.toVariable)) // state doesn't change for eager closure
+      MatchCase(InstanceOfPattern(Some(binder), ctype), None, rhs)
+    }
+    dfun.body = Some(MatchExpr(param1.toVariable, eagerCase +: bodyMatchCases))
     dfun.addFlag(Annotation("axiom", Seq()))
     (tname -> dfun)
   }.toMap
@@ -212,7 +225,7 @@ class LazyClosureConverter(p: Program, closureFactory: LazyClosureFactory) {
    */
   val computeFunctions = evalFunctions.map {
     case (tname, evalfd) =>
-      val tpe = /*freshenTypeArguments(*/closureFactory.lazyType(tname)//)
+      val tpe = /*freshenTypeArguments(*/ closureFactory.lazyType(tname) //)
       val param1 = evalfd.params.head
       val fun = new FunDef(FreshIdentifier(evalfd.id.name + "*", Untyped),
         evalfd.tparams, Seq(param1), tpe)
@@ -228,7 +241,7 @@ class LazyClosureConverter(p: Program, closureFactory: LazyClosureFactory) {
    * They are defined for each lazy class since it avoids generics and
    * simplifies the type inference (which is not full-fledged in Leon)
    */
-  val closureCons = tnames.map { tname =>
+  lazy val closureCons = tnames.map { tname =>
     val adt = closureFactory.absClosureType(tname)
     val param1Type = AbstractClassType(adt, adt.tparams.map(_.tp))
     val param1 = FreshIdentifier("cc", param1Type)
@@ -238,11 +251,15 @@ class LazyClosureConverter(p: Program, closureFactory: LazyClosureFactory) {
     val fun = new FunDef(FreshIdentifier(closureConsName(tname)), adt.tparams,
       Seq(ValDef(param1), ValDef(param2)), param1Type)
     fun.body = Some(param1.toVariable)
-    val resid = FreshIdentifier("res", param1Type)
-    val postbody = Not(ElementOfSet(resid.toVariable, param2.toVariable))
-        /*SubsetOf(FiniteSet(Set(resid.toVariable), param1Type), param2.toVariable)*/
-    fun.postcondition = Some(Lambda(Seq(ValDef(resid)), postbody))
-    fun.addFlag(Annotation("axiom", Seq()))
+
+    // assert that the closure in unevaluated if useRefEquality is enabled
+    if (useRefEquality) {
+      val resid = FreshIdentifier("res", param1Type)
+      val postbody = Not(ElementOfSet(resid.toVariable, param2.toVariable))
+      /*SubsetOf(FiniteSet(Set(resid.toVariable), param1Type), param2.toVariable)*/
+      fun.postcondition = Some(Lambda(Seq(ValDef(resid)), postbody))
+      fun.addFlag(Annotation("axiom", Seq()))
+    }
     (tname -> fun)
   }.toMap
 
@@ -259,14 +276,25 @@ class LazyClosureConverter(p: Program, closureFactory: LazyClosureFactory) {
       }, false)
       mapNAryOperator(args, op)
 
+    case finv @ FunctionInvocation(_, Seq(arg)) if isEagerInvocation(finv)(p) =>
+      // here arg is guaranteed to be a variable
+      ((st: Map[String, Expr]) => {
+        val rootType = bestRealType(arg.getType)
+        val tname = typeNameWOParams(rootType)
+        val tparams = getTypeArguments(rootType)
+        val eagerClosure = closureFactory.eagerClosure(tname)
+        CaseClass(CaseClassType(eagerClosure, tparams), Seq(arg))
+      }, false)
+
     case finv @ FunctionInvocation(_, args) if isEvaluatedInvocation(finv)(p) => // isEval function ?
       val op = (nargs: Seq[Expr]) => ((st: Map[String, Expr]) => {
         val narg = nargs(0) // there must be only one argument here
         val baseType = unwrapLazyType(narg.getType).get
         val tname = typeNameWOParams(baseType)
-        //val adtType = AbstractClassType(closureFactory.absClosureType(tname), getTypeParameters(baseType))
-        //SubsetOf(FiniteSet(Set(narg), adtType), st(tname))
-        ElementOfSet(narg, st(tname))
+        val memberTest = ElementOfSet(narg, st(tname)) // should we use subtype instead ?
+        val subtypeTest = IsInstanceOf(narg,
+          CaseClassType(closureFactory.eagerClosure(tname), getTypeArguments(baseType)))
+        Or(memberTest, subtypeTest)
       }, false)
       mapNAryOperator(args, op)
 
@@ -440,7 +468,7 @@ class LazyClosureConverter(p: Program, closureFactory: LazyClosureFactory) {
 
   def assignBodiesToFunctions = funMap foreach {
     case (fd, nfd) =>
-//      /println("Considering function: "+fd)
+      //      /println("Considering function: "+fd)
       // Here, using name to identify 'state' parameters, also relying
       // on fact that nfd.params are in the same order as tnames
       val stateParams = nfd.params.foldLeft(Seq[Expr]()) {
@@ -471,7 +499,7 @@ class LazyClosureConverter(p: Program, closureFactory: LazyClosureFactory) {
           else Some(npreFun(initStateMap))
       }
 
-      if (fd.hasPostcondition) {
+      val simpPost = if (fd.hasPostcondition) {
         val Lambda(arg @ Seq(ValDef(resid, _)), post) = fd.postcondition.get
         val (npostFun, postUpdatesState) = mapBody(post)
         val newres = FreshIdentifier(resid.name, bodyWithState.getType)
@@ -486,12 +514,51 @@ class LazyClosureConverter(p: Program, closureFactory: LazyClosureFactory) {
         val npost =
           if (postUpdatesState) {
             TupleSelect(npost1, 1) // ignore state updated by post
+          } else npost1
+        Some(Lambda(Seq(ValDef(newres)), npost))
+      } else None
+      // add invariants on state
+      val fpost =
+        if (funsRetStates(fd)) { // add specs on states
+          val instates = stateParams
+          val resid = if (fd.hasPostcondition) {
+            val Lambda(Seq(ValDef(r, _)), _) = simpPost.get
+            r
+          } else FreshIdentifier("r", nfd.returnType)
+          val outstates = (0 until tnames.size).map(i => TupleSelect(resid.toVariable, i + 2))
+          val invstate = fd.annotations.contains("invstate")
+          val statePred = PredicateUtil.createAnd((instates zip outstates).map {
+            case (x, y) =>
+              if (invstate)
+                Equals(x, y)
+              else SubsetOf(x, y)
+          })
+          val post = Lambda(Seq(ValDef(resid)), (if (fd.hasPostcondition) {
+            val Lambda(Seq(ValDef(_, _)), p) = simpPost.get
+            And(p, statePred)
+          } else statePred))
+          Some(post)
+        } else simpPost
+      if (fpost.isDefined) {
+        nfd.postcondition = fpost
+        // also attach postcondition to uninterpreted targets
+        if (removeRecursionViaEval) {
+          uninterpretedTargets.get(fd) match {
+            case Some(uitarget) =>
+              /*val nfdRes = fpost.get.args(0).id
+              val repmap: Map[Expr, Expr] = ((nfdRes.toVariable, FreshIdentifier(nfdRes.name).toVariable) +:
+                (nfd.params.map(_.id.toVariable) zip uitarget.params.map(_.id.toVariable))).toMap*/
+              // uitarget uses the same identifiers as nfd
+              uitarget.postcondition = fpost
+            case None => ;
           }
-          else npost1
-        nfd.postcondition = Some(Lambda(Seq(ValDef(newres)), npost))
+        }
       }
   }
 
+  /**
+   * This method is not used for now,
+   */
   def assignContractsForEvals = evalFunctions.foreach {
     case (tname, evalfd) =>
       val cdefs = closureFactory.closures(tname)
@@ -523,9 +590,11 @@ class LazyClosureConverter(p: Program, closureFactory: LazyClosureFactory) {
           Util.tru
         MatchCase(pattern, None, rhs)
       }
+      // create a default case to match eagerClosures
+      val default = MatchCase(WildcardPattern(None), None, Util.tru)
       evalfd.postcondition = Some(
         Lambda(Seq(ValDef(postres)),
-          MatchExpr(evalfd.params.head.toVariable, postMatchCases)))
+          MatchExpr(evalfd.params.head.toVariable, postMatchCases :+ default)))
   }
 
   /**
@@ -554,14 +623,18 @@ class LazyClosureConverter(p: Program, closureFactory: LazyClosureFactory) {
     val anchor = funMap.values.last
     transformCaseClasses
     assignBodiesToFunctions
-    assignContractsForEvals
+    //assignContractsForEvals
     addDefs(
       copyProgram(p,
         (defs: Seq[Definition]) => defs.flatMap {
           case fd: FunDef if funMap.contains(fd) =>
-            if (removeRecursionViaEval)
-              Seq(funMap(fd), uninterpretedTargets(fd))
-            else Seq(funMap(fd))
+            if (removeRecursionViaEval) {
+              uninterpretedTargets.get(fd) match {
+                case Some(uitarget) =>
+                  Seq(funMap(fd), uitarget)
+                case _ => Seq(funMap(fd))
+              }
+            } else Seq(funMap(fd))
           case d => Seq(d)
         }),
       closureFactory.allClosuresAndParents ++ closureCons.values ++
diff --git a/src/main/scala/leon/laziness/LazyClosureFactory.scala b/src/main/scala/leon/laziness/LazyClosureFactory.scala
index 5d0302ae670419ee29ae8b1f048a2a4a317bc7b5..1f156b539ac20008a37b5849c7eeddf1fd47b1c0 100644
--- a/src/main/scala/leon/laziness/LazyClosureFactory.scala
+++ b/src/main/scala/leon/laziness/LazyClosureFactory.scala
@@ -13,6 +13,7 @@ import purescala.ExprOps._
 import purescala.DefOps._
 import purescala.Extractors._
 import purescala.Types._
+import purescala.TypeOps._
 import leon.invariant.util.TypeUtil._
 import leon.invariant.util.LetTupleSimplification._
 import java.io.File
@@ -71,11 +72,12 @@ class LazyClosureFactory(p: Program) {
     var opToAdt = Map[FunDef, CaseClassDef]()
     val tpeToADT = tpeToLazyops map {
       case (tpename, ops) =>
+        val baseT = ops(0).returnType //TODO: replace targs here ?
         val absClass = tpeToAbsClass(tpename)
-        val absTParams = absClass.tparams
+        val absTParamsDef = absClass.tparams
         // create a case class for every operation
         val cdefs = ops map { opfd =>
-          assert(opfd.tparams.size == absTParams.size)
+          assert(opfd.tparams.size == absTParamsDef.size)
           val absType = AbstractClassType(absClass, opfd.tparams.map(_.tp))
           val classid = FreshIdentifier(opNameToCCName(opfd.id.name), Untyped)
           val cdef = CaseClassDef(classid, opfd.tparams, Some(absType), isCaseObject = false)
@@ -94,7 +96,17 @@ class LazyClosureFactory(p: Program) {
           opToAdt += (opfd -> cdef)
           cdef
         }
-        (tpename -> (ops(0).returnType, absClass, cdefs))
+        // create a case class to represent eager evaluation
+        val absTParams = absTParamsDef.map(_.tp)
+        val fldType = ops(0).returnType match {
+          case NAryType(tparams, tcons) => tcons(absTParams)
+        }
+        val eagerid = FreshIdentifier("Eager"+TypeUtil.typeNameWOParams(fldType))
+        val eagerClosure = CaseClassDef(eagerid, absTParamsDef,
+            Some(AbstractClassType(absClass, absTParams)), isCaseObject = false)
+        eagerClosure.setFields(Seq(ValDef(FreshIdentifier("a", fldType))))
+        absClass.registerChild(eagerClosure)
+        (tpename -> (baseT, absClass, cdefs, eagerClosure))
     }
     /*tpeToADT.foreach {
       case (k, v) => println(s"$k --> ${ (v._2 +: v._3).mkString("\n\t") }")
@@ -105,7 +117,7 @@ class LazyClosureFactory(p: Program) {
   // this fixes an ordering on lazy types
   lazy val lazyTypeNames = tpeToADT.keys.toSeq
 
-  def allClosuresAndParents = tpeToADT.values.flatMap(v => v._2 +: v._3)
+  def allClosuresAndParents = tpeToADT.values.flatMap(v => v._2 +: v._3 :+ v._4)
 
   def lazyType(tn: String) = tpeToADT(tn)._1
 
@@ -113,12 +125,15 @@ class LazyClosureFactory(p: Program) {
 
   def closures(tn: String) = tpeToADT(tn)._3
 
+  def eagerClosure(tn: String) = tpeToADT(tn)._4
+
   lazy val caseClassToOp = opToCaseClass map { case (k, v) => v -> k }
 
   def lazyopOfClosure(cl: CaseClassDef) = caseClassToOp(cl)
 
   def closureOfLazyOp(op: FunDef) = opToCaseClass(op)
 
+  def isLazyOp(op: FunDef) = opToCaseClass.contains(op)
   /**
    * Here, the lazy type name is recovered from the closure's name.
    * This avoids the use of additional maps.
diff --git a/src/main/scala/leon/laziness/LazyInstrumenter.scala b/src/main/scala/leon/laziness/LazyInstrumenter.scala
index 1f239b4012368ae41ace8bd038c25306a62ccfdf..f72b85b88a88e20f507f89a61ddcd05bb7ab02af 100644
--- a/src/main/scala/leon/laziness/LazyInstrumenter.scala
+++ b/src/main/scala/leon/laziness/LazyInstrumenter.scala
@@ -28,11 +28,17 @@ import LazinessUtil._
 
 class LazyInstrumenter(p: Program) {
 
-  def apply: Program = {
-    val exprInstFactory = (x: Map[FunDef, FunDef], y: SerialInstrumenter, z: FunDef) =>
+  val exprInstFactory = (x: Map[FunDef, FunDef], y: SerialInstrumenter, z: FunDef) =>
       new LazyExprInstrumenter(x, y)(z)
-    (new SerialInstrumenter(p, Some(exprInstFactory))).apply
-  }
+  val serialInst = new SerialInstrumenter(p, Some(exprInstFactory))
+
+  /*def funsWithInstSpecs  = {
+    serialInst.instToInstrumenter.values.flatMap{inst =>
+      inst.getRootFuncs(p)
+    }.toList.distinct
+  }*/
+
+  def apply: Program = serialInst.apply
 
   class LazyExprInstrumenter(funMap: Map[FunDef, FunDef], serialInst: SerialInstrumenter)(implicit currFun: FunDef)
       extends ExprInstrumenter(funMap, serialInst)(currFun) {
@@ -44,18 +50,35 @@ class LazyInstrumenter(p: Program) {
       if (isEvalFunction(currFun)) {
         val closureParam = currFun.params(0).id.toVariable
         val stateParam = currFun.params(1).id.toVariable
-        val nbody = super.apply(e)
+        // we need to specialize instrumentation of body
+        val nbody = e match {
+          case MatchExpr(scr, mcases) =>
+            val ncases = mcases map {
+              case MatchCase(pat, guard, Tuple(Seq(valpart, statepart))) =>
+                // instrument the state part (and ignore the val part)
+                // (Note: this is an hack to ensure that we always consider only one call to targets)
+                val transState = transform(statepart)(Map())
+                val transVal = transform(valpart)(Map())
+
+                val caseId = FreshIdentifier("cd", transState.getType, true)
+                val casePart = Tuple(Seq(TupleSelect(transVal, 1), TupleSelect(caseId.toVariable, 1)))
+                val instPart = instrumenters map { m => selectInst(caseId.toVariable, m.inst) }
+                val lete = Let(caseId, transState, Tuple(casePart +: instPart))
+                MatchCase(pat, guard, lete)
+            }
+            MatchExpr(scr, ncases)
+        }
+        //val nbody = super.apply(e)
         val bodyId = FreshIdentifier("bd", nbody.getType, true)
         val instExprs = instrumenters map { m =>
           IfExpr(ElementOfSet(closureParam, stateParam),
-              //SubsetOf(FiniteSet(Set(closureParam), closureParam.getType), stateParam),
             InfiniteIntegerLiteral(costOfMemoization(m.inst)),
             selectInst(bodyId.toVariable, m.inst))
         }
         Let(bodyId, nbody,
           Tuple(TupleSelect(bodyId.toVariable, 1) +: instExprs))
-
-      } else super.apply(e)
+      } else
+        super.apply(e)
     }
   }
 }
diff --git a/src/main/scala/leon/laziness/TypeChecker.scala b/src/main/scala/leon/laziness/TypeChecker.scala
index 96f9967f1b128447848f8e2411e6845bae95b321..6bb093b738763eb1d1da7bcbd581355e1afd2f7e 100644
--- a/src/main/scala/leon/laziness/TypeChecker.scala
+++ b/src/main/scala/leon/laziness/TypeChecker.scala
@@ -43,9 +43,15 @@ object TypeChecker {
           (btype, Let(nid, nval, nbody))
 
         case Ensuring(body, Lambda(Seq(resdef @ ValDef(resid, _)), postBody)) =>
-          val (btype, nbody) = rec(body)
-          val nres = makeIdOfType(resid, btype)
-          (btype, Ensuring(nbody, Lambda(Seq(ValDef(nres)), rec(postBody)._2)))
+          body match {
+            case NoTree(tpe) =>
+              val nres = makeIdOfType(resid, tpe)
+              (tpe, Ensuring(body, Lambda(Seq(ValDef(nres)), rec(postBody)._2)))
+            case _ =>
+              val (btype, nbody) = rec(body)
+              val nres = makeIdOfType(resid, btype)
+              (btype, Ensuring(nbody, Lambda(Seq(ValDef(nres)), rec(postBody)._2)))
+          }
 
         case MatchExpr(scr, mcases) =>
           val (scrtype, nscr) = rec(scr)
diff --git a/src/main/scala/leon/laziness/TypeRectifier.scala b/src/main/scala/leon/laziness/TypeRectifier.scala
index b95cb815b10051e6b93ed703341c174e5a81c60e..89583bbb0b990d14463f8c888180cd70b59ebf34 100644
--- a/src/main/scala/leon/laziness/TypeRectifier.scala
+++ b/src/main/scala/leon/laziness/TypeRectifier.scala
@@ -126,11 +126,13 @@ class TypeRectifier(p: Program, placeHolderParameter: TypeParameter => Boolean)
       case Variable(id) if paramMap.contains(id) =>
         paramMap(id).toVariable
       case TupleSelect(tup, index) => TupleSelect(rec(tup), index)
+      case Ensuring(NoTree(_), post) =>
+        Ensuring(nfd.fullBody, rec(post)) // the newfd body would already be type correct
       case Operator(args, op)      => op(args map rec)
       case t: Terminal             => t
     }
     val nbody = rec(ifd.fullBody)
-    //println("Inferring types for: "+ifd.id)
+    //println(s"Inferring types for ${ifd.id} new fun: $nfd new body: $nbody")
     val initGamma = nfd.params.map(vd => vd.id -> vd.getType).toMap
     TypeChecker.inferTypesOfLocals(nbody, initGamma)
   }
diff --git a/testcases/lazy-datastructures/BottomUpMegeSort.scala b/testcases/lazy-datastructures/BottomUpMegeSort.scala
index 84e8ebcd45bf4682634035ec4953bf234b5bdae1..23ae5e1e3c507fb22a0d908c1f8458f7638ad4ef 100644
--- a/testcases/lazy-datastructures/BottomUpMegeSort.scala
+++ b/testcases/lazy-datastructures/BottomUpMegeSort.scala
@@ -1,6 +1,7 @@
 package lazybenchmarks
 
 import leon.lazyeval._
+import leon.lazyeval.$._
 import leon.lang._
 import leon.annotation._
 import leon.instrumentation._
@@ -113,12 +114,12 @@ object BottomUpMergeSort {
     l match {
       case INil() => SNil()
       case ICons(x, xs) =>
-        SCons($(LCons(x, $(LNil()))), IListToLList(xs))
+        SCons(LCons(x, LNil()), IListToLList(xs))
     }
   } ensuring (res => res.fullSize == l.size &&
     res.size == l.size &&
     res.valid &&
-    time <= 9 * l.size + 3)
+    time <= 11 * l.size + 3)
 
   def mergeSort(l: IList): ILList = {
     l match {
diff --git a/testcases/lazy-datastructures/RealTimeQueue.scala b/testcases/lazy-datastructures/RealTimeQueue.scala
index 879fc40c0b8ed8445c898da0bcec7f59beb0e3c3..64fcd5aa15b996a9b7e3cc0adfd31e6286aafc87 100644
--- a/testcases/lazy-datastructures/RealTimeQueue.scala
+++ b/testcases/lazy-datastructures/RealTimeQueue.scala
@@ -1,9 +1,11 @@
 import leon.lazyeval._
+import leon.lazyeval.$._
 import leon.lang._
 import leon.annotation._
 import leon.collection._
 import leon.instrumentation._
 
+//TODO: need to automatically check monotonicity of isConcrete
 object RealTimeQueue {
 
   sealed abstract class LList[T] {
@@ -33,6 +35,7 @@ object RealTimeQueue {
 
   def ssize[T](l: $[LList[T]]): BigInt = (l*).size
 
+  //@monotonic
   def isConcrete[T](l: $[LList[T]]): Boolean = {
     (l.isEvaluated && (l* match {
       case SCons(_, tail) =>
@@ -41,16 +44,19 @@ object RealTimeQueue {
     })) || (l*).isEmpty
   }
 
-  // an axiom about lazy streams (this should be a provable axiom, but not as of now)
-  @axiom
-  def streamLemma[T](l: $[LList[T]]) = {
-    l.isEvaluated ||
-      (l* match {
-        case SCons(_, tail) =>
-          l != tail && !tail.isEvaluated
-        case _ => true
-      })
-  } holds
+   @invstate
+  def rotate[T](f: $[LList[T]], r: List[T], a: $[LList[T]]): LList[T] = {
+    require(r.size == ssize(f) + 1 && isConcrete(f)) // size invariant between 'f' and 'r' holds
+    (f.value, r) match {
+      case (SNil(), Cons(y, _)) => //in this case 'y' is the only element in 'r'
+        SCons[T](y, a)
+      case (SCons(x, tail), Cons(y, r1)) =>
+        val newa: LList[T] = SCons[T](y, a)
+        val rot = $(rotate(tail, r1, newa)) //this creates a lazy rotate operation
+        SCons[T](x, rot)
+    }
+  } ensuring (res => res.size == (f*).size + r.size + (a*).size && res.isCons && // using f*.size instead of ssize seems to help magically
+                     time <= 30)
 
   def firstUnevaluated[T](l: $[LList[T]]): $[LList[T]] = {
     if (l.isEvaluated) {
@@ -63,15 +69,14 @@ object RealTimeQueue {
       l
   } ensuring (res => (!(res*).isEmpty || isConcrete(l)) && //if there are no lazy closures then the stream is concrete
     ((res*).isEmpty || !res.isEvaluated) && // if the return value is not a Nil closure then it would not have been evaluated
-    streamLemma(res) &&
     (res.value match {
       case SCons(_, tail) =>
-        firstUnevaluated(l) == tail // after evaluating the firstUnevaluated closure in 'l' we get the next unevaluated closure
+        firstUnevaluated(l) == firstUnevaluated(tail) // after evaluating the firstUnevaluated closure in 'l' we can access the next unevaluated closure
       case _ => true
     }))
 
   def streamScheduleProperty[T](s: $[LList[T]], sch: $[LList[T]]) = {
-    firstUnevaluated(s) == sch
+    firstUnevaluated(s) == firstUnevaluated(sch)
   }
 
   case class Queue[T](f: $[LList[T]], r: List[T], s: $[LList[T]]) {
@@ -82,21 +87,6 @@ object RealTimeQueue {
     }
   }
 
-  @invstate
-  def rotate[T](f: $[LList[T]], r: List[T], a: $[LList[T]]): LList[T] = {
-    require(r.size == ssize(f) + 1 && isConcrete(f)) // size invariant between 'f' and 'r' holds
-    (f.value, r) match {
-      case (SNil(), Cons(y, _)) => //in this case 'y' is the only element in 'r'
-        SCons[T](y, a)
-      case (SCons(x, tail), Cons(y, r1)) =>
-        val newa: LList[T] = SCons[T](y, a)
-        val rot = $(rotate(tail, r1, $(newa))) //this creates a lazy rotate operation
-        SCons[T](x, rot)
-    }
-  } ensuring (res => res.size == ssize(f) + r.size + ssize(a) && res.isCons &&
-                     time <= 30)
-
-  // TODO: make newa into sch to avoid a different closure category
   def createQueue[T](f: $[LList[T]], r: List[T], sch: $[LList[T]]): Queue[T] = {
     require(streamScheduleProperty(f, sch) &&
       ssize(sch) == ssize(f) - r.size + 1) //size invariant holds
@@ -105,7 +95,7 @@ object RealTimeQueue {
         Queue(f, r, tail)
       case SNil() =>
         val newa: LList[T] = SNil[T]()
-        val rotres = $(rotate(f, r, $(newa)))
+        val rotres = $(rotate(f, r, newa))
         Queue(rotres, Nil[T](), rotres)
     }
   } ensuring (res => res.valid && time <= 50)
@@ -124,9 +114,9 @@ object RealTimeQueue {
             Queue(nf, q.r, st)
           case _ =>
             val newa: LList[T] = SNil[T]()
-            val rotres = $(rotate(nf, q.r, $(newa)))
+            val rotres = $(rotate(nf, q.r, newa))
             Queue(rotres, Nil[T](), rotres)
         }
     }
-  } ensuring (res => time <= 120) //res.valid && )
+  } ensuring(res => res.valid && time <= 120)
 }