diff --git a/library/lang/package.scala b/library/lang/package.scala
index 44351d02ca9328bbbf86063745d233f2db17cd7c..bb7ec69122f4814bd61b1ce79f94c2eab9054c74 100644
--- a/library/lang/package.scala
+++ b/library/lang/package.scala
@@ -47,6 +47,9 @@ package object lang {
@ignore
def error[T](reason: java.lang.String): T = sys.error(reason)
+ @ignore
+ def old[T](value: T): T = value
+
@ignore
implicit class Passes[A,B](io : (A,B)) {
val (in, out) = io
diff --git a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
index db477ec494742b0dc2b0e42e098676c4ab55282d..fb64b3311dfdd2af5b06df85ab2cb26088d3233e 100644
--- a/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
+++ b/src/main/scala/leon/frontends/scalac/ASTExtractors.scala
@@ -574,6 +574,15 @@ trait ASTExtractors {
}
}
+ object ExOldExpression {
+ def unapply(tree: Apply) : Option[Symbol] = tree match {
+ case a @ Apply(TypeApply(ExSymbol("leon", "lang", "old"), List(tpe)), List(arg)) =>
+ Some(arg.symbol)
+ case _ =>
+ None
+ }
+ }
+
object ExHoleExpression {
def unapply(tree: Tree) : Option[(Tree, List[Tree])] = tree match {
case a @ Apply(TypeApply(s @ ExSymbol("leon", "lang", "synthesis", "$qmark"), List(tpt)), args1) =>
diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 77a6c719f8f4d0c06766982456b6a094545512ce..4bca0e76794e64a40f32b56679d4a502d0b1590c 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -1054,6 +1054,15 @@ trait CodeExtraction extends ASTExtractors {
val tupleExprs = exprs.map(e => extractTree(e))
Tuple(tupleExprs)
+ case ex@ExOldExpression(sym) if dctx.isVariable(sym) =>
+ dctx.vars.get(sym).orElse(dctx.mutableVars.get(sym)) match {
+ case Some(builder) =>
+ val Variable(id) = builder()
+ Old(id).setPos(ex.pos)
+ case None =>
+ outOfSubsetError(current, "old can only be used with variables")
+ }
+
case ExErrorExpression(str, tpt) =>
Error(extractType(tpt), str)
@@ -1105,7 +1114,7 @@ trait CodeExtraction extends ASTExtractors {
val oldCurrentFunDef = currentFunDef
- val funDefWithBody = extractFunBody(fd, params, b)(newDctx.copy(mutableVars = Map()))
+ val funDefWithBody = extractFunBody(fd, params, b)(newDctx)
currentFunDef = oldCurrentFunDef
@@ -1200,11 +1209,11 @@ trait CodeExtraction extends ASTExtractors {
}
getOwner(lhsRec) match {
- case Some(Some(fd)) if fd != currentFunDef =>
- outOfSubsetError(tr, "cannot update an array that is not defined locally")
+ // case Some(Some(fd)) if fd != currentFunDef =>
+ // outOfSubsetError(tr, "cannot update an array that is not defined locally")
- case Some(None) =>
- outOfSubsetError(tr, "cannot update an array that is not defined locally")
+ // case Some(None) =>
+ // outOfSubsetError(tr, "cannot update an array that is not defined locally")
case Some(_) =>
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index c106d1393bcf793a7fe5d6944ecd533d84a42e36..c80d777480f66d795f2bc15eef0a3010452394fb 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -345,6 +345,7 @@ object ExprOps {
val subvs = subs.flatten.toSet
e match {
case Variable(i) => subvs + i
+ case Old(i) => subvs + i
case LetDef(fd, _) => subvs -- fd.params.map(_.id)
case Let(i, _, _) => subvs - i
case LetVar(i, _, _) => subvs - i
diff --git a/src/main/scala/leon/purescala/Expressions.scala b/src/main/scala/leon/purescala/Expressions.scala
index 6e9adae5f6ee3548b1fa70af41b127e6a46a76b4..1569ebfb8ab3d8c0ab7f0e09bbb31f82870fc8f9 100644
--- a/src/main/scala/leon/purescala/Expressions.scala
+++ b/src/main/scala/leon/purescala/Expressions.scala
@@ -76,6 +76,10 @@ object Expressions {
val getType = tpe
}
+ case class Old(id: Identifier) extends Expr with Terminal {
+ val getType = id.getType
+ }
+
/** Precondition of an [[Expressions.Expr]]. Corresponds to the Leon keyword *require*
*
* @param pred The precondition formula inside ``require(...)``
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index 6b22810e542bdb9af65251da1c9a4d4ab1ab7142..3b96fff138dd7bc6a91c66acf3e3928fac0e44d0 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -77,6 +77,9 @@ class PrettyPrinter(opts: PrinterOptions,
}
p"$name"
+ case Old(id) =>
+ p"old($id)"
+
case Variable(id) =>
p"$id"
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index fe9582d548deb679e0de7a082d5e4ba178582a1f..e9802d500208b96b5af448391d69c6660a05f843 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -10,6 +10,7 @@ import leon.purescala.Extractors._
import leon.purescala.Constructors._
import leon.purescala.ExprOps._
import leon.purescala.TypeOps._
+import leon.purescala.Types._
import leon.xlang.Expressions._
object ImperativeCodeElimination extends UnitPhase[Program] {
@@ -22,13 +23,22 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
fd <- pgm.definedFunctions
body <- fd.body
} {
- val (res, scope, _) = toFunction(body)(State(fd, Set()))
+ val (res, scope, _) = toFunction(body)(State(fd, Set(), Map()))
fd.body = Some(scope(res))
}
}
- case class State(parent: FunDef, varsInScope: Set[Identifier]) {
+ /* varsInScope refers to variable declared in the same level scope.
+ Typically, when entering a nested function body, the scope should be
+ reset to empty */
+ private case class State(
+ parent: FunDef,
+ varsInScope: Set[Identifier],
+ funDefsMapping: Map[FunDef, (FunDef, List[Identifier])]
+ ) {
def withVar(i: Identifier) = copy(varsInScope = varsInScope + i)
+ def withFunDef(fd: FunDef, nfd: FunDef, ids: List[Identifier]) =
+ copy(funDefsMapping = funDefsMapping + (fd -> (nfd, ids)))
}
//return a "scope" consisting of purely functional code that defines potentially needed
@@ -119,6 +129,7 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
(resId.toVariable, scope, scrutFun ++ modifiedVars.zip(freshIds).toMap)
case wh@While(cond, body) =>
+ //TODO: rewrite by re-using the nested function transformation code
val (condRes, condScope, condFun) = toFunction(cond)
val (_, bodyScope, bodyFun) = toFunction(body)
val condBodyFun = condFun ++ bodyFun
@@ -218,14 +229,115 @@ object ImperativeCodeElimination extends UnitPhase[Program] {
bindFun ++ bodyFun
)
+ //a function invocation can update variables in scope.
+ case fi@FunctionInvocation(tfd, args) =>
+
+
+ val (recArgs, argScope, argFun) = args.foldRight((Seq[Expr](), (body: Expr) => body, Map[Identifier, Identifier]()))((arg, acc) => {
+ val (accArgs, accScope, accFun) = acc
+ val (argVal, argScope, argFun) = toFunction(arg)
+ val newScope = (body: Expr) => argScope(replaceNames(argFun, accScope(body)))
+ (argVal +: accArgs, newScope, argFun ++ accFun)
+ })
+
+ val fd = tfd.fd
+ state.funDefsMapping.get(fd) match {
+ case Some((newFd, modifiedVars)) => {
+ val newInvoc = FunctionInvocation(newFd.typed, recArgs ++ modifiedVars.map(id => id.toVariable)).setPos(fi)
+ val freshNames = modifiedVars.map(id => id.freshen)
+ val tmpTuple = FreshIdentifier("t", newFd.returnType)
+
+ val scope = (body: Expr) => {
+ argScope(Let(tmpTuple, newInvoc,
+ freshNames.zipWithIndex.foldRight(body)((p, b) =>
+ Let(p._1, TupleSelect(tmpTuple.toVariable, p._2 + 2), b))
+ ))
+ }
+ val newMap = argFun ++ modifiedVars.zip(freshNames).toMap
+
+ (TupleSelect(tmpTuple.toVariable, 1), scope, newMap)
+ }
+ case None =>
+ (FunctionInvocation(tfd, recArgs).copiedFrom(fi), argScope, argFun)
+ }
+
+
case LetDef(fd, b) =>
- //Recall that here the nested function should not access mutable variables from an outside scope
- fd.body.foreach { bd =>
- val (fdRes, fdScope, _) = toFunction(bd)
- fd.body = Some(fdScope(fdRes))
+
+ def fdWithoutSideEffects = {
+ fd.body.foreach { bd =>
+ val (fdRes, fdScope, _) = toFunction(bd)
+ fd.body = Some(fdScope(fdRes))
+ }
+ val (bodyRes, bodyScope, bodyFun) = toFunction(b)
+ (bodyRes, (b2: Expr) => LetDef(fd, bodyScope(b2)).setPos(fd).copiedFrom(expr), bodyFun)
+ }
+
+ fd.body match {
+ case Some(bd) => {
+
+ val modifiedVars: List[Identifier] =
+ collect[Identifier]({
+ case Assignment(v, _) => Set(v)
+ case _ => Set()
+ })(bd).intersect(state.varsInScope).toList
+
+ if(modifiedVars.isEmpty) fdWithoutSideEffects else {
+
+ val freshNames: List[Identifier] = modifiedVars.map(id => id.freshen)
+
+ val newParams: Seq[ValDef] = fd.params ++ freshNames.map(n => ValDef(n))
+ val freshVarDecls: List[Identifier] = freshNames.map(id => id.freshen)
+
+ val rewritingMap: Map[Identifier, Identifier] =
+ modifiedVars.zip(freshVarDecls).toMap
+ val freshBody =
+ preMap({
+ case Assignment(v, e) => rewritingMap.get(v).map(nv => Assignment(nv, e))
+ case Variable(id) => rewritingMap.get(id).map(nid => Variable(nid))
+ case _ => None
+ })(bd)
+ val wrappedBody = freshNames.zip(freshVarDecls).foldLeft(freshBody)((body, p) => {
+ LetVar(p._2, Variable(p._1), body)
+ })
+
+ val newReturnType = TupleType(fd.returnType :: modifiedVars.map(_.getType))
+
+ val newFd = new FunDef(fd.id.freshen, fd.tparams, newParams, newReturnType).setPos(fd)
+
+ val (fdRes, fdScope, fdFun) =
+ toFunction(wrappedBody)(
+ State(state.parent, Set(),
+ state.funDefsMapping + (fd -> ((newFd, freshVarDecls))))
+ )
+ val newRes = Tuple(fdRes :: freshVarDecls.map(vd => fdFun(vd).toVariable))
+ val newBody = fdScope(newRes)
+
+ newFd.body = Some(newBody)
+ newFd.precondition = fd.precondition.map(prec => {
+ replace(modifiedVars.zip(freshNames).map(p => (p._1.toVariable, p._2.toVariable)).toMap, prec)
+ })
+ newFd.postcondition = fd.postcondition.map(post => {
+ val Lambda(Seq(res), postBody) = post
+ val newRes = ValDef(FreshIdentifier(res.id.name, newFd.returnType))
+
+ val newBody =
+ replace(
+ modifiedVars.zipWithIndex.map{ case (v, i) =>
+ (v.toVariable, TupleSelect(newRes.toVariable, i+2)): (Expr, Expr)}.toMap ++
+ modifiedVars.zip(freshNames).map{ case (ov, nv) =>
+ (Old(ov), nv.toVariable)}.toMap +
+ (res.toVariable -> TupleSelect(newRes.toVariable, 1)),
+ postBody)
+ Lambda(Seq(newRes), newBody).setPos(post)
+ })
+
+ val (bodyRes, bodyScope, bodyFun) = toFunction(b)(state.withFunDef(fd, newFd, modifiedVars))
+ (bodyRes, (b2: Expr) => LetDef(newFd, bodyScope(b2)).copiedFrom(expr), bodyFun)
+ }
+ }
+ case None => fdWithoutSideEffects
}
- val (bodyRes, bodyScope, bodyFun) = toFunction(b)
- (bodyRes, (b2: Expr) => LetDef(fd, bodyScope(b2)).copiedFrom(expr), bodyFun)
case c @ Choose(b) =>
//Recall that Choose cannot mutate variables from the scope
diff --git a/src/test/resources/regression/verification/xlang/invalid/NestedFunState1.scala b/src/test/resources/regression/verification/xlang/invalid/NestedFunState1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9372ea742a278a3da3d476dca57e52c55c09b978
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/NestedFunState1.scala
@@ -0,0 +1,20 @@
+object NestedFunState1 {
+
+ def simpleSideEffect(n: BigInt): BigInt = {
+ require(n > 0)
+
+ var a = BigInt(0)
+
+ def incA(prevA: BigInt): Unit = {
+ require(prevA == a)
+ a += 1
+ } ensuring(_ => a == prevA + 1)
+
+ incA(a)
+ incA(a)
+ incA(a)
+ incA(a)
+ a
+ } ensuring(_ == 5)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/NestedFunState2.scala b/src/test/resources/regression/verification/xlang/invalid/NestedFunState2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..68769df28353c9defa6d33000bb8ae4de21c7ace
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/NestedFunState2.scala
@@ -0,0 +1,23 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+object NestedFunState2 {
+
+ def sum(n: BigInt): BigInt = {
+ require(n > 0)
+ var i = BigInt(0)
+ var res = BigInt(0)
+
+ def iter(): Unit = {
+ require(res >= i && i >= 0)
+ if(i < n) {
+ i += 1
+ res += i
+ iter()
+ }
+ }
+
+ iter()
+ res
+ } ensuring(_ < 0)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/ArrayNested1.scala b/src/test/resources/regression/verification/xlang/valid/ArrayNested1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..196a6442bd544a3981e6a7de7e923e040cadd32d
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ArrayNested1.scala
@@ -0,0 +1,19 @@
+import leon.lang._
+
+object ArrayNested1 {
+
+ def test(): Int = {
+
+ var a = Array(1, 2, 0)
+
+ def nested(): Unit = {
+ require(a.length == 3)
+ a = a.updated(1, 5)
+ }
+
+ nested()
+ a(1)
+
+ } ensuring(_ == 5)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/ArrayNested2.scala b/src/test/resources/regression/verification/xlang/valid/ArrayNested2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a8935ab8c1d4eec6980b85f171e695071f2a9442
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/ArrayNested2.scala
@@ -0,0 +1,19 @@
+import leon.lang._
+
+object ArrayNested2 {
+
+ def test(): Int = {
+
+ val a = Array(1, 2, 0)
+
+ def nested(): Unit = {
+ require(a.length == 3)
+ a(2) = 5
+ }
+
+ nested()
+ a(2)
+
+ } ensuring(_ == 5)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/FunInvocEvaluationOrder1.scala b/src/test/resources/regression/verification/xlang/valid/FunInvocEvaluationOrder1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..8ef668a2afeb61a6b305831358a65e675bf670ed
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/FunInvocEvaluationOrder1.scala
@@ -0,0 +1,22 @@
+object FunInvocEvaluationOrder1 {
+
+ def test(): Int = {
+
+ var res = 10
+ justAddingStuff({
+ res += 1
+ res
+ }, {
+ res *= 2
+ res
+ }, {
+ res += 10
+ res
+ })
+
+ res
+ } ensuring(_ == 32)
+
+ def justAddingStuff(x: Int, y: Int, z: Int): Int = x + y + z
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/FunInvocEvaluationOrder2.scala b/src/test/resources/regression/verification/xlang/valid/FunInvocEvaluationOrder2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..12090f0f3fad0a5fcf2451e30fdb6f25bb09c590
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/FunInvocEvaluationOrder2.scala
@@ -0,0 +1,17 @@
+object FunInvocEvaluationOrder2 {
+
+ def leftToRight(n: BigInt): BigInt = {
+ require(n > 0)
+
+ var a = BigInt(0)
+
+ def nested(x: BigInt, y: BigInt): BigInt = {
+ require(y >= x)
+ x + y
+ }
+
+ nested({a += 10; a}, {a *= 2; a})
+
+ } ensuring(_ == 30)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/FunInvocEvaluationOrder3.scala b/src/test/resources/regression/verification/xlang/valid/FunInvocEvaluationOrder3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f263529653486ee5477b9fd1934760bcdc737d15
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/FunInvocEvaluationOrder3.scala
@@ -0,0 +1,17 @@
+object FunInvocEvaluationOrder3 {
+
+ def leftToRight(n: BigInt): BigInt = {
+ require(n > 0)
+
+ var a = BigInt(0)
+
+ def nested(x: BigInt, y: BigInt): Unit = {
+ a = x + y
+ }
+
+ nested({a += 10; a}, {a *= 2; a})
+ a
+
+ } ensuring(_ == 30)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/NestedFunState1.scala b/src/test/resources/regression/verification/xlang/valid/NestedFunState1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1ec0266f846dd55cfa1a6274d5c6dc7dc67dd125
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/NestedFunState1.scala
@@ -0,0 +1,23 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+object NestedFunState1 {
+
+ def sum(n: BigInt): BigInt = {
+ require(n > 0)
+ var i = BigInt(0)
+ var res = BigInt(0)
+
+ def iter(): Unit = {
+ require(res >= i && i >= 0)
+ if(i < n) {
+ i += 1
+ res += i
+ iter()
+ }
+ } ensuring(_ => res >= n)
+
+ iter()
+ res
+ } ensuring(_ >= n)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/NestedFunState2.scala b/src/test/resources/regression/verification/xlang/valid/NestedFunState2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e48b1b959b3a83262329cf48c63370a2b591cd41
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/NestedFunState2.scala
@@ -0,0 +1,19 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+
+object NestedFunState2 {
+
+ def countConst(): Int = {
+
+ var counter = 0
+
+ def inc(): Unit = {
+ counter += 1
+ }
+
+ inc()
+ inc()
+ inc()
+ counter
+ } ensuring(_ == 3)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/NestedFunState3.scala b/src/test/resources/regression/verification/xlang/valid/NestedFunState3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..650f5987dcd352a3f5c47d41c684e94d4b9be20c
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/NestedFunState3.scala
@@ -0,0 +1,25 @@
+/* Copyright 2009-2015 EPFL, Lausanne */
+import leon.lang._
+
+object NestedFunState3 {
+
+
+ def counterN(n: Int): Int = {
+ require(n > 0)
+
+ var counter = 0
+
+ def inc(): Unit = {
+ counter += 1
+ }
+
+ var i = 0
+ (while(i < n) {
+ inc()
+ i += 1
+ }) invariant(i >= 0 && counter == i && i <= n)
+
+ counter
+ } ensuring(_ == n)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/NestedFunState4.scala b/src/test/resources/regression/verification/xlang/valid/NestedFunState4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9f4fb2621f60c60da3a677dc732e6c93f4d8ae72
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/NestedFunState4.scala
@@ -0,0 +1,38 @@
+import leon.lang._
+
+object NestedFunState4 {
+
+ def deep(n: BigInt): BigInt = {
+ require(n > 0)
+
+ var a = BigInt(0)
+
+ def iter(): Unit = {
+ require(a >= 0)
+
+ var b = BigInt(0)
+
+ def nestedIter(): Unit = {
+ b += 1
+ }
+
+ var i = BigInt(0)
+ (while(i < n) {
+ i += 1
+ nestedIter()
+ }) invariant(i >= 0 && i <= n && b == i)
+
+ a += b
+
+ } ensuring(_ => a >= n)
+
+ var i = BigInt(0)
+ (while(i < n) {
+ i += 1
+ iter()
+ }) invariant(i >= 0 && i <= n && a >= i)
+
+ a
+ } ensuring(_ >= n)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/NestedFunState5.scala b/src/test/resources/regression/verification/xlang/valid/NestedFunState5.scala
new file mode 100644
index 0000000000000000000000000000000000000000..13f3cf47cd0ee6c831f12877493cbfe6c7edea5a
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/NestedFunState5.scala
@@ -0,0 +1,29 @@
+import leon.lang._
+
+object NestedFunState5 {
+
+ def deep(n: BigInt): BigInt = {
+ require(n > 0)
+
+ var a = BigInt(0)
+
+ def iter(prevA: BigInt): Unit = {
+ require(prevA == a)
+ def nestedIter(): Unit = {
+ a += 1
+ }
+
+ nestedIter()
+ nestedIter()
+
+ } ensuring(_ => a == prevA + 2)
+
+ var i = BigInt(0)
+ (while(i < n) {
+ i += 1
+ iter(a)
+ }) invariant(i >= 0 && i <= n && a >= 2*i)
+
+ a
+ } ensuring(_ >= 2*n)
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/NestedFunState6.scala b/src/test/resources/regression/verification/xlang/valid/NestedFunState6.scala
new file mode 100644
index 0000000000000000000000000000000000000000..cea0f2e1900a00bc803df4107b46dd62cf082c68
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/NestedFunState6.scala
@@ -0,0 +1,20 @@
+object NestedFunState6 {
+
+ def simpleSideEffect(n: BigInt): BigInt = {
+ require(n > 0)
+
+ var a = BigInt(0)
+
+ def incA(prevA: BigInt): Unit = {
+ require(prevA == a)
+ a += 1
+ } ensuring(_ => a == prevA + 1)
+
+ incA(a)
+ incA(a)
+ incA(a)
+ incA(a)
+ a
+ } ensuring(_ == 4)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/NestedFunState7.scala b/src/test/resources/regression/verification/xlang/valid/NestedFunState7.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ff2418a0c972add2d48c08f6319905f35d0493c2
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/NestedFunState7.scala
@@ -0,0 +1,27 @@
+import leon.lang._
+
+object NestedFunState7 {
+
+ def test(x: BigInt): BigInt = {
+
+ var a = BigInt(0)
+
+ def defCase(): Unit = {
+ a = 100
+ }
+
+ if(x >= 0) {
+ a = 2*x
+ if(a < 100) {
+ a = 100 - a
+ } else {
+ defCase()
+ }
+ } else {
+ defCase()
+ }
+
+ a
+ } ensuring(res => res >= 0 && res <= 100)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/NestedOld1.scala b/src/test/resources/regression/verification/xlang/valid/NestedOld1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..903dfd63aca5105c9366c459552865646139033e
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/NestedOld1.scala
@@ -0,0 +1,16 @@
+import leon.lang._
+
+object NestedOld1 {
+
+ def test(): Int = {
+ var counter = 0
+
+ def inc(): Unit = {
+ counter += 1
+ } ensuring(_ => counter == old(counter) + 1)
+
+ inc()
+ counter
+ } ensuring(_ == 1)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/NestedOld2.scala b/src/test/resources/regression/verification/xlang/valid/NestedOld2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..fe6143ecf623c295251ca2b9d75d6474d422fd4f
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/NestedOld2.scala
@@ -0,0 +1,24 @@
+import leon.lang._
+
+object NestedOld2 {
+
+ def test(): Int = {
+ var counterPrev = 0
+ var counterNext = 1
+
+ def step(): Unit = {
+ require(counterNext == counterPrev + 1)
+ counterPrev = counterNext
+ counterNext = counterNext+1
+ } ensuring(_ => {
+ counterPrev == old(counterNext) &&
+ counterNext == old(counterNext) + 1 &&
+ counterPrev == old(counterPrev) + 1
+ })
+
+ step()
+ step()
+ counterNext
+ } ensuring(_ == 3)
+
+}