diff --git a/src/main/scala/leon/Settings.scala b/src/main/scala/leon/Settings.scala
index 9aa0c57ac2371bdaa01df63543a6947312c23a75..3aba078e9d2b0ed00171c5b000fd5c301936a52a 100644
--- a/src/main/scala/leon/Settings.scala
+++ b/src/main/scala/leon/Settings.scala
@@ -5,7 +5,7 @@ package leon
object Settings {
lazy val reporter: Reporter = new DefaultReporter
- var showIDs: Boolean = false
+ var showIDs: Boolean = true
var silentlyTolerateNonPureBodies: Boolean = false
}
diff --git a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
index c9c69511ef57c5ab07d26d75e89c34287e244c6f..bc246e2e68827c66d7e2abe5efc5d0977316d3ac 100644
--- a/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
+++ b/src/main/scala/leon/solvers/z3/FairZ3Solver.scala
@@ -291,6 +291,7 @@ class FairZ3Solver(context : LeonContext)
val newClauses = unrollingBank.scanForNewTemplates(expression)
for (cl <- newClauses) {
+ println("transforming to z3: " + cl)
solver.assertCnstr(z3.mkImplies(guard, toZ3Formula(cl).get))
}
}
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index d4a2b71b7ca348d0797b771e873d84ec90744fdc..2785fae3eeff31d90625cf6be58f6c93ddd30800 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -21,6 +21,7 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
)
def run(ctx: LeonContext)(program: Program) : VerificationReport = {
+ println(program)
val functionsToAnalyse : MutableSet[String] = MutableSet.empty
for(opt <- ctx.options) opt match {
diff --git a/src/main/scala/leon/xlang/ArrayTransformation.scala b/src/main/scala/leon/xlang/ArrayTransformation.scala
index 1d7a20dcf3801fb957964b713150394148208f10..880e870f52134dccd7b7ddd3397fe86b01b3cf53 100644
--- a/src/main/scala/leon/xlang/ArrayTransformation.scala
+++ b/src/main/scala/leon/xlang/ArrayTransformation.scala
@@ -14,8 +14,11 @@ object ArrayTransformation extends TransformationPhase {
val name = "Array Transformation"
val description = "Add bound checking for array access and remove array update with side effect"
+ private var id2FreshId = Map[Identifier, Identifier]()
+
def apply(ctx: LeonContext, pgm: Program): Program = {
+ id2FreshId = Map()
val allFuns = pgm.definedFunctions
allFuns.foreach(fd => {
id2FreshId = Map()
@@ -26,7 +29,6 @@ object ArrayTransformation extends TransformationPhase {
pgm
}
- private var id2FreshId = Map[Identifier, Identifier]()
def transform(expr: Expr): Expr = expr match {
case sel@ArraySelect(a, i) => {
diff --git a/src/main/scala/leon/xlang/FunctionClosure.scala b/src/main/scala/leon/xlang/FunctionClosure.scala
index 6c5000849510be1647da1ccf0ee2786037439b41..47e0cbeede0090b6afc8e784ed127943d7e12177 100644
--- a/src/main/scala/leon/xlang/FunctionClosure.scala
+++ b/src/main/scala/leon/xlang/FunctionClosure.scala
@@ -21,14 +21,20 @@ object FunctionClosure extends TransformationPhase{
private var topLevelFuns: Set[FunDef] = Set()
def apply(ctx: LeonContext, program: Program): Program = {
- newFunDefs = Map()
+
+ pathConstraints = Nil
+ enclosingLets = Nil
+ newFunDefs = Map()
+ topLevelFuns = Set()
+
val funDefs = program.definedFunctions
funDefs.foreach(fd => {
pathConstraints = fd.precondition.toList
fd.body = fd.body.map(b => functionClosure(b, fd.args.map(_.id).toSet, Map(), Map()))
})
val Program(id, ObjectDef(objId, defs, invariants)) = program
- Program(id, ObjectDef(objId, defs ++ topLevelFuns, invariants))
+ val res = Program(id, ObjectDef(objId, defs ++ topLevelFuns, invariants))
+ res
}
private def functionClosure(expr: Expr, bindedVars: Set[Identifier], id2freshId: Map[Identifier, Identifier], fd2FreshFd: Map[FunDef, (FunDef, Seq[Variable])]): Expr = expr match {
diff --git a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
index c66a7094956727787e6ab686ffe51ba50810ac98..330e44c138f47b53370c2637cedc1df8d0997532 100644
--- a/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
+++ b/src/main/scala/leon/xlang/ImperativeCodeElimination.scala
@@ -19,8 +19,12 @@ object ImperativeCodeElimination extends TransformationPhase {
private var parent: FunDef = null //the enclosing fundef
def apply(ctx: LeonContext, pgm: Program): Program = {
+ varInScope = Set()
+ parent = null
+
val allFuns = pgm.definedFunctions
allFuns.foreach(fd => fd.body.map(body => {
+ println("processing fun: " + fd)
parent = fd
val (res, scope, _) = toFunction(body)
fd.body = Some(scope(res))
@@ -35,6 +39,7 @@ object ImperativeCodeElimination extends TransformationPhase {
private def toFunction(expr: Expr): (Expr, Expr => Expr, Map[Identifier, Identifier]) = {
val res = expr match {
case LetVar(id, e, b) => {
+ println("in letvar with id: " + id)
val newId = FreshIdentifier(id.name).setType(id.getType)
val (rhsVal, rhsScope, rhsFun) = toFunction(e)
varInScope += id
diff --git a/src/main/scala/leon/xlang/Trees.scala b/src/main/scala/leon/xlang/Trees.scala
index 8995aba734bd2050b913b74f28513e858f5422ac..31c717784281d5bf556580d6c9cf77b9a23cbec1 100644
--- a/src/main/scala/leon/xlang/Trees.scala
+++ b/src/main/scala/leon/xlang/Trees.scala
@@ -260,39 +260,51 @@ object Trees {
(fd.precondition, fd.postcondition) match {
case (None, None) =>
Some((Seq(b, body), (as: Seq[Expr]) => {
- val nfd = new FunDef(fd.id, fd.returnType, fd.args)
- nfd.fromLoop = fd.fromLoop
- nfd.parent = fd.parent
- nfd.body = Some(as(0))
- LetDef(nfd, as(1))
+ //val nfd = new FunDef(fd.id, fd.returnType, fd.args)
+ //nfd.fromLoop = fd.fromLoop
+ //nfd.parent = fd.parent
+ //nfd.body = Some(as(0))
+ //LetDef(nfd, as(1))
+ fd.body = Some(as(0))
+ LetDef(fd, as(1))
}))
case (Some(pre), None) =>
Some((Seq(b, body, pre), (as: Seq[Expr]) => {
- val nfd = new FunDef(fd.id, fd.returnType, fd.args)
- nfd.fromLoop = fd.fromLoop
- nfd.parent = fd.parent
- nfd.body = Some(as(0))
- nfd.precondition = Some(as(2))
- LetDef(nfd, as(1))
+ //val nfd = new FunDef(fd.id, fd.returnType, fd.args)
+ //nfd.fromLoop = fd.fromLoop
+ //nfd.parent = fd.parent
+ //nfd.body = Some(as(0))
+ //nfd.precondition = Some(as(2))
+ //LetDef(nfd, as(1))
+ fd.body = Some(as(0))
+ fd.precondition = Some(as(2))
+ LetDef(fd, as(1))
}))
case (None, Some(post)) =>
Some((Seq(b, body, post), (as: Seq[Expr]) => {
- val nfd = new FunDef(fd.id, fd.returnType, fd.args)
- nfd.fromLoop = fd.fromLoop
- nfd.parent = fd.parent
- nfd.body = Some(as(0))
- nfd.postcondition = Some(as(2))
- LetDef(nfd, as(1))
+ //val nfd = new FunDef(fd.id, fd.returnType, fd.args)
+ //nfd.fromLoop = fd.fromLoop
+ //nfd.parent = fd.parent
+ //nfd.body = Some(as(0))
+ //nfd.postcondition = Some(as(2))
+ //LetDef(nfd, as(1))
+ fd.body = Some(as(0))
+ fd.postcondition = Some(as(2))
+ LetDef(fd, as(1))
}))
case (Some(pre), Some(post)) =>
Some((Seq(b, body, pre, post), (as: Seq[Expr]) => {
- val nfd = new FunDef(fd.id, fd.returnType, fd.args)
- nfd.fromLoop = fd.fromLoop
- nfd.parent = fd.parent
- nfd.body = Some(as(0))
- nfd.precondition = Some(as(2))
- nfd.postcondition = Some(as(3))
- LetDef(nfd, as(1))
+ //val nfd = new FunDef(fd.id, fd.returnType, fd.args)
+ //nfd.fromLoop = fd.fromLoop
+ //nfd.parent = fd.parent
+ //nfd.body = Some(as(0))
+ //nfd.precondition = Some(as(2))
+ //nfd.postcondition = Some(as(3))
+ //LetDef(nfd, as(1))
+ fd.body = Some(as(0))
+ fd.precondition = Some(as(2))
+ fd.postcondition = Some(as(3))
+ LetDef(fd, as(1))
}))
}
@@ -300,35 +312,43 @@ object Trees {
(fd.precondition, fd.postcondition) match {
case (None, None) =>
Some((Seq(body), (as: Seq[Expr]) => {
- val nfd = new FunDef(fd.id, fd.returnType, fd.args)
- nfd.fromLoop = fd.fromLoop
- nfd.parent = fd.parent
- LetDef(nfd, as(0))
+ //val nfd = new FunDef(fd.id, fd.returnType, fd.args)
+ //nfd.fromLoop = fd.fromLoop
+ //nfd.parent = fd.parent
+ //LetDef(nfd, as(0))
+ LetDef(fd, as(0))
}))
case (Some(pre), None) =>
Some((Seq(body, pre), (as: Seq[Expr]) => {
- val nfd = new FunDef(fd.id, fd.returnType, fd.args)
- nfd.fromLoop = fd.fromLoop
- nfd.parent = fd.parent
- nfd.precondition = Some(as(1))
- LetDef(nfd, as(0))
+ //val nfd = new FunDef(fd.id, fd.returnType, fd.args)
+ //nfd.fromLoop = fd.fromLoop
+ //nfd.parent = fd.parent
+ //nfd.precondition = Some(as(1))
+ //LetDef(nfd, as(0))
+ fd.precondition = Some(as(1))
+ LetDef(fd, as(0))
}))
case (None, Some(post)) =>
Some((Seq(body, post), (as: Seq[Expr]) => {
- val nfd = new FunDef(fd.id, fd.returnType, fd.args)
- nfd.fromLoop = fd.fromLoop
- nfd.parent = fd.parent
- nfd.postcondition = Some(as(1))
- LetDef(nfd, as(0))
+ //val nfd = new FunDef(fd.id, fd.returnType, fd.args)
+ //nfd.fromLoop = fd.fromLoop
+ //nfd.parent = fd.parent
+ //nfd.postcondition = Some(as(1))
+ //LetDef(nfd, as(0))
+ fd.postcondition = Some(as(1))
+ LetDef(fd, as(0))
}))
case (Some(pre), Some(post)) =>
Some((Seq(body, pre, post), (as: Seq[Expr]) => {
- val nfd = new FunDef(fd.id, fd.returnType, fd.args)
- nfd.fromLoop = fd.fromLoop
- nfd.parent = fd.parent
- nfd.precondition = Some(as(1))
- nfd.postcondition = Some(as(2))
- LetDef(nfd, as(0))
+ //val nfd = new FunDef(fd.id, fd.returnType, fd.args)
+ //nfd.fromLoop = fd.fromLoop
+ //nfd.parent = fd.parent
+ //nfd.precondition = Some(as(1))
+ //nfd.postcondition = Some(as(2))
+ //LetDef(nfd, as(0))
+ fd.precondition = Some(as(1))
+ fd.postcondition = Some(as(2))
+ LetDef(fd, as(0))
}))
}
}
diff --git a/src/test/resources/regression/verification/xlang/invalid/Array1.scala b/src/test/resources/regression/verification/xlang/invalid/Array1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a8451250c8f9e9c95684b4ea10490aced2a23f6e
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/Array1.scala
@@ -0,0 +1,9 @@
+object Array1 {
+
+ def foo(): Int = {
+ val a = Array.fill(5)(0)
+ a(2) = 3
+ a(2)
+ } ensuring(_ == 0)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/Array2.scala b/src/test/resources/regression/verification/xlang/invalid/Array2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..54ab5e3c27918596af58c427fabedd2016a33db9
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/Array2.scala
@@ -0,0 +1,9 @@
+object Array2 {
+
+ def foo(): Int = {
+ val a = Array.fill(5)(0)
+ a(2) = 3
+ a.length
+ } ensuring(_ == 4)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/Array3.scala b/src/test/resources/regression/verification/xlang/invalid/Array3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0c1bb76fdce099bd095c59d8c03fe8e6508a9776
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/Array3.scala
@@ -0,0 +1,16 @@
+import leon.Utils._
+
+object Array3 {
+
+ def foo(): Int = {
+ val a = Array.fill(5)(3)
+ var i = 0
+ var sum = 0
+ (while(i <= a.length) {
+ sum = sum + a(i)
+ i = i + 1
+ }) invariant(i >= 0)
+ sum
+ } ensuring(_ == 15)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/Array4.scala b/src/test/resources/regression/verification/xlang/invalid/Array4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5b5e7406165ad214a7d5d5fffd85d2d4fce226e0
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/Array4.scala
@@ -0,0 +1,9 @@
+import leon.Utils._
+
+object Array4 {
+
+ def foo(a: Array[Int]): Int = {
+ a(2)
+ }
+
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/Array5.scala b/src/test/resources/regression/verification/xlang/invalid/Array5.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ecb00334971f3ecf19f3b6e6f9c25a5082f2d2d7
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/Array5.scala
@@ -0,0 +1,10 @@
+import leon.Utils._
+
+object Array4 {
+
+ def foo(a: Array[Int]): Int = {
+ require(a.length > 2)
+ a(2)
+ } ensuring(_ == 0)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/Epsilon1.scala b/src/test/resources/regression/verification/xlang/invalid/Epsilon1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..c3c0a48be96f594fe725518a7289333bb587ef40
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/Epsilon1.scala
@@ -0,0 +1,12 @@
+import leon.Utils._
+
+object Epsilon1 {
+
+ def rand2(x: Int): Int = epsilon((y: Int) => true)
+
+ //this should not hold
+ def property2(x: Int): Boolean = {
+ rand2(x) == rand2(x+1)
+ } holds
+
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/Epsilon2.scala b/src/test/resources/regression/verification/xlang/invalid/Epsilon2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..20699fc427e7dce9025e578767f5364ae19aaf88
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/Epsilon2.scala
@@ -0,0 +1,11 @@
+import leon.Utils._
+
+object Epsilon1 {
+
+ def rand3(x: Int): Int = epsilon((y: Int) => x == x)
+
+ //this should not hold
+ def property3(x: Int): Boolean = {
+ rand3(x) == rand3(x+1)
+ } holds
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/Epsilon3.scala b/src/test/resources/regression/verification/xlang/invalid/Epsilon3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5ff47b6d638cc7270640f0bba95f4cd572f8201a
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/Epsilon3.scala
@@ -0,0 +1,9 @@
+import leon.Utils._
+
+object Epsilon3 {
+
+ def posWrong(): Int = {
+ epsilon((y: Int) => y >= 0)
+ } ensuring(_ > 0)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/Epsilon4.scala b/src/test/resources/regression/verification/xlang/invalid/Epsilon4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..6619e59d6f9d9721c4bc7587b47dac79f48bf437
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/Epsilon4.scala
@@ -0,0 +1,27 @@
+import leon.Utils._
+
+object Epsilon4 {
+
+ sealed abstract class MyList
+ case class MyCons(head: Int, tail: MyList) extends MyList
+ case class MyNil() extends MyList
+
+ def size(lst: MyList): Int = (lst match {
+ case MyNil() => 0
+ case MyCons(_, xs) => 1 + size(xs)
+ })
+
+ def toSet(lst: MyList): Set[Int] = lst match {
+ case MyCons(x, xs) => toSet(xs) ++ Set(x)
+ case MyNil() => Set[Int]()
+ }
+
+ def toList(set: Set[Int]): MyList = if(set == Set.empty[Int]) MyNil() else {
+ val elem = epsilon((x : Int) => set contains x)
+ MyCons(elem, toList(set -- Set[Int](elem)))
+ }
+
+
+ def wrongProperty0(lst: MyList): Boolean = (size(toList(toSet(lst))) == size(lst)) holds
+ //def wrongProperty1(lst: MyList): Boolean = (toList(toSet(lst)) == lst) holds
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/Epsilon5.scala b/src/test/resources/regression/verification/xlang/invalid/Epsilon5.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b96fa7564e5dba8a44aeb9d750034153b362ebfe
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/Epsilon5.scala
@@ -0,0 +1,9 @@
+import leon.Utils._
+
+object Epsilon5 {
+
+ def fooWrong(x: Int, y: Int): Int = {
+ epsilon((z: Int) => z >= x && z <= y)
+ } ensuring(_ > x)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/Epsilon6.scala b/src/test/resources/regression/verification/xlang/invalid/Epsilon6.scala
new file mode 100644
index 0000000000000000000000000000000000000000..bc5aca78c3818a94df43146aba16077ffab50a71
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/Epsilon6.scala
@@ -0,0 +1,9 @@
+import leon.Utils._
+
+object Epsilon6 {
+
+ def greaterWrong(x: Int): Int = {
+ epsilon((y: Int) => y >= x)
+ } ensuring(_ > x)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/IfExpr2.scala b/src/test/resources/regression/verification/xlang/invalid/IfExpr2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1284904b5c7dfda8f601e130b6346680538aa99a
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/IfExpr2.scala
@@ -0,0 +1,14 @@
+object IfExpr2 {
+
+ def foo(): Int = {
+ var a = 1
+ var b = 2
+ if(a < b) {
+ a = a + 3
+ b = b + 2
+ a = a + b
+ }
+ a
+ } ensuring(_ == 0)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/MyTuple1.scala b/src/test/resources/regression/verification/xlang/invalid/MyTuple1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f2b06b5b28e405bfb2487875c8e964b8f212792c
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/MyTuple1.scala
@@ -0,0 +1,11 @@
+object MyTuple1 {
+
+ def foo(): Int = {
+ val t = (1, true, 3)
+ val a1 = t._1
+ val a2 = t._2
+ val a3 = t._3
+ a3
+ } ensuring( _ == 1)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/MyTuple2.scala b/src/test/resources/regression/verification/xlang/invalid/MyTuple2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..22b62dc75b75b3193cb2f304118a89afbc90eb91
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/MyTuple2.scala
@@ -0,0 +1,14 @@
+object MyTuple2 {
+
+ abstract class A
+ case class B(i: Int) extends A
+ case class C(a: A) extends A
+
+ def foo(): Int = {
+ val t = (B(2), C(B(3)))
+ t match {
+ case (B(x), C(y)) => x
+ }
+ } ensuring( _ == 3)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/MyTuple3.scala b/src/test/resources/regression/verification/xlang/invalid/MyTuple3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..da9f85b16a48f0676d1f15741ad47536e14b57ab
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/MyTuple3.scala
@@ -0,0 +1,7 @@
+object MyTuple3 {
+
+ def foo(t: (Int, Int)): (Int, Int) = {
+ t
+ } ensuring(res => res._1 > 0 && res._2 > 1)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/invalid/Unit1.scala b/src/test/resources/regression/verification/xlang/invalid/Unit1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..789a8f058cd8145a0dd3b7bb0d72d44fb92ee94e
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/invalid/Unit1.scala
@@ -0,0 +1,7 @@
+object Unit1 {
+
+ def foo(u: Unit): Unit = ({
+ u
+ }) ensuring(_ != ())
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Array1.scala b/src/test/resources/regression/verification/xlang/valid/Array1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..3815f03443448a28fb60475b49c09c981a1377f9
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Array1.scala
@@ -0,0 +1,9 @@
+object Array1 {
+
+ def foo(): Int = {
+ val a = Array.fill(5)(0)
+ a(2) = 3
+ a(2)
+ } ensuring(_ == 3)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Array10.scala b/src/test/resources/regression/verification/xlang/valid/Array10.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ebb60ad6e0ba7556c55c74e1b1b624e6c34b4311
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Array10.scala
@@ -0,0 +1,9 @@
+object Array10 {
+
+ def foo(a: Array[Int]): Int = {
+ require(a.length > 0)
+ val b = a.clone
+ b(0)
+ } ensuring(res => res == a(0))
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Array2.scala b/src/test/resources/regression/verification/xlang/valid/Array2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4f149a9305cb4b53a4a9353b82e25468c898bdc8
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Array2.scala
@@ -0,0 +1,9 @@
+object Array2 {
+
+ def foo(): Int = {
+ val a = Array.fill(5)(0)
+ a(2) = 3
+ a.length
+ } ensuring(_ == 5)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Array3.scala b/src/test/resources/regression/verification/xlang/valid/Array3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..bbb1845b80c0ca747cb0c830828bacdc9668943f
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Array3.scala
@@ -0,0 +1,16 @@
+import leon.Utils._
+
+object Array3 {
+
+ def foo(): Int = {
+ val a = Array.fill(5)(3)
+ var i = 0
+ var sum = 0
+ (while(i < a.length) {
+ sum = sum + a(i)
+ i = i + 1
+ }) invariant(i >= 0)
+ sum
+ } ensuring(_ == 15)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Array4.scala b/src/test/resources/regression/verification/xlang/valid/Array4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..fd76e02faa83f8fd1bda5fef7c91e7df7fc29864
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Array4.scala
@@ -0,0 +1,15 @@
+import leon.Utils._
+
+object Array4 {
+
+ def foo(a: Array[Int]): Int = {
+ var i = 0
+ var sum = 0
+ (while(i < a.length) {
+ sum = sum + a(i)
+ i = i + 1
+ }) invariant(i >= 0)
+ sum
+ }
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Array5.scala b/src/test/resources/regression/verification/xlang/valid/Array5.scala
new file mode 100644
index 0000000000000000000000000000000000000000..14bed6eff332db69600353001488c46a3e56aa5d
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Array5.scala
@@ -0,0 +1,20 @@
+import leon.Utils._
+
+object Array5 {
+
+ def foo(a: Array[Int]): Int = {
+ var i = 0
+ var sum = 0
+ (while(i < a.length) {
+ sum = sum + a(i)
+ i = i + 1
+ }) invariant(i >= 0)
+ sum
+ }
+
+ def bar(): Int = {
+ val a = Array.fill(5)(5)
+ foo(a)
+ }
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Array6.scala b/src/test/resources/regression/verification/xlang/valid/Array6.scala
new file mode 100644
index 0000000000000000000000000000000000000000..bdd6b0c5d9bee06eec14b9f5917762c67af4751b
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Array6.scala
@@ -0,0 +1,15 @@
+import leon.Utils._
+
+object Array6 {
+
+ def foo(a: Array[Int]): Int = {
+ require(a.length > 2 && a(2) == 5)
+ a(2)
+ } ensuring(_ == 5)
+
+ def bar(): Int = {
+ val a = Array.fill(5)(5)
+ foo(a)
+ }
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Array7.scala b/src/test/resources/regression/verification/xlang/valid/Array7.scala
new file mode 100644
index 0000000000000000000000000000000000000000..55bbbb72908e2b192152162d82d2ed9fea67923b
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Array7.scala
@@ -0,0 +1,17 @@
+import leon.Utils._
+
+object Array7 {
+
+ def foo(a: Array[Int]): Array[Int] = {
+ require(a.length > 0)
+ val a2 = Array.fill(a.length)(0)
+ var i = 0
+ (while(i < a.length) {
+ a2(i) = a(i)
+ i = i + 1
+ }) invariant(a.length == a2.length && i >= 0 && (if(i > 0) a2(0) == a(0) else true))
+ a2
+ } ensuring(_(0) == a(0))
+
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Array8.scala b/src/test/resources/regression/verification/xlang/valid/Array8.scala
new file mode 100644
index 0000000000000000000000000000000000000000..270b181220b55af1588f63e7953221ae71f9bde3
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Array8.scala
@@ -0,0 +1,8 @@
+object Array8 {
+
+ def foo(a: Array[Int]): Array[Int] = {
+ require(a.length >= 2)
+ a.updated(1, 3)
+ } ensuring(res => res.length == a.length && res(1) == 3)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Array9.scala b/src/test/resources/regression/verification/xlang/valid/Array9.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f49333236abfaf63caa278405a89670b1c9c115d
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Array9.scala
@@ -0,0 +1,15 @@
+object Array9 {
+
+ def foo(i: Int): Array[Int] = {
+ require(i > 0)
+ val a = Array.fill(i)(0)
+ a
+ } ensuring(res => res.length == i)
+
+ def bar(i: Int): Int = {
+ require(i > 0)
+ val b = foo(i)
+ b(0)
+ }
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Assign1.scala b/src/test/resources/regression/verification/xlang/valid/Assign1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0506c6afb39b49ac5a15c77dc10ab60f54de9ee6
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Assign1.scala
@@ -0,0 +1,12 @@
+object Assign1 {
+
+ def foo(): Int = {
+ var a = 0
+ val tmp = a + 1
+ a = a + 2
+ a = a + tmp
+ a = a + 4
+ a
+ } ensuring(_ == 7)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Epsilon1.scala b/src/test/resources/regression/verification/xlang/valid/Epsilon1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2ae7201dd933e345fa71a6218b48599a61110f44
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Epsilon1.scala
@@ -0,0 +1,9 @@
+import leon.Utils._
+
+object Epsilon1 {
+
+ def greater(x: Int): Int = {
+ epsilon((y: Int) => y > x)
+ } ensuring(_ >= x)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Epsilon2.scala b/src/test/resources/regression/verification/xlang/valid/Epsilon2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..36e5268e2b1ccdbc710dc8d6410ce6968231c7d1
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Epsilon2.scala
@@ -0,0 +1,13 @@
+import leon.Utils._
+
+object Epsilon1 {
+
+ def rand(): Int = epsilon((x: Int) => true)
+
+ //this should hold, that is the expected semantic of our epsilon
+ def property1(): Boolean = {
+ rand() == rand()
+ } holds
+
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Epsilon3.scala b/src/test/resources/regression/verification/xlang/valid/Epsilon3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f652016d28976d0b7e110b009a0802a7aac10c99
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Epsilon3.scala
@@ -0,0 +1,9 @@
+import leon.Utils._
+
+object Epsilon3 {
+
+ def pos(): Int = {
+ epsilon((y: Int) => y > 0)
+ } ensuring(_ >= 0)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Epsilon4.scala b/src/test/resources/regression/verification/xlang/valid/Epsilon4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..174042863a690067fae5a2fd4aaf55f95bf29129
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Epsilon4.scala
@@ -0,0 +1,32 @@
+import leon.Utils._
+
+object Epsilon4 {
+
+ sealed abstract class MyList
+ case class MyCons(head: Int, tail: MyList) extends MyList
+ case class MyNil() extends MyList
+
+ def size(lst: MyList): Int = (lst match {
+ case MyNil() => 0
+ case MyCons(_, xs) => 1 + size(xs)
+ })
+
+ def toSet(lst: MyList): Set[Int] = lst match {
+ case MyCons(x, xs) => toSet(xs) ++ Set(x)
+ case MyNil() => Set[Int]()
+ }
+
+ def toList(set: Set[Int]): MyList = if(set == Set.empty[Int]) MyNil() else {
+ val elem = epsilon((x : Int) => set contains x)
+ MyCons(elem, toList(set -- Set[Int](elem)))
+ }
+
+ //timeout, but this probably means that it is valid as expected
+ //def property(lst: MyList): Boolean = (size(toList(toSet(lst))) <= size(lst)) holds
+
+ def propertyBase(lst: MyList): Boolean = ({
+ require(lst match { case MyNil() => true case _ => false})
+ size(toList(toSet(lst))) <= size(lst)
+ }) holds
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Epsilon5.scala b/src/test/resources/regression/verification/xlang/valid/Epsilon5.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0427cf086ba1050226ae8a3e28d6177a9904b460
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Epsilon5.scala
@@ -0,0 +1,9 @@
+import leon.Utils._
+
+object Epsilon5 {
+
+ def foo(x: Int, y: Int): Int = {
+ epsilon((z: Int) => z > x && z < y)
+ } ensuring(_ >= x)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Field1.scala b/src/test/resources/regression/verification/xlang/valid/Field1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..116557ab7b883d01a10168aeaf529d5300ee5f19
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Field1.scala
@@ -0,0 +1,11 @@
+object Field1 {
+
+ abstract sealed class A
+ case class B(size: Int) extends A
+
+ def foo(): Int = {
+ val b = B(3)
+ b.size
+ } ensuring(_ == 3)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Field2.scala b/src/test/resources/regression/verification/xlang/valid/Field2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9a96610235a68754b84e58f73f5e435ce642ebc9
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Field2.scala
@@ -0,0 +1,11 @@
+object Field2 {
+
+ abstract sealed class A
+ case class B(length: Int) extends A
+
+ def foo(): Int = {
+ val b = B(3)
+ b.length
+ } ensuring(_ == 3)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/IfExpr1.scala b/src/test/resources/regression/verification/xlang/valid/IfExpr1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..82db13d5285bc3c779010fd3e62b6e9e68e84e84
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/IfExpr1.scala
@@ -0,0 +1,13 @@
+object IfExpr1 {
+
+ def foo(): Int = {
+ var a = 1
+ var b = 2
+ if({a = a + 1; a != b})
+ a = a + 3
+ else
+ b = a + b
+ a
+ } ensuring(_ == 2)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/IfExpr2.scala b/src/test/resources/regression/verification/xlang/valid/IfExpr2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..7a681bc7276d07e41884147342dc0874d0bbf93d
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/IfExpr2.scala
@@ -0,0 +1,14 @@
+object IfExpr2 {
+
+ def foo(): Int = {
+ var a = 1
+ var b = 2
+ if(a < b) {
+ a = a + 3
+ b = b + 2
+ a = a + b
+ }
+ a
+ } ensuring(_ == 8)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/IfExpr3.scala b/src/test/resources/regression/verification/xlang/valid/IfExpr3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..86d4e494a7ce8fd22024020bb9580b393af8377a
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/IfExpr3.scala
@@ -0,0 +1,19 @@
+object IfExpr1 {
+
+ def foo(a: Int): Int = {
+
+ if(a > 0) {
+ var a = 1
+ var b = 2
+ a = 3
+ a + b
+ } else {
+ 5
+ //var a = 3
+ //var b = 1
+ //b = b + 1
+ //a + b
+ }
+ } ensuring(_ == 5)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/IfExpr4.scala b/src/test/resources/regression/verification/xlang/valid/IfExpr4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..94b99fde39e6f7e10b1c898548d60592023ffbd6
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/IfExpr4.scala
@@ -0,0 +1,18 @@
+object IfExpr4 {
+
+ def foo(a: Int): Int = {
+
+ if(a > 0) {
+ var a = 1
+ var b = 2
+ a = 3
+ a + b
+ } else {
+ var a = 3
+ var b = 1
+ b = b + 1
+ a + b
+ }
+ } ensuring(_ == 5)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/InstanceOf1.scala b/src/test/resources/regression/verification/xlang/valid/InstanceOf1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1c52338bbda859f82ef7ea619af088b9c1a1812d
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/InstanceOf1.scala
@@ -0,0 +1,18 @@
+object InstanceOf1 {
+
+ abstract class A
+ case class B(i: Int) extends A
+ case class C(i: Int) extends A
+
+ def foo(): Int = {
+ require(C(3).isInstanceOf[C])
+ val b: A = B(2)
+ if(b.isInstanceOf[B])
+ 0
+ else
+ -1
+ } ensuring(_ == 0)
+
+ def bar(): Int = foo()
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/MyTuple3.scala b/src/test/resources/regression/verification/xlang/valid/MyTuple3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2e14c067b78d86d4d915eb72178169d641e9755a
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/MyTuple3.scala
@@ -0,0 +1,8 @@
+object MyTuple3 {
+
+ def foo(): Int = {
+ val t = ((2, 3), true)
+ t._1._2
+ } ensuring( _ == 3)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/MyTuple4.scala b/src/test/resources/regression/verification/xlang/valid/MyTuple4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..6fcfed661beca0487da4b02db71677e2dbaac60e
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/MyTuple4.scala
@@ -0,0 +1,14 @@
+
+object MyTuple4 {
+
+ abstract class A
+ case class B(i: Int) extends A
+ case class C(a: A) extends A
+
+ def foo(): Int = {
+ val t = (1, (C(B(4)), 2), 3)
+ val (a1, (C(B(x)), a2), a3) = t
+ x
+ } ensuring( _ == 4)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/MyTuple5.scala b/src/test/resources/regression/verification/xlang/valid/MyTuple5.scala
new file mode 100644
index 0000000000000000000000000000000000000000..6a55bc8c9cdbc4f70be7a6b79c8d11137ecb0d71
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/MyTuple5.scala
@@ -0,0 +1,16 @@
+object MyTuple1 {
+
+ abstract class A
+ case class B(t: (Int, Int)) extends A
+ case class C(a: A) extends A
+
+ def foo(): Int = {
+ val t: (Int, (A, Int), Int) = (1, (C(B((4, 5))), 2), 3)
+ t match {
+ case (_, (B((x, y)), _), _) => x
+ case (_, (C(B((_, x))), _), y) => x
+ case (_, _, x) => x
+ }
+ } ensuring( _ == 5)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/MyTuple6.scala b/src/test/resources/regression/verification/xlang/valid/MyTuple6.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a54710fbbe54d9532a5ab4d2ba9906a48ad37acc
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/MyTuple6.scala
@@ -0,0 +1,8 @@
+object MyTuple6 {
+
+ def foo(t: (Int, Int)): (Int, Int) = {
+ require(t._1 > 0 && t._2 > 1)
+ t
+ } ensuring(res => res._1 > 0 && res._2 > 1)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested1.scala b/src/test/resources/regression/verification/xlang/valid/Nested1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..7745f794f369cf59b529133fa6c73383466acec8
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Nested1.scala
@@ -0,0 +1,15 @@
+object Nested1 {
+
+ def foo(i: Int): Int = {
+ val n = 2
+ def rec1(j: Int) = i + j + n
+ def rec2(j: Int) = {
+ def rec3(k: Int) = k + j + i
+ rec3(5)
+ }
+ rec2(2)
+ } ensuring(i + 7 == _)
+
+}
+
+// vim: set ts=4 sw=4 et:
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested10.scala b/src/test/resources/regression/verification/xlang/valid/Nested10.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b3c4f865367ca84a52091e89b655ac6438dc65a2
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Nested10.scala
@@ -0,0 +1,14 @@
+object Nested10 {
+
+ def foo(i: Int): Int = {
+ val n = 2
+ def rec1(j: Int) = {
+ i + j + n
+ }
+ def rec2(j: Int) = {
+ rec1(j)
+ }
+ rec2(2)
+ } ensuring(i + 4 == _)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested11.scala b/src/test/resources/regression/verification/xlang/valid/Nested11.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0316fc5f2ba3497691bc48b1d573933ba2cea027
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Nested11.scala
@@ -0,0 +1,14 @@
+object Nested11 {
+
+ abstract class A
+ case class B(b: Int) extends A
+
+ def foo(i: Int): Int = {
+ val b: A = B(3)
+ def rec1(j: Int) = b match {
+ case B(b) => i + j + b
+ }
+ rec1(2)
+ } ensuring(i + 5 == _)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested12.scala b/src/test/resources/regression/verification/xlang/valid/Nested12.scala
new file mode 100644
index 0000000000000000000000000000000000000000..05ac1569f630f1fc905a84f0550cbbaa42047906
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Nested12.scala
@@ -0,0 +1,17 @@
+object Nested12 {
+
+ abstract class A
+ case class B(b: Int) extends A
+
+ def foo(i: Int): Int = {
+ val b: A = B(3)
+ def rec1(a: A, j: Int, j2: Int) = a match {
+ case B(b) => i + j + j2 + b
+ }
+ def rec2(a: A, k: Int) = a match {
+ case B(b) => rec1(a, b, k)
+ }
+ rec2(b, 2)
+ } ensuring(i + 8 == _)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested13.scala b/src/test/resources/regression/verification/xlang/valid/Nested13.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ccb742494564433dffe096210fac07b37a663dfe
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Nested13.scala
@@ -0,0 +1,21 @@
+object Nested13 {
+
+ abstract class D
+ case class E(e: Int) extends D
+ case class F(d: D, f: Int) extends D
+
+ def foo(a : Int): Int = {
+
+ def rec1(d: D, j: Int): Int = d match {
+ case E(e) => j + e + a
+ case F(dNext, f) => f + rec1(dNext, j)
+ }
+
+ def rec2(d: D, i : Int) : Int = d match {
+ case E(e) => e
+ case F(dNext, f) => rec1(d, i)
+ }
+
+ rec2(F(E(2), 3), 0)
+ } ensuring(a + 5 == _)
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested14.scala b/src/test/resources/regression/verification/xlang/valid/Nested14.scala
new file mode 100644
index 0000000000000000000000000000000000000000..9a79a4f6e4e7c28aa860d0636487a60a06e9e2ba
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Nested14.scala
@@ -0,0 +1,11 @@
+object Nested14 {
+
+ def foo(i: Int): Int = {
+ def rec1(j: Int): Int = {
+ def rec2(k: Int): Int = if(k == 0) 0 else rec1(j-1)
+ rec2(j)
+ }
+ rec1(3)
+ } ensuring(0 == _)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested2.scala b/src/test/resources/regression/verification/xlang/valid/Nested2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..cc7220b02109c394e71c127e4cd3f53d6714ed7f
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Nested2.scala
@@ -0,0 +1,13 @@
+object Nested2 {
+
+ def foo(a: Int): Int = {
+ require(a >= 0)
+ val b = a + 2
+ def rec1(c: Int): Int = {
+ require(c >= 0)
+ b + c
+ }
+ rec1(2)
+ } ensuring(_ > 0)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested3.scala b/src/test/resources/regression/verification/xlang/valid/Nested3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..be6e6d04a335d12d079a9e3dc1a4b14ec0164014
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Nested3.scala
@@ -0,0 +1,15 @@
+object Nested3 {
+
+ def foo(a: Int): Int = {
+ require(a >= 0 && a <= 50)
+ val b = a + 2
+ val c = a + b
+ def rec1(d: Int): Int = {
+ require(d >= 0 && d <= 50)
+ val e = d + b + c
+ e
+ }
+ rec1(2)
+ } ensuring(_ > 0)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested4.scala b/src/test/resources/regression/verification/xlang/valid/Nested4.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ea1e6066c6f4b7aaf6df23065e3011b86471b7f4
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Nested4.scala
@@ -0,0 +1,19 @@
+object Nested4 {
+
+ def foo(a: Int, a2: Int): Int = {
+ require(a >= 0 && a <= 50)
+ val b = a + 2
+ val c = a + b
+ if(a2 > a) {
+ def rec1(d: Int): Int = {
+ require(d >= 0 && d <= 50)
+ val e = d + b + c + a2
+ e
+ } ensuring(_ > 0)
+ rec1(2)
+ } else {
+ 5
+ }
+ } ensuring(_ > 0)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested5.scala b/src/test/resources/regression/verification/xlang/valid/Nested5.scala
new file mode 100644
index 0000000000000000000000000000000000000000..6ba128f415ecc3c61ebcccb42b65100d15373982
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Nested5.scala
@@ -0,0 +1,12 @@
+object Nested5 {
+
+ def foo(a: Int): Int = {
+ require(a >= 0)
+ def bar(b: Int): Int = {
+ require(b > 0)
+ b + 3
+ } ensuring(a >= 0 && _ == b + 3)
+ bar(2)
+ } ensuring(a >= 0 && _ == 5)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested6.scala b/src/test/resources/regression/verification/xlang/valid/Nested6.scala
new file mode 100644
index 0000000000000000000000000000000000000000..1c0220c0447dba10ccd710d60e5f19b1c1ec6e18
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Nested6.scala
@@ -0,0 +1,14 @@
+object Nested5 {
+
+ def foo(a: Int): Int = {
+ require(a >= 0)
+ def bar(b: Int): Int = {
+ require(b > 0)
+ b + 3
+ } ensuring(prop(a, b) && a >= 0 && _ == b + 3)
+ bar(2)
+ } ensuring(a >= 0 && _ == 5)
+
+ def prop(x: Int, y: Int): Boolean = x + y > 0
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested7.scala b/src/test/resources/regression/verification/xlang/valid/Nested7.scala
new file mode 100644
index 0000000000000000000000000000000000000000..62f5a567f49be174873a24711e630f69e8469a22
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Nested7.scala
@@ -0,0 +1,19 @@
+object Nested2 {
+
+ def foo(a: Int): Int = {
+ require(a >= 0)
+ val b = a + 2
+ def rec1(c: Int): Int = {
+ require(c >= 0)
+ b + c + bar(a) + bar(b) + bar(c)
+ }
+ rec1(2) + bar(a)
+ } ensuring(_ > 0)
+
+
+ def bar(x: Int): Int = {
+ require(x >= 0)
+ x
+ } ensuring(_ >= 0)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested8.scala b/src/test/resources/regression/verification/xlang/valid/Nested8.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e8a05e40e6cd1b2428e03bcf1a9f96c67797c698
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Nested8.scala
@@ -0,0 +1,43 @@
+import leon.Utils._
+
+object Nested8 {
+
+ def foo(a: Int): Int = {
+ require(a > 0)
+
+ def bar(b: Int): Int = {
+ if(a < b) {
+ def rec(c: Int): Int = {
+ require(c > 0)
+ c + b
+ } ensuring(_ > 0)
+ rec(2)
+ } else 3
+ }
+ bar(1)
+ } ensuring(_ > 0)
+
+ /*
+ def partitioned(a: Map[Int, Int], size: Int, l1: Int, u1: Int, l2: Int, u2: Int): Boolean = {
+ require(l1 >= 0 && u1 < l2 && u2 < size)
+ if(l2 > u2 || l1 > u1)
+ true
+ else {
+ var i = l1
+ var j = l2
+ var isPartitionned = true
+ (while(i <= u1) {
+ j = l2
+ (while(j <= u2) {
+ if(a(i) > a(j))
+ isPartitionned = false
+ j = j + 1
+ }) invariant(j >= l2 && i <= u1)
+ i = i + 1
+ }) invariant(i >= l1)
+ isPartitionned
+ }
+ }
+ */
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Nested9.scala b/src/test/resources/regression/verification/xlang/valid/Nested9.scala
new file mode 100644
index 0000000000000000000000000000000000000000..3344a2c7973bed9da2c42208742c34c184b458ac
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Nested9.scala
@@ -0,0 +1,23 @@
+object Nested4 {
+
+ def foo(a: Int, a2: Int): Int = {
+ require(a >= 0 && a <= 50)
+ val b = a + 2
+ val c = a + b
+ if(a2 > a) {
+ def rec1(d: Int): Int = {
+ require(d >= 0 && d <= 50)
+ val e = d + b + c + a2
+ def rec2(f: Int): Int = {
+ require(f >= c)
+ f + e
+ } ensuring(_ > 0)
+ rec2(c+1)
+ } ensuring(_ > 0)
+ rec1(2)
+ } else {
+ 5
+ }
+ } ensuring(_ > 0)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/NestedVar.scala b/src/test/resources/regression/verification/xlang/valid/NestedVar.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a26b7312b2f5f85509c6e55cc706fb29845202b1
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/NestedVar.scala
@@ -0,0 +1,17 @@
+object NestedVar {
+
+ def foo(): Int = {
+ val a = 3
+ def rec(x: Int): Int = {
+ var b = 3
+ var c = 3
+ if(x > 0)
+ b = 2
+ else
+ c = 2
+ c+b
+ }
+ rec(a)
+ } ensuring(_ == 5)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Unit1.scala b/src/test/resources/regression/verification/xlang/valid/Unit1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..a7b890d762648cba480c817506c7eee22259860d
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Unit1.scala
@@ -0,0 +1,7 @@
+object Unit1 {
+
+ def foo(): Unit = ({
+ ()
+ }) ensuring(_ == ())
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/Unit2.scala b/src/test/resources/regression/verification/xlang/valid/Unit2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..ac659589af503a8a79f261f9eb05be095e2e0943
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/Unit2.scala
@@ -0,0 +1,7 @@
+object Unit2 {
+
+ def foo(u: Unit): Unit = {
+ u
+ } ensuring(_ == ())
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/While1.scala b/src/test/resources/regression/verification/xlang/valid/While1.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0d868b399330c91342bd4ed26f7166f6b40dae5f
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/While1.scala
@@ -0,0 +1,13 @@
+object While1 {
+
+ def foo(): Int = {
+ var a = 0
+ var i = 0
+ while(i < 10) {
+ a = a + 1
+ i = i + 1
+ }
+ a
+ } ensuring(_ == 10)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/While2.scala b/src/test/resources/regression/verification/xlang/valid/While2.scala
new file mode 100644
index 0000000000000000000000000000000000000000..e841ed40ebf045e5545b584b5c16e80bfc11396a
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/While2.scala
@@ -0,0 +1,13 @@
+object While1 {
+
+ def foo(): Int = {
+ var a = 0
+ var i = 0
+ while(i < 10) {
+ a = a + i
+ i = i + 1
+ }
+ a
+ } ensuring(_ == 45)
+
+}
diff --git a/src/test/resources/regression/verification/xlang/valid/While3.scala b/src/test/resources/regression/verification/xlang/valid/While3.scala
new file mode 100644
index 0000000000000000000000000000000000000000..da85d5dfab90410eb4d2ee23cea90627d1d40c93
--- /dev/null
+++ b/src/test/resources/regression/verification/xlang/valid/While3.scala
@@ -0,0 +1,13 @@
+object While3 {
+
+ def foo(): Int = {
+ var a = 0
+ var i = 0
+ while({i = i+2; i <= 10}) {
+ a = a + i
+ i = i - 1
+ }
+ a
+ } ensuring(_ == 54)
+
+}