From c373f2165a9b94615f6b2d66469f5ecae247ef20 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Fri, 28 Aug 2015 14:32:45 +0200
Subject: [PATCH] Forwarded to current master

---
 .../leon/evaluators/RecursiveEvaluator.scala  |  7 --
 .../frontends/scalac/CodeExtraction.scala     | 16 +++++
 .../scala/leon/purescala/CheckForalls.scala   | 64 +++++++++++--------
 src/main/scala/leon/purescala/ExprOps.scala   |  3 +-
 .../scala/leon/purescala/Expressions.scala    |  6 ++
 .../scala/leon/purescala/Extractors.scala     |  2 +
 .../leon/solvers/smtlib/SMTLIBSolver.scala    |  5 +-
 .../solvers/templates/TemplateGenerator.scala | 32 +++++++---
 .../solvers/z3/Z3ModelReconstruction.scala    |  2 -
 .../purescala/invalid/HOInvocations2.scala    | 16 +++++
 .../invalid/InductiveQuantification.scala     | 17 +++++
 .../purescala/invalid/Monotonic.scala         | 10 +++
 .../purescala/invalid/PositiveMap2.scala      | 23 +++++++
 .../purescala/invalid/Postcondition.scala     | 14 ++++
 .../invalid/SimpleQuantification.scala        | 20 ++++++
 .../purescala/valid/Composition.scala         | 14 ++++
 .../purescala/valid/HOInvocations2.scala      | 17 +++++
 .../valid/InductiveQuantification.scala       | 26 ++++++++
 .../purescala/valid/Monotonic.scala           | 10 +++
 .../purescala/valid/PositiveMap2.scala        | 33 ++++++++++
 .../purescala/valid/Postcondition.scala       | 23 +++++++
 .../valid/SimpleQuantification.scala          | 44 +++++++++++++
 .../valid/TransitiveQuantification.scala      | 12 ++++
 23 files changed, 368 insertions(+), 48 deletions(-)
 create mode 100644 src/test/resources/regression/verification/purescala/invalid/HOInvocations2.scala
 create mode 100644 src/test/resources/regression/verification/purescala/invalid/InductiveQuantification.scala
 create mode 100644 src/test/resources/regression/verification/purescala/invalid/Monotonic.scala
 create mode 100644 src/test/resources/regression/verification/purescala/invalid/PositiveMap2.scala
 create mode 100644 src/test/resources/regression/verification/purescala/invalid/Postcondition.scala
 create mode 100644 src/test/resources/regression/verification/purescala/invalid/SimpleQuantification.scala
 create mode 100644 src/test/resources/regression/verification/purescala/valid/Composition.scala
 create mode 100644 src/test/resources/regression/verification/purescala/valid/HOInvocations2.scala
 create mode 100644 src/test/resources/regression/verification/purescala/valid/InductiveQuantification.scala
 create mode 100644 src/test/resources/regression/verification/purescala/valid/Monotonic.scala
 create mode 100644 src/test/resources/regression/verification/purescala/valid/PositiveMap2.scala
 create mode 100644 src/test/resources/regression/verification/purescala/valid/Postcondition.scala
 create mode 100644 src/test/resources/regression/verification/purescala/valid/SimpleQuantification.scala
 create mode 100644 src/test/resources/regression/verification/purescala/valid/TransitiveQuantification.scala

diff --git a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
index f67f03e19..38710837f 100644
--- a/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
+++ b/src/main/scala/leon/evaluators/RecursiveEvaluator.scala
@@ -551,14 +551,7 @@ abstract class RecursiveEvaluator(ctx: LeonContext, prog: Program, maxSteps: Int
     case p : Passes => 
       e(p.asConstraint)
 
-<<<<<<< HEAD
     case choose: Choose =>
-=======
-    case choose @ Choose(_, Some(impl)) =>
-      e(impl)
-
-    case choose @ Choose(_, None) =>
->>>>>>> Reverted evaluation of quantifiers
 
       implicit val debugSection = utils.DebugSectionSynthesis
 
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index da0a83066..025aa4b98 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1312,6 +1312,22 @@ trait CodeExtraction extends ASTExtractors {
 
           Lambda(vds, exBody)
 
+        case ExForallExpression(args, body) =>
+          val vds = args map { case (tpt, sym) =>
+            val aTpe = extractType(tpt)
+            val newID = FreshIdentifier(sym.name.toString, aTpe)
+            owners += (newID -> None)
+            LeonValDef(newID)
+          }
+
+          val newVars = (args zip vds).map { case ((_, sym), lvd) =>
+            sym -> (() => lvd.toVariable)
+          }
+
+          val exBody = extractTree(body)(dctx.withNewVars(newVars))
+
+          Forall(vds, exBody)
+
         case ExFiniteMap(tptFrom, tptTo, args) =>
           val singletons: Seq[(LeonExpr, LeonExpr)] = args.collect {
             case ExTuple(tpes, trees) if trees.size == 2 =>
diff --git a/src/main/scala/leon/purescala/CheckForalls.scala b/src/main/scala/leon/purescala/CheckForalls.scala
index 6afcfad1f..bb9874373 100644
--- a/src/main/scala/leon/purescala/CheckForalls.scala
+++ b/src/main/scala/leon/purescala/CheckForalls.scala
@@ -60,34 +60,44 @@ object CheckForalls extends UnitPhase[Program] {
             })
           }) ctx.reporter.warning("Matcher arguments must have simple form in " + conjunct)
 
-          if (matchers.filter(_._2.exists {
-            case Variable(id) => quantified(id)
-            case _ => false
-          }).map(_._1).toSet.size != 1)
-            ctx.reporter.warning("Quantification conjuncts must contain exactly one matcher in " + conjunct)
+          val id2Quant = matchers.foldLeft(Map.empty[Identifier, Set[Identifier]]) {
+            case (acc, (m, args)) => acc + (m -> (acc.getOrElse(m, Set.empty) ++ args.flatMap {
+              case Variable(id) if quantified(id) => Set(id)
+              case _ => Set.empty[Identifier]
+            }))
+          }
 
-          preTraversal {
-            case Matcher(_, _) => // OK
-            case LessThan(_: Variable, _: Variable) => // OK
-            case LessEquals(_: Variable, _: Variable) => // OK
-            case GreaterThan(_: Variable, _: Variable) => // OK
-            case GreaterEquals(_: Variable, _: Variable) => // OK
-            case And(_) => // OK
-            case Or(_) => // OK
-            case Implies(_, _) => // OK
-            case BinaryOperator(Matcher(_, _), _, _) => // OK
-            case BinaryOperator(_, Matcher(_, _), _) => // OK
-            case BinaryOperator(e1, _, _) if (variablesOf(e1) & quantified).isEmpty => // OK
-            case BinaryOperator(_, e2, _) if (variablesOf(e2) & quantified).isEmpty => // OK
-            case FunctionInvocation(_, args) if {
-              val argVars = args.flatMap(variablesOf).toSet
-              (argVars & quantified).size <= 1 && (argVars & free).isEmpty
-            } => // OK
-            case UnaryOperator(_, _) => // OK
-            case BinaryOperator(e1, e2, _) if ((variablesOf(e1) ++ variablesOf(e2)) & quantified).isEmpty => // OK
-            case NAryOperator(es, _) if (es.flatMap(variablesOf).toSet & quantified).isEmpty => // OK
-            case _: Terminal => // OK
-            case e => ctx.reporter.warning("Invalid operation " + e + " on quantified variables")
+          if (id2Quant.filter(_._2.nonEmpty).groupBy(_._2).size != 1)
+            ctx.reporter.warning("Multiple matchers must provide bijective matching in " + conjunct)
+
+          foldRight[Set[Identifier]] { case (m, children) =>
+            val q = children.toSet.flatten
+
+            m match {
+              case Matcher(_, args) =>
+                q -- args.flatMap {
+                  case Variable(id) if quantified(id) => Set(id)
+                  case _ => Set.empty[Identifier]
+                }
+              case LessThan(_: Variable, _: Variable) => q
+              case LessEquals(_: Variable, _: Variable) => q
+              case GreaterThan(_: Variable, _: Variable) => q
+              case GreaterEquals(_: Variable, _: Variable) => q
+              case And(_) => q
+              case Or(_) => q
+              case Implies(_, _) => q
+              case Operator(es, _) =>
+                val vars = es.flatMap {
+                  case Variable(id) => Set(id)
+                  case _ => Set.empty[Identifier]
+                }.toSet
+
+                if (!(q.isEmpty || (q.size == 1 && (vars & free).isEmpty)))
+                  ctx.reporter.warning("Invalid operation " + m + " on quantified variables")
+                q -- vars
+              case Variable(id) if quantified(id) => Set(id)
+              case _ => q
+            }
           } (conjunct)
         }
       }
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 484b468ba..3f641000a 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -319,7 +319,8 @@ object ExprOps {
           case Let(i,_,_)   => subvs - i
           case MatchExpr(_, cses)  => subvs -- cses.flatMap(_.pattern.binders)
           case Passes(_, _ , cses) => subvs -- cses.flatMap(_.pattern.binders)
-          case Lambda(args, _)  => subvs -- args.map(_.id)
+          case Lambda(args, _) => subvs -- args.map(_.id)
+          case Forall(args, _) => subvs -- args.map(_.id)
           case _ => subvs
         }
     }(expr)
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index 720024b4f..f738c3f38 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -226,6 +226,12 @@ object Expressions {
     }
   }
 
+  /* Universal Quantification */
+
+  case class Forall(args: Seq[ValDef], body: Expr) extends Expr {
+    assert(body.getType == BooleanType)
+    val getType = BooleanType
+  }
 
   /* Control flow */
 
diff --git a/src/main/scala/leon/purescala/Extractors.scala b/src/main/scala/leon/purescala/Extractors.scala
index ca6a21fb0..c1e1ff439 100644
--- a/src/main/scala/leon/purescala/Extractors.scala
+++ b/src/main/scala/leon/purescala/Extractors.scala
@@ -41,6 +41,8 @@ object Extractors {
         Some((Seq(a), (es: Seq[Expr]) => ArrayLength(es.head)))
       case Lambda(args, body) =>
         Some((Seq(body), (es: Seq[Expr]) => Lambda(args, es.head)))
+      case Forall(args, body) =>
+        Some((Seq(body), (es: Seq[Expr]) => Forall(args, es.head)))
 
       /* Binary operators */
       case LetDef(fd, body) => Some((
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index bcf8a5fa1..f6e00625a 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -62,7 +62,10 @@ abstract class SMTLIBSolver(val context: LeonContext,
 
     reporter.debug(s"Outputting smt session into $fileName" )
 
-    val fw = new java.io.FileWriter(fileName, false)
+    val javaFile = new java.io.File(fileName)
+    javaFile.getParentFile.mkdirs()
+
+    val fw = new java.io.FileWriter(javaFile, false)
 
     fw.write("; Solver : "+name+"\n")
     fw.write("; Options: "+interpreterOps(context).mkString(" ")+"\n")
diff --git a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
index ac155c710..725fecfa5 100644
--- a/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
+++ b/src/main/scala/leon/solvers/templates/TemplateGenerator.scala
@@ -47,11 +47,13 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
     val newBody : Option[Expr] = tfd.body.map(b => matchToIfThenElse(b))
     val lambdaBody : Option[Expr] = newBody.map(b => simplifyHOFunctions(b))
 
-    val invocation : Expr = FunctionInvocation(tfd, tfd.params.map(_.toVariable))
+    val funDefArgs: Seq[Identifier] = tfd.params.map(_.id)
+    val lambdaArguments: Seq[Identifier] = lambdaBody.map(lambdaArgs).toSeq.flatten
+    val invocation : Expr = FunctionInvocation(tfd, funDefArgs.map(_.toVariable))
 
     val invocationEqualsBody : Option[Expr] = lambdaBody match {
       case Some(body) if isRealFunDef =>
-        val b : Expr = appliedEquals(invocation, body)
+        val b : Expr = And(Equals(invocation, body), liftedEquals(invocation, body, lambdaArguments))
 
         Some(if(prec.isDefined) {
           Implies(prec.get, b)
@@ -66,8 +68,7 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
     val start : Identifier = FreshIdentifier("start", BooleanType, true)
     val pathVar : (Identifier, T) = start -> encoder.encodeId(start)
 
-    val funDefArgs : Seq[Identifier] = tfd.params.map(_.id)
-    val allArguments = funDefArgs ++ lambdaBody.map(lambdaArgs).toSeq.flatten
+    val allArguments : Seq[Identifier] = funDefArgs ++ lambdaArguments
     val arguments : Seq[(Identifier, T)] = allArguments.map(id => id -> encoder.encodeId(id))
 
     val substMap : Map[Identifier, T] = arguments.toMap + pathVar
@@ -115,13 +116,24 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
 
   private def lambdaArgs(expr: Expr): Seq[Identifier] = expr match {
     case Lambda(args, body) => args.map(_.id) ++ lambdaArgs(body)
+    case IsTyped(_, _: FunctionType) => sys.error("Only applicable on lambda chains")
     case _ => Seq.empty
   }
 
-  private def appliedEquals(invocation: Expr, body: Expr): Expr = body match {
-    case Lambda(args, lambdaBody) =>
-      appliedEquals(application(invocation, args.map(_.toVariable)), lambdaBody)
-    case _ => Equals(invocation, body)
+  private def liftedEquals(invocation: Expr, body: Expr, args: Seq[Identifier], inlineFirst: Boolean = false): Expr = {
+    def rec(i: Expr, b: Expr, args: Seq[Identifier], inline: Boolean): Seq[Expr] = i.getType match {
+      case FunctionType(from, to) =>
+        val (currArgs, nextArgs) = args.splitAt(from.size)
+        val arguments = currArgs.map(_.toVariable)
+        val apply = if (inline) application _ else Application
+        val (appliedInv, appliedBody) = (apply(i, arguments), apply(b, arguments))
+        Equals(appliedInv, appliedBody) +: rec(appliedInv, appliedBody, nextArgs, false)
+      case _ =>
+        assert(args.isEmpty, "liftedEquals should consume all provided arguments")
+        Seq.empty
+    }
+
+    andJoin(rec(invocation, body, args, inlineFirst))
   }
 
   def mkClauses(pathVar: Identifier, expr: Expr, substMap: Map[Identifier, T]):
@@ -263,10 +275,10 @@ class TemplateGenerator[T](val encoder: TemplateEncoder[T],
 
         case l @ Lambda(args, body) =>
           val idArgs : Seq[Identifier] = lambdaArgs(l)
-          val trArgs : Seq[T] = idArgs.map(encoder.encodeId)
+          val trArgs : Seq[T] = idArgs.map(id => substMap.getOrElse(id, encoder.encodeId(id)))
 
           val lid = FreshIdentifier("lambda", l.getType, true)
-          val clause = appliedEquals(Variable(lid), l)
+          val clause = liftedEquals(Variable(lid), l, idArgs, inlineFirst = true)
 
           val localSubst: Map[Identifier, T] = substMap ++ condVars ++ exprVars ++ lambdaVars
           val clauseSubst: Map[Identifier, T] = localSubst ++ (idArgs zip trArgs)
diff --git a/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala b/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
index 5b9d6be13..62f43d736 100644
--- a/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
+++ b/src/main/scala/leon/solvers/z3/Z3ModelReconstruction.scala
@@ -38,8 +38,6 @@ trait Z3ModelReconstruction {
   def modelToMap(model: Z3Model, ids: Iterable[Identifier]) : Map[Identifier,Expr] = {
     var asMap = Map.empty[Identifier,Expr]
 
-    println(model)
-
     def completeID(id : Identifier) : Unit = {
       asMap = asMap + (id -> simplestValue(id.getType))
       reporter.debug("Completing variable '" + id + "' to simplest value")
diff --git a/src/test/resources/regression/verification/purescala/invalid/HOInvocations2.scala b/src/test/resources/regression/verification/purescala/invalid/HOInvocations2.scala
new file mode 100644
index 000000000..5cd0afc42
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/HOInvocations2.scala
@@ -0,0 +1,16 @@
+import leon.lang._
+
+object HOInvocations {
+  def switch(x: BigInt, f: (BigInt) => BigInt, g: (BigInt) => BigInt) = if(x > 0) f else g
+
+  def failling_1(f: (BigInt) => BigInt) = {
+    switch(-10, (x: BigInt) => x + 1, f)(2)
+  } ensuring { res => res > 0 }
+
+  def failling_2(x: BigInt, f: (BigInt) => BigInt, g: (BigInt) => BigInt) = {
+    require(x > 0 && forall((a: BigInt) => a > 0 ==> f(a) > 0))
+    switch(1, switch(x, f, g), g)(0)
+  } ensuring { res => res > 0 }
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/verification/purescala/invalid/InductiveQuantification.scala b/src/test/resources/regression/verification/purescala/invalid/InductiveQuantification.scala
new file mode 100644
index 000000000..970b3b53b
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/InductiveQuantification.scala
@@ -0,0 +1,17 @@
+import leon.lang._
+
+object SizeInc {
+  
+  abstract class List[A]
+  case class Cons[A](head: A, tail: List[A]) extends List[A]
+  case class Nil[A]() extends List[A]
+
+  def failling_1[A](x: List[A]): Int => Int = {
+    (i: Int) => x match {
+      case Cons(head, tail) => 1 + failling_1(tail)(i)
+      case Nil() => i
+    }
+  } ensuring { res => forall((a: Int) => res(a) > 0) }
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/verification/purescala/invalid/Monotonic.scala b/src/test/resources/regression/verification/purescala/invalid/Monotonic.scala
new file mode 100644
index 000000000..bc9a1bc76
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/Monotonic.scala
@@ -0,0 +1,10 @@
+import leon.lang._
+
+object Monotonic {
+  def failling_1(f: BigInt => BigInt, g: BigInt => BigInt): BigInt => BigInt = {
+    require(forall((a: BigInt, b: BigInt) => (a > b ==> f(a) > f(b))))
+    (x: BigInt) => f(g(x))
+  } ensuring { res => forall((a: BigInt, b: BigInt) => a > b ==> res(a) > res(b)) }
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/verification/purescala/invalid/PositiveMap2.scala b/src/test/resources/regression/verification/purescala/invalid/PositiveMap2.scala
new file mode 100644
index 000000000..7b15cb257
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/PositiveMap2.scala
@@ -0,0 +1,23 @@
+import leon.lang._
+
+object PositiveMap {
+  
+  abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case class Nil() extends List
+
+  def positive(list: List): Boolean = list match {
+    case Cons(head, tail) => if (head < 0) false else positive(tail)
+    case Nil() => true
+  }
+
+  def positiveMap_failling_1(f: (BigInt) => BigInt, list: List): List = {
+    require(forall((a: BigInt) => f(a) > -2))
+    list match {
+      case Cons(head, tail) => Cons(f(head), positiveMap_failling_1(f, tail))
+      case Nil() => Nil()
+    }
+  } ensuring { res => positive(res) }
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/verification/purescala/invalid/Postcondition.scala b/src/test/resources/regression/verification/purescala/invalid/Postcondition.scala
new file mode 100644
index 000000000..d942f446e
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/Postcondition.scala
@@ -0,0 +1,14 @@
+import leon.lang._
+
+object Postconditions {
+  def failling_1(f: BigInt => BigInt) = {
+    require(forall((a: BigInt) => a > 0 ==> f(a) > 0))
+    f(10)
+  } ensuring { res => forall((a: BigInt) => res > f(a)) }
+
+  def failling_2(f: BigInt => BigInt, x: BigInt) = {
+    require(x >= 0 && forall((a: BigInt) => a > 0 ==> f(a) < 0))
+    x
+  } ensuring { res => forall((a: BigInt) => res > f(a)) }
+
+}
diff --git a/src/test/resources/regression/verification/purescala/invalid/SimpleQuantification.scala b/src/test/resources/regression/verification/purescala/invalid/SimpleQuantification.scala
new file mode 100644
index 000000000..7a3446612
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/invalid/SimpleQuantification.scala
@@ -0,0 +1,20 @@
+import leon.lang._
+
+object Simple {
+
+  def failling_1(f: BigInt => BigInt) = {
+    require(forall((a: BigInt) => a > 0 ==> f(a) > 0))
+    f(-1)
+  } ensuring { res => res > 0 }
+
+  def failling_2(f: BigInt => BigInt) = {
+    require(forall((a: BigInt) => a > 0 ==> f(a) > 1))
+    f(1) + f(2)
+  } ensuring { res => res > 4 }
+
+  def failling_4(f: BigInt => BigInt, g: BigInt => BigInt, x: BigInt) = {
+    require(forall((a: BigInt, b: BigInt) => f(a) + g(a) > 0))
+    if(x < 0) f(x) + g(x)
+    else x
+  } ensuring { res => res > 0 }
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/Composition.scala b/src/test/resources/regression/verification/purescala/valid/Composition.scala
new file mode 100644
index 000000000..cd62eb8da
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/Composition.scala
@@ -0,0 +1,14 @@
+
+import leon.lang._
+
+object Composition {
+  def passing_1(f: (Int) => Int, g: (Int) => Int, x: Int): Int = {
+    require(g(1) == 2 && forall((a: Int) => f(g(a)) == a))
+    val a = g(x)
+    if(x == 1)
+      f(g(a))
+    else 2
+  } ensuring { _ == 2 }
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/verification/purescala/valid/HOInvocations2.scala b/src/test/resources/regression/verification/purescala/valid/HOInvocations2.scala
new file mode 100644
index 000000000..ba44b8fdc
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/HOInvocations2.scala
@@ -0,0 +1,17 @@
+import leon.lang._
+
+object HOInvocations {
+  def switch(x: Int, f: (Int) => Int, g: (Int) => Int) = if(x > 0) f else g
+
+  def passing_1(f: (Int) => Int) = {
+    switch(10, (x: Int) => x + 1, f)(2)
+  } ensuring { res => res > 0 }
+
+  def passing_2(x: Int, f: (Int) => Int, g: (Int) => Int) = {
+    require(x > 0 && forall((a: Int) => a > 0 ==> f(a) > 0))
+    switch(1, switch(x, f, g), g)(1)
+  } ensuring { res => res > 0 }
+
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/verification/purescala/valid/InductiveQuantification.scala b/src/test/resources/regression/verification/purescala/valid/InductiveQuantification.scala
new file mode 100644
index 000000000..9fe7ea96e
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/InductiveQuantification.scala
@@ -0,0 +1,26 @@
+import leon.lang._
+
+object SizeInc {
+  
+  abstract class List[A]
+  case class Cons[A](head: A, tail: List[A]) extends List[A]
+  case class Nil[A]() extends List[A]
+
+  def sizeInc[A](x: List[A]): BigInt => BigInt = {
+    (i: BigInt) => x match {
+      case Cons(head, tail) => 1 + sizeInc(tail)(i)
+      case Nil() => i
+    }
+  } ensuring { res => forall((a: BigInt) => a > 0 ==> res(a) > 0) }
+
+  def sizeInc2[A](x: BigInt): List[A] => BigInt = {
+    require(x > 0)
+
+    (list: List[A]) => list match {
+      case Cons(head, tail) => 1 + sizeInc2(x)(tail)
+      case Nil() => x
+    }
+  } ensuring { res => forall((a: List[A]) => res(a) > 0) }
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/verification/purescala/valid/Monotonic.scala b/src/test/resources/regression/verification/purescala/valid/Monotonic.scala
new file mode 100644
index 000000000..cef6be60f
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/Monotonic.scala
@@ -0,0 +1,10 @@
+import leon.lang._
+
+object Monotonic {
+  def composeMonotonic(f: BigInt => BigInt, g: BigInt => BigInt): BigInt => BigInt = {
+    require(forall((a: BigInt, b: BigInt) => (a > b ==> f(a) > f(b)) && (a > b ==> g(a) > g(b))))
+    (x: BigInt) => f(g(x))
+  } ensuring { res => forall((a: BigInt, b: BigInt) => a > b ==> res(a) > res(b)) }
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/verification/purescala/valid/PositiveMap2.scala b/src/test/resources/regression/verification/purescala/valid/PositiveMap2.scala
new file mode 100644
index 000000000..030e70959
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/PositiveMap2.scala
@@ -0,0 +1,33 @@
+
+import leon.lang._
+
+object PositiveMap {
+  
+  abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case class Nil() extends List
+
+  def positive(list: List): Boolean = list match {
+    case Cons(head, tail) => if (head < 0) false else positive(tail)
+    case Nil() => true
+  }
+
+  def positiveMap_passing_1(f: (BigInt) => BigInt, list: List): List = {
+    require(forall((a: BigInt) => f(a) > 0))
+    list match {
+      case Cons(head, tail) => Cons(f(head), positiveMap_passing_1(f, tail))
+      case Nil() => Nil()
+    }
+  } ensuring { res => positive(res) }
+
+  def positiveMap_passing_2(f: (BigInt) => BigInt, list: List): List = {
+    require(forall((a: BigInt) => f(a) > -1))
+    list match {
+      case Cons(head, tail) => Cons(f(head), positiveMap_passing_2(f, tail))
+      case Nil() => Nil()
+    }
+  } ensuring { res => positive(res) }
+
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/verification/purescala/valid/Postcondition.scala b/src/test/resources/regression/verification/purescala/valid/Postcondition.scala
new file mode 100644
index 000000000..e044a9a3a
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/Postcondition.scala
@@ -0,0 +1,23 @@
+import leon.lang._
+
+object Postconditions {
+
+  def passing_1(f: BigInt => BigInt, x: BigInt) = {
+    require(x >= 0 && forall((a: BigInt) => f(a) < 0))
+    x
+  } ensuring { res => forall((a: BigInt) => res > f(a)) }
+
+  def passing_2(f: BigInt => BigInt, x: BigInt) = {
+    require(x >= 0 && forall((a: BigInt) => a > 0 ==> f(a) < 0))
+    x
+  } ensuring { res => forall((a: BigInt) => a > 0 ==> res > f(a)) }
+
+  def passing_3(f: BigInt => BigInt) = {
+    require(forall((a: BigInt) => f(a) > 0))
+    f
+  } ensuring { res => forall((a: BigInt) => res(a) > 0) }
+
+  def passing_4() = {
+    (x: BigInt) => x + 1
+  } ensuring { res => forall((a: BigInt) => res(a) > a) }
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/SimpleQuantification.scala b/src/test/resources/regression/verification/purescala/valid/SimpleQuantification.scala
new file mode 100644
index 000000000..5e7e9cb33
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/SimpleQuantification.scala
@@ -0,0 +1,44 @@
+import leon.lang._
+
+object Simple {
+
+  def passing_1(f: BigInt => BigInt) = {
+    require(forall((a: BigInt) => a > 0 ==> f(a) > 0))
+    f(10)
+  } ensuring { res => res > 0 }
+
+  def passing_2(f: BigInt => BigInt) = {
+    require(forall((a: BigInt) => a > 0 ==> f(a) > 1))
+    f(1) + f(2)
+  } ensuring { res => res > 2 }
+
+  def passing_3(f: BigInt => BigInt) = {
+    require(forall((a: BigInt) => f(a) > 0 || f(a) < 0))
+    f(8)
+  } ensuring { res => res != 0 }
+
+  def passing_4(f: BigInt => BigInt, g: BigInt => BigInt, x: BigInt) = {
+    require(forall((a: BigInt, b: BigInt) => f(a) + f(b) > 0))
+    if(x <= 0) f(x) + f(x)
+    else x
+  } ensuring { res => res > 0 }
+
+  def passing_5(f: BigInt => BigInt, g: BigInt => Boolean): BigInt = {
+    require(forall((a: BigInt) => if(g(a)) { f(a) > 0 || f(a) < 0 } else { f(a) == 0 }))
+    if(g(8)) f(8)
+    else BigInt(1)
+  } ensuring { res => res != 0 }
+
+  def passing_6(f: BigInt => BigInt, x: BigInt) = {
+    require(x > 0 && forall((a: BigInt) => a > 0 ==> f(a) > 0))
+    if(x > 0) f(1)
+    else f(-1)
+  } ensuring { res => res > 0 }
+
+  def passing_7(f: BigInt => BigInt) = {
+    require(forall((a: BigInt) => a > 0 ==> f(a) > 0))
+    val a = f(-1)
+    f(2)
+  } ensuring { res => res > 0 }
+
+}
diff --git a/src/test/resources/regression/verification/purescala/valid/TransitiveQuantification.scala b/src/test/resources/regression/verification/purescala/valid/TransitiveQuantification.scala
new file mode 100644
index 000000000..5e7bb03cd
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/TransitiveQuantification.scala
@@ -0,0 +1,12 @@
+import leon.lang._
+
+object Transitive {
+  
+  def multiAssoc(f: (Int, Int, Int) => Int): Boolean = {
+    require(forall { (a: Int, b: Int, c: Int, d: Int, e: Int) =>
+      f(f(a,b,c),d,e) == f(a,f(b,c,d),e) && f(a,f(b,c,d),e) == f(a,b,f(c,d,e))
+    })
+    f(f(1,2,3),4,5) == f(1,2,f(3,4,5))
+  }.holds
+
+}
-- 
GitLab