Supress warnings/ small fixes

src/main/scala/leon/invariant/engine/UnfoldingTemplateSolver.scala

@@ -183,11 +183,10 @@ class UnfoldingTemplateSolver(ctx: InferenceContext, program: Program, rootFd: F
    * Uses default postcondition VC, but can be overriden in the case of non-standard VCs
    */
   def verifyVC(newprog: Program, newroot: FunDef) = {
-    (newroot.postcondition, newroot.body) match {
-      case (Some(post), Some(body)) =>
-        val vc = implies(newroot.precOrTrue, application(post, Seq(body)))
-        solveUsingLeon(ctx.leonContext, newprog, VC(vc, newroot, VCKinds.Postcondition))
-    }
+    val post = newroot.postcondition.get
+    val body = newroot.body.get
+    val vc = implies(newroot.precOrTrue, application(post, Seq(body)))
+    solveUsingLeon(ctx.leonContext, newprog, VC(vc, newroot, VCKinds.Postcondition))
   }
 
   import leon.solvers._

src/main/scala/leon/invariant/structure/Formula.scala

@@ -3,26 +3,20 @@
 package leon
 package invariant.structure
 
-import z3.scala._
-import purescala._
 import purescala.Common._
 import purescala.Definitions._
 import purescala.Expressions._
 import purescala.ExprOps._
 import purescala.Extractors._
 import purescala.Types._
-import solvers.{ Solver, TimeoutSolver }
-import solvers.z3.FairZ3Solver
 import java.io._
-import solvers.z3._
 import invariant.engine._
 import invariant.util._
-import leon.solvers.Model
+import solvers.Model
 import Util._
 import PredicateUtil._
 import TVarFactory._
 import ExpressionTransformer._
-import evaluators._
 import invariant.factories._
 import evaluators._
 import EvaluationResults._
@@ -224,7 +218,7 @@ class Formula(val fd: FunDef, initexpr: Expr, ctx: InferenceContext, initSpecCal
    * 'neweexpr' is required to be in negation normal form and And/Ors have been pulled up
    */
   def conjoinWithDisjunct(guard: Variable, newexpr: Expr, callParents: List[FunDef], inSpec:Boolean) = {
-     val (exprRoot, newGaurds) = addConstraints(newexpr, callParents, _ => inSpec)
+     val (exprRoot, newGuards) = addConstraints(newexpr, callParents, _ => inSpec)
      //add 'newguard' in conjunction with 'disjuncts(guard)'
      val ctrs = disjuncts(guard)
      disjuncts -= guard
@@ -233,7 +227,7 @@ class Formula(val fd: FunDef, initexpr: Expr, ctx: InferenceContext, initSpecCal
   }
 
   def conjoinWithRoot(newexpr: Expr, callParents: List[FunDef], inSpec: Boolean) = {
-    val (exprRoot, newGaurds) = addConstraints(newexpr, callParents, _ => inSpec)
+    val (exprRoot, newGuards) = addConstraints(newexpr, callParents, _ => inSpec)
     roots :+= exprRoot
     exprRoot
   }
@@ -401,10 +395,10 @@ class Formula(val fd: FunDef, initexpr: Expr, ctx: InferenceContext, initSpecCal
    * Functions for stats
    */
   def atomsCount = disjuncts.map(_._2.size).sum + conjuncts.map(i => atomNum(i._2)).sum
-  def funsCount = disjuncts.map(_._2.filter {
+  def funsCount = disjuncts.map(_._2.count {
     case _: Call | _: ADTConstraint => true
-    case _                          => false
-  }.size).sum
+    case _ => false
+  }).sum
 
   /**
    * Functions solely used for debugging
@@ -465,14 +459,14 @@ class Formula(val fd: FunDef, initexpr: Expr, ctx: InferenceContext, initSpecCal
   def pickSatFromUnflatFormula(unflate: Expr, model: Model, evaluator: DefaultEvaluator): Seq[Expr] = {
     def rec(e: Expr): Seq[Expr] = e match {
       case IfExpr(cond, thn, elze) =>
-        evaluator.eval(cond, model) match {
+        (evaluator.eval(cond, model): @unchecked) match {
           case Successful(BooleanLiteral(true)) => cond +: rec(thn)
           case Successful(BooleanLiteral(false)) => Not(cond) +: rec(elze)
         }
       case And(args) => args flatMap rec
       case Or(args) => rec(args.find(evaluator.eval(_, model) == Successful(BooleanLiteral(true))).get)
       case Equals(b: Variable, rhs) if b.getType == BooleanType =>
-        evaluator.eval(b, model) match {
+        (evaluator.eval(b, model): @unchecked) match {
           case Successful(BooleanLiteral(true)) =>
             rec(b) ++ rec(rhs)
           case Successful(BooleanLiteral(false)) =>

src/main/scala/leon/invariant/templateSolvers/UFADTEliminator.scala

@@ -78,7 +78,7 @@ class UFADTEliminator(ctx: LeonContext, program: Program) {
       }
       // an weaker property whose equality is necessary for mayAlias
       val hashcode =
-        key match {
+        (key: @unchecked) match {
           case Left(TypedFunDef(fd, _))   => fd.id.hashCode()
           case Right(ct: CaseClassType)   => ct.classDef.id.hashCode()
           case Right(tp @ TupleType(tps)) => (tps.hashCode() << 3) ^ tp.dimension

src/test/scala/leon/regression/orb/LazyEvalRegressionSuite.scala

@@ -4,9 +4,7 @@ package leon.regression.orb
 import leon.test._
 
 import leon._
-import purescala.Definitions._
 import invariant.engine._
-import transformations._
 import laziness._
 import verification._
 
@@ -35,14 +33,14 @@ class LazyEvalRegressionSuite extends LeonRegressionSuite {
     }
     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")}")
+      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")}")
     }
   }