Add bound variables in simplifier

src/main/scala/inox/transformers/SimplifierWithPC.scala

@@ -97,7 +97,7 @@ trait SimplifierWithPC extends Transformer { self =>
     case c: Choose => (c, opts.assumeChecked)
 
     case Lambda(params, body) =>
-      val (rb, _) = simplify(body, path)
+      val (rb, _) = simplify(body, path withBounds params)
       (Lambda(params, rb).copiedFrom(e), true)
 
     case Implies(l, r) => simplify(Or(Not(l).copiedFrom(l), r).copiedFrom(e), path)
@@ -265,14 +265,16 @@ trait SimplifierWithPC extends Transformer { self =>
       val (rargs, pargs) = args.map(simplify(_, path)).unzip
       (FunctionInvocation(id, tps, rargs).copiedFrom(fi), pargs.foldLeft(isPureFunction(id))(_ && _))
 
-    case n @ Not(e)           => simplifyAndCons(Seq(e), path, es => not(es.head).copiedFrom(n))
-    case Equals(l, r)         => simplifyAndCons(Seq(l, r), path, es => equality(es(0), es(1)).copiedFrom(e))
-    case Tuple(es)            => simplifyAndCons(es, path, es => tupleWrap(es).copiedFrom(e))
-    case UMinus(t)            => simplifyAndCons(Seq(t), path, es => uminus(es.head).copiedFrom(e))
-    case Plus(l, r)           => simplifyAndCons(Seq(l, r), path, es => plus(es(0), es(1)).copiedFrom(e))
-    case Minus(l, r)          => simplifyAndCons(Seq(l, r), path, es => minus(es(0), es(1)).copiedFrom(e))
-    case Times(l, r)          => simplifyAndCons(Seq(l, r), path, es => times(es(0), es(1)).copiedFrom(e))
-    case Forall(params, body) => simplifyAndCons(Seq(body), path, es => simpForall(params, es.head).copiedFrom(e))
+    case n @ Not(e)   => simplifyAndCons(Seq(e), path, es => not(es.head).copiedFrom(n))
+    case Equals(l, r) => simplifyAndCons(Seq(l, r), path, es => equality(es(0), es(1)).copiedFrom(e))
+    case Tuple(es)    => simplifyAndCons(es, path, es => tupleWrap(es).copiedFrom(e))
+    case UMinus(t)    => simplifyAndCons(Seq(t), path, es => uminus(es.head).copiedFrom(e))
+    case Plus(l, r)   => simplifyAndCons(Seq(l, r), path, es => plus(es(0), es(1)).copiedFrom(e))
+    case Minus(l, r)  => simplifyAndCons(Seq(l, r), path, es => minus(es(0), es(1)).copiedFrom(e))
+    case Times(l, r)  => simplifyAndCons(Seq(l, r), path, es => times(es(0), es(1)).copiedFrom(e))
+
+    case Forall(params, body) =>
+      simplifyAndCons(Seq(body), path withBounds params, es => simpForall(params, es.head).copiedFrom(e))
 
     case app @ Application(e, es)  =>
       val (caller, recons): (Expr, Expr => Expr) = simplify(e, path) match {