diff --git a/src/test/resources/regression/frontends/passing/ImplicitDefs2.scala b/src/test/resources/regression/frontends/passing/ImplicitDefs2.scala
index 9f4b1a83fbb7dd4c6e4600d1030d083335344b62..dba63890bd682f1d392cfe719ffd851b25dfd695 100644
--- a/src/test/resources/regression/frontends/passing/ImplicitDefs2.scala
+++ b/src/test/resources/regression/frontends/passing/ImplicitDefs2.scala
@@ -103,10 +103,10 @@ sealed abstract class List[T] {
} ensuring (res => (res.size == size) && (res.content == content))
def take(i: BigInt): List[T] = { (this, i) match {
- case (Nil(), _) => Nil()
+ case (Nil(), _) => Nil[T]()
case (Cons(h, t), i) =>
if (i <= BigInt(0)) {
- Nil()
+ Nil[T]()
} else {
Cons(h, t.take(i-1))
}
@@ -117,7 +117,7 @@ sealed abstract class List[T] {
)}
def drop(i: BigInt): List[T] = { (this, i) match {
- case (Nil(), _) => Nil()
+ case (Nil(), _) => Nil[T]()
case (Cons(h, t), i) =>
if (i <= BigInt(0)) {
Cons(h, t)
@@ -136,7 +136,7 @@ sealed abstract class List[T] {
}
def replace(from: T, to: T): List[T] = { this match {
- case Nil() => Nil()
+ case Nil() => Nil[T]()
case Cons(h, t) =>
val r = t.replace(from, to)
if (h == from) {
@@ -177,7 +177,7 @@ sealed abstract class List[T] {
case (Cons(h1, t1), Cons(h2, t2)) =>
Cons((h1, h2), t1.zip(t2))
case (_) =>
- Nil()
+ Nil[(T, B)]()
}} ensuring { _.size == (
if (this.size <= that.size) this.size else that.size
)}
@@ -190,7 +190,7 @@ sealed abstract class List[T] {
Cons(h, t - e)
}
case Nil() =>
- Nil()
+ Nil[T]()
}} ensuring { _.content == this.content -- Set(e) }
def --(that: List[T]): List[T] = { this match {
@@ -201,7 +201,7 @@ sealed abstract class List[T] {
Cons(h, t -- that)
}
case Nil() =>
- Nil()
+ Nil[T]()
}} ensuring { _.content == this.content -- that.content }
def &(that: List[T]): List[T] = { this match {
@@ -212,7 +212,7 @@ sealed abstract class List[T] {
t & that
}
case Nil() =>
- Nil()
+ Nil[T]()
}} ensuring { _.content == (this.content & that.content) }
def pad(s: BigInt, e: T): List[T] = (this, s) match {
@@ -225,13 +225,13 @@ sealed abstract class List[T] {
}
def find(e: T): Option[BigInt] = { this match {
- case Nil() => None()
+ case Nil() => None[BigInt]()
case Cons(h, t) =>
if (h == e) {
- Some(0)
+ Some[BigInt](0)
} else {
t.find(e) match {
- case None() => None()
+ case None() => None[BigInt]()
case Some(i) => Some(i+1)
}
}
@@ -350,7 +350,7 @@ sealed abstract class List[T] {
// Higher-order API
def map[R](f: T => R): List[R] = { this match {
- case Nil() => Nil()
+ case Nil() => Nil[R]()
case Cons(h, t) => f(h) :: t.map(f)
}} ensuring { _.size == this.size}
@@ -365,12 +365,12 @@ sealed abstract class List[T] {
}
def scanLeft[R](z: R)(f: (R,T) => R): List[R] = this match {
- case Nil() => z :: Nil()
+ case Nil() => z :: Nil[R]()
case Cons(h,t) => z :: t.scanLeft(f(z,h))(f)
}
def scanRight[R](f: (T,R) => R)(z: R): List[R] = { this match {
- case Nil() => z :: Nil()
+ case Nil() => z :: Nil[R]()
case Cons(h, t) =>
val rest@Cons(h1,_) = t.scanRight(f)(z)
f(h, h1) :: rest
@@ -380,7 +380,7 @@ sealed abstract class List[T] {
ListOps.flatten(this map f)
def filter(p: T => Boolean): List[T] = { this match {
- case Nil() => Nil()
+ case Nil() => Nil[T]()
case Cons(h, t) if p(h) => Cons(h, t.filter(p))
case Cons(_, t) => t.filter(p)
}} ensuring { res => res.size <= this.size && res.forall(p) }
@@ -396,7 +396,7 @@ sealed abstract class List[T] {
def exists(p: T => Boolean) = !forall(!p(_))
def find(p: T => Boolean): Option[T] = { this match {
- case Nil() => None()
+ case Nil() => None[T]()
case Cons(h, t) if p(h) => Some(h)
case Cons(_, t) => t.find(p)
}} ensuring { _.isDefined == exists(p) }
@@ -426,7 +426,7 @@ object List {
object ListOps {
def flatten[T](ls: List[List[T]]): List[T] = ls match {
case Cons(h, t) => h ++ flatten(t)
- case Nil() => Nil()
+ case Nil() => Nil[T]()
}
def isSorted(ls: List[BigInt]): Boolean = ls match {
diff --git a/src/test/resources/regression/repair/Compiler1.scala b/src/test/resources/regression/repair/Compiler1.scala
index 9ff0785d70b9080327890a5af4729a59f5c41edd..300868d67463da6ae3690b719c0bb7a74eae5b1b 100644
--- a/src/test/resources/regression/repair/Compiler1.scala
+++ b/src/test/resources/regression/repair/Compiler1.scala
@@ -110,9 +110,9 @@ object Semantics {
def semUntyped(t : Expr): BigInt = { t match {
case Plus (lhs, rhs) => semUntyped(lhs) + semUntyped(rhs)
case Minus(lhs, rhs) => semUntyped(lhs) - semUntyped(rhs)
- case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else 0
+ case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else BigInt(0)
case Or(lhs, rhs ) =>
- if (semUntyped(lhs) == 0) semUntyped(rhs) else 1
+ if (semUntyped(lhs) == 0) semUntyped(rhs) else BigInt(1)
case Not(e) =>
b2i(semUntyped(e) == 0)
case LessThan(lhs, rhs) =>
diff --git a/src/test/resources/regression/repair/Heap4.scala b/src/test/resources/regression/repair/Heap4.scala
index 01c8b41f941c31d8a8bf2186bb26ac48c42de42b..937e29b5c41eadbc1939c7a7d8febb2956e026d0 100644
--- a/src/test/resources/regression/repair/Heap4.scala
+++ b/src/test/resources/regression/repair/Heap4.scala
@@ -47,7 +47,7 @@ object HeapSort {
}
def heapSize(t: Heap): BigInt = { t match {
- case Leaf() => 0
+ case Leaf() => BigInt(0)
case Node(v, l, r) => heapSize(l) + 1 + heapSize(r)
}} ensuring(_ >= 0)
diff --git a/src/test/resources/regression/repair/List1.scala b/src/test/resources/regression/repair/List1.scala
index ff31089cf42af55b2e8a43331fcfd39cd5f2334e..79b7ecb444be464b464202721dbebd0b4045c158 100644
--- a/src/test/resources/regression/repair/List1.scala
+++ b/src/test/resources/regression/repair/List1.scala
@@ -9,8 +9,8 @@ import leon.collection._
sealed abstract class List0[T] {
def size: BigInt = (this match {
- case Nil0() => 0
- case Cons0(h, t) => 1 + t.size
+ case Nil0() => BigInt(0)
+ case Cons0(h, t) => BigInt(1) + t.size
}) ensuring (_ >= 0)
def content: Set[T] = this match {
diff --git a/src/test/resources/regression/repair/MergeSort2.scala b/src/test/resources/regression/repair/MergeSort2.scala
index 649582ee282910cfd38e48983cea3a389ce68564..4447edc40430d87690516ea86020095cb2727243 100644
--- a/src/test/resources/regression/repair/MergeSort2.scala
+++ b/src/test/resources/regression/repair/MergeSort2.scala
@@ -9,7 +9,7 @@ object MergeSort {
case Cons(a, Cons(b, t)) =>
val (rec1, rec2) = split(t)
(Cons(a, rec1), Cons(b, rec2))
- case other => (other, Nil())
+ case other => (other, Nil[BigInt]())
}} ensuring { res =>
val (l1, l2) = res
l1.size >= l2.size &&
diff --git a/src/test/resources/regression/synthesis/Church/Add.scala b/src/test/resources/regression/synthesis/Church/Add.scala
index 5931eeb591cf61567d285e68fee9bb49f7c19c07..c94fc4c7f1cb29e2a1fb49d4b134bb163c5b69eb 100644
--- a/src/test/resources/regression/synthesis/Church/Add.scala
+++ b/src/test/resources/regression/synthesis/Church/Add.scala
@@ -11,8 +11,8 @@ object Numerals {
def value(n: Num): BigInt = {
n match {
- case Z => 0
- case S(p) => 1 + value(p)
+ case Z => BigInt(0)
+ case S(p) => BigInt(1) + value(p)
}
} ensuring (_ >= 0)
diff --git a/src/test/resources/regression/synthesis/Church/Distinct.scala b/src/test/resources/regression/synthesis/Church/Distinct.scala
index a6fb4881c471d936e3627dcc7dd42e1189bdb89c..b7f093e9f752adbee5ccc9f8833a34d71011022a 100644
--- a/src/test/resources/regression/synthesis/Church/Distinct.scala
+++ b/src/test/resources/regression/synthesis/Church/Distinct.scala
@@ -11,8 +11,8 @@ object Numerals {
def value(n: Num): BigInt = {
n match {
- case Z => 0
- case S(p) => 1 + value(p)
+ case Z => BigInt(0)
+ case S(p) => BigInt(1) + value(p)
}
} ensuring (_ >= 0)
diff --git a/src/test/resources/regression/synthesis/Church/Mult.scala b/src/test/resources/regression/synthesis/Church/Mult.scala
index 9f8f422c689d741bf076605615e3f8cdf3039354..bc4afe213fa9af7ac3174e11325e4bcbd29b8e20 100644
--- a/src/test/resources/regression/synthesis/Church/Mult.scala
+++ b/src/test/resources/regression/synthesis/Church/Mult.scala
@@ -11,8 +11,8 @@ object Numerals {
def value(n: Num): BigInt = {
n match {
- case Z => 0
- case S(p) => 1 + value(p)
+ case Z => BigInt(0)
+ case S(p) => BigInt(1) + value(p)
}
} ensuring (_ >= 0)
diff --git a/src/test/resources/regression/synthesis/Church/Squared.scala b/src/test/resources/regression/synthesis/Church/Squared.scala
index 5d7877469d3cf5015b703e179fde86b8a6a234ea..92ac747b8fbe26afe008d1796dbd3ce5743b3a35 100644
--- a/src/test/resources/regression/synthesis/Church/Squared.scala
+++ b/src/test/resources/regression/synthesis/Church/Squared.scala
@@ -11,8 +11,8 @@ object Numerals {
def value(n:Num) : BigInt = {
n match {
- case Z => 0
- case S(p) => 1 + value(p)
+ case Z => BigInt(0)
+ case S(p) => BigInt(1) + value(p)
}
} ensuring (_ >= 0)
diff --git a/src/test/resources/regression/synthesis/List/Delete.scala b/src/test/resources/regression/synthesis/List/Delete.scala
index 07d64d6b307f5e7b998026fe0773425ae02a6947..0c82b3da420c405a86c6467e75070bb5761dca1b 100644
--- a/src/test/resources/regression/synthesis/List/Delete.scala
+++ b/src/test/resources/regression/synthesis/List/Delete.scala
@@ -10,8 +10,8 @@ object Delete {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/src/test/resources/regression/synthesis/List/Diff.scala b/src/test/resources/regression/synthesis/List/Diff.scala
index 8659cd59bec9f6efe542008120312357a53869ad..477ea0bdb32ea47b559815c3a39f3e20f6aadc93 100644
--- a/src/test/resources/regression/synthesis/List/Diff.scala
+++ b/src/test/resources/regression/synthesis/List/Diff.scala
@@ -10,8 +10,8 @@ object Diff {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/src/test/resources/regression/synthesis/List/Insert.scala b/src/test/resources/regression/synthesis/List/Insert.scala
index 13636c1554e698f5b89bf37459307f5ed3e46b35..c98947bb1afaa8ce8038fb5aa184bf8f394b5bd9 100644
--- a/src/test/resources/regression/synthesis/List/Insert.scala
+++ b/src/test/resources/regression/synthesis/List/Insert.scala
@@ -10,8 +10,8 @@ object Insert {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/src/test/resources/regression/synthesis/List/Split1.scala b/src/test/resources/regression/synthesis/List/Split1.scala
index facbda843c5a6349cc6efca052bf104ec63f7156..66def0ffa2a6980c7416bc18f5d6882d0c55c255 100644
--- a/src/test/resources/regression/synthesis/List/Split1.scala
+++ b/src/test/resources/regression/synthesis/List/Split1.scala
@@ -8,8 +8,8 @@ object List {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/src/test/resources/regression/synthesis/List/Split2.scala b/src/test/resources/regression/synthesis/List/Split2.scala
index 38c07caf52566eb6f599e2557900b1ed83a53c37..5d66b4a59da65f3bed57867f7a00b2465c92fe71 100644
--- a/src/test/resources/regression/synthesis/List/Split2.scala
+++ b/src/test/resources/regression/synthesis/List/Split2.scala
@@ -8,8 +8,8 @@ object List {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/src/test/resources/regression/synthesis/List/Split3.scala b/src/test/resources/regression/synthesis/List/Split3.scala
index 15c74190e1839abb484b375b28fea1582d8d58ea..eca76884d352aeb72eb2af2cd098b0d6166a2a0a 100644
--- a/src/test/resources/regression/synthesis/List/Split3.scala
+++ b/src/test/resources/regression/synthesis/List/Split3.scala
@@ -8,8 +8,8 @@ object List {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/src/test/resources/regression/synthesis/List/Union.scala b/src/test/resources/regression/synthesis/List/Union.scala
index 79d97ee9f4de9107c31a7a370e6f7f55b61a5290..c36a5933c81393b5ab21bf3b9c463943b9f45e3c 100644
--- a/src/test/resources/regression/synthesis/List/Union.scala
+++ b/src/test/resources/regression/synthesis/List/Union.scala
@@ -10,8 +10,8 @@ object Union {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => BigInt(1) + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/src/test/resources/regression/termination/looping/LambdaCalculus.scala b/src/test/resources/regression/termination/looping/LambdaCalculus.scala
index 884e5dee5564e90eb9b97210e000a30418ea22f8..d24d8c31b998dc0226827f832409b685e3a1f47d 100644
--- a/src/test/resources/regression/termination/looping/LambdaCalculus.scala
+++ b/src/test/resources/regression/termination/looping/LambdaCalculus.scala
@@ -32,9 +32,9 @@ object LambdaCalculus {
case App(t1, t2) => looping_eval(t1) match {
case Some(Abs(x, body)) => looping_eval(t2) match {
case Some(v2) => looping_eval(subst(x, v2, body))
- case None() => None()
+ case None() => None[Term]()
}
- case _ => None() // stuck
+ case _ => None[Term]() // stuck
}
case _ => Some(t) // Abs or Var, already a value
}) ensuring { res => res match {
diff --git a/src/test/resources/regression/termination/looping/Queue.scala b/src/test/resources/regression/termination/looping/Queue.scala
index a571e82e853d96dc84b7376a6751b1281dc50787..3df1a9ac5a69ca639a88a335b70a260e6d7df8a5 100644
--- a/src/test/resources/regression/termination/looping/Queue.scala
+++ b/src/test/resources/regression/termination/looping/Queue.scala
@@ -7,19 +7,19 @@ sealed abstract class Queue[T] {
def looping_1: BigInt = {
this match {
- case QEmpty() => 0
+ case QEmpty() => BigInt(0)
case QCons(f, r) => f.size + r.size
}
} ensuring (res => res == this.looping_2.size && res >= 0)
def looping_2: List[T] = (this match {
- case QEmpty() => Nil()
+ case QEmpty() => Nil[T]()
case QCons(f, r) => f ++ r.reverse
}) ensuring (resOne => this.looping_3 == resOne.content && resOne.size == this.looping_1 && resOne.size >= 0)
def looping_3: Set[T] = (this match {
- case QEmpty() => Set()
+ case QEmpty() => Set[T]()
case QCons(f, r) => f.content ++ r.content
}) ensuring (res => res == this.looping_2.content)
}
diff --git a/src/test/resources/regression/termination/valid/CountTowardsZero.scala b/src/test/resources/regression/termination/valid/CountTowardsZero.scala
index 4ef5ba8b07ccbe508c4a88945f9ccf7faaf5231d..e0ce187ad4fddcd8b2aac5f973ba50fc1d589fb6 100644
--- a/src/test/resources/regression/termination/valid/CountTowardsZero.scala
+++ b/src/test/resources/regression/termination/valid/CountTowardsZero.scala
@@ -2,13 +2,13 @@
object Test {
def f(x: BigInt): BigInt = {
if (x == 0) {
- 0
+ BigInt(0)
} else if (x > 0) {
f(x-1)+2
} else if (x < 0) {
f(x+1)-2
} else {
- 33
+ BigInt(33)
}
} ensuring (_ == x*2)
}
diff --git a/src/test/resources/regression/termination/valid/Queue.scala b/src/test/resources/regression/termination/valid/Queue.scala
index 2b73919a7c732a2233273d4f284f4f8c3ad93143..dee019a41f27c7fca1f3e2cc7011ac544e18a541 100644
--- a/src/test/resources/regression/termination/valid/Queue.scala
+++ b/src/test/resources/regression/termination/valid/Queue.scala
@@ -7,13 +7,13 @@ sealed abstract class Queue[T] {
def size: BigInt = {
this match {
- case QEmpty() => 0
+ case QEmpty() => BigInt(0)
case QCons(f, r) => f.size + r.size
}
} ensuring (res => res == this.toList.size && res >= 0)
def toList: List[T] = (this match {
- case QEmpty() => Nil()
+ case QEmpty() => Nil[T]()
case QCons(f, r) => f ++ r.reverse
}) ensuring (resOne => this.content == resOne.content && resOne.size >= 0)
diff --git a/src/test/resources/regression/verification/purescala/valid/ParBalance.scala b/src/test/resources/regression/verification/purescala/valid/ParBalance.scala
index 4db8aecb027d02c0a9ae7bbb8bdd9411a1d87c6a..29133762e6da8118e1e380b6fabb4fb3880d482b 100644
--- a/src/test/resources/regression/verification/purescala/valid/ParBalance.scala
+++ b/src/test/resources/regression/verification/purescala/valid/ParBalance.scala
@@ -147,8 +147,8 @@ object ParBalance {
}
def size(list: List): BigInt = (list match {
- case Nil() => 0
- case Cons(h, t) => 1 + size(t)
+ case Nil() => BigInt(0)
+ case Cons(h, t) => BigInt(1) + size(t)
}) ensuring (_ >= 0)
def addLast(list: List, x: BigInt): List = {
diff --git a/src/test/scala/leon/test/testcases/TestCasesCompile.scala b/src/test/scala/leon/test/testcases/TestCasesCompile.scala
index b5fe1ca32d128891662989877267386b2f713463..f82ff346c2c14cb8ce92664959a4345a0653b12d 100644
--- a/src/test/scala/leon/test/testcases/TestCasesCompile.scala
+++ b/src/test/scala/leon/test/testcases/TestCasesCompile.scala
@@ -13,7 +13,7 @@ class TestCasesCompile extends LeonTestSuite {
val pipeline = frontends.scalac.ExtractionPhase andThen utils.PreprocessingPhase
- def testFrontend(f: File, strip: Int) = {
+ def testFrontend(f: File, strip: Int): Boolean = {
val name = f.getAbsolutePath.split("/").toList.drop(strip).mkString("/")
val ctx = createLeonContext()
@@ -21,9 +21,11 @@ class TestCasesCompile extends LeonTestSuite {
try {
pipeline.run(ctx)(List(f.getAbsolutePath))
info(name)
+ true
} catch {
case _: LeonFatalError =>
- fail("Failed to compile "+name)
+ info(Console.YELLOW+" Failed to compile "+name)
+ false
}
}
@@ -46,8 +48,16 @@ class TestCasesCompile extends LeonTestSuite {
info("Compiling "+all.size+" testcases...")
+ var nFailed = new java.util.concurrent.atomic.AtomicInteger(0)
all.par.foreach { f =>
- testFrontend(f, slashes)
+ if (!testFrontend(f, slashes)) {
+ nFailed.incrementAndGet()
+ }
+ }
+
+ val nFailedInt = nFailed.get()
+ if (nFailedInt > 0) {
+ fail(s"$nFailedInt test(s) failed to compile")
}
}
}
diff --git a/testcases/repair/Compiler/Compiler.scala b/testcases/repair/Compiler/Compiler.scala
index f0d0ed1f07fc49fa3f94e1fcf50194c84912e7a9..4b77a547a378b84aab4378459a5fb5b91f83d8a3 100644
--- a/testcases/repair/Compiler/Compiler.scala
+++ b/testcases/repair/Compiler/Compiler.scala
@@ -108,9 +108,9 @@ object Semantics {
def semUntyped( t : Expr) : BigInt = { t match {
case Plus (lhs, rhs) => semUntyped(lhs) + semUntyped(rhs)
case Minus(lhs, rhs) => semUntyped(lhs) - semUntyped(rhs)
- case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else 0
+ case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else BigInt(0)
case Or(lhs, rhs ) =>
- if (semUntyped(lhs) == 0) semUntyped(rhs) else 1
+ if (semUntyped(lhs) == 0) semUntyped(rhs) else BigInt(1)
case Not(e) =>
b2i(semUntyped(e) == 0)
case LessThan(lhs, rhs) =>
diff --git a/testcases/repair/Compiler/Compiler1.scala b/testcases/repair/Compiler/Compiler1.scala
index f3e840442bdb3936cc167baa9a29b3937d616d71..b1f9bc859cccdc53162b29d3480e5c4519e7cd96 100644
--- a/testcases/repair/Compiler/Compiler1.scala
+++ b/testcases/repair/Compiler/Compiler1.scala
@@ -108,9 +108,9 @@ object Semantics {
def semUntyped( t : Expr) : BigInt = { t match {
case Plus (lhs, rhs) => semUntyped(lhs) + semUntyped(rhs)
case Minus(lhs, rhs) => semUntyped(lhs) - semUntyped(rhs)
- case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else 0
+ case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else BigInt(0)
case Or(lhs, rhs ) =>
- if (semUntyped(lhs) == 0) semUntyped(rhs) else 1
+ if (semUntyped(lhs) == 0) semUntyped(rhs) else BigInt(1)
case Not(e) =>
b2i(semUntyped(e) == 0)
case LessThan(lhs, rhs) =>
diff --git a/testcases/repair/Compiler/Compiler2.scala b/testcases/repair/Compiler/Compiler2.scala
index 6703cf715953f44bb4c0a9a0b2f4222d7a6df7a8..1950b679a6d5727bec02a6fe4bf457f1260bc1c7 100644
--- a/testcases/repair/Compiler/Compiler2.scala
+++ b/testcases/repair/Compiler/Compiler2.scala
@@ -108,9 +108,9 @@ object Semantics {
def semUntyped( t : Expr) : BigInt = { t match {
case Plus (lhs, rhs) => semUntyped(lhs) + semUntyped(rhs)
case Minus(lhs, rhs) => semUntyped(lhs) - semUntyped(rhs)
- case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else 0
+ case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else BigInt(0)
case Or(lhs, rhs ) =>
- if (semUntyped(lhs) == 0) semUntyped(rhs) else 1
+ if (semUntyped(lhs) == 0) semUntyped(rhs) else BigInt(1)
case Not(e) =>
b2i(semUntyped(e) == 0)
case LessThan(lhs, rhs) =>
diff --git a/testcases/repair/Compiler/Compiler3.scala b/testcases/repair/Compiler/Compiler3.scala
index 24937f81a069ea5e7480b4d088e6db0190eab3ce..367e43b9fcf8e1579dd91ed08a13506184a05532 100644
--- a/testcases/repair/Compiler/Compiler3.scala
+++ b/testcases/repair/Compiler/Compiler3.scala
@@ -108,9 +108,9 @@ object Semantics {
def semUntyped( t : Expr) : BigInt = { t match {
case Plus (lhs, rhs) => semUntyped(lhs) + semUntyped(rhs)
case Minus(lhs, rhs) => semUntyped(lhs) - semUntyped(rhs)
- case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else 0
+ case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else BigInt(0)
case Or(lhs, rhs ) =>
- if (semUntyped(lhs) == 0) semUntyped(rhs) else 1
+ if (semUntyped(lhs) == 0) semUntyped(rhs) else BigInt(1)
case Not(e) =>
b2i(semUntyped(e) == 0)
case LessThan(lhs, rhs) =>
diff --git a/testcases/repair/Compiler/Compiler4.scala b/testcases/repair/Compiler/Compiler4.scala
index 33f24376efc4240a32c6428ae7a2d6db5949b851..f49670ddc31632343fea32f1b8d39ca288f214d4 100644
--- a/testcases/repair/Compiler/Compiler4.scala
+++ b/testcases/repair/Compiler/Compiler4.scala
@@ -108,9 +108,9 @@ object Semantics {
def semUntyped( t : Expr) : BigInt = { t match {
case Plus (lhs, rhs) => semUntyped(lhs) + semUntyped(rhs)
case Minus(lhs, rhs) => semUntyped(lhs) - semUntyped(rhs)
- case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else 0
+ case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else BigInt(0)
case Or(lhs, rhs ) =>
- if (semUntyped(lhs) == 0) semUntyped(rhs) else 1
+ if (semUntyped(lhs) == 0) semUntyped(rhs) else BigInt(1)
case Not(e) =>
b2i(semUntyped(e) == 0)
case LessThan(lhs, rhs) =>
diff --git a/testcases/repair/Compiler/Compiler5.scala b/testcases/repair/Compiler/Compiler5.scala
index 5ce70621262330906b9182d526994e8e6953bdef..fdefc6b31d8edabc379968c101b3db2d8513a007 100644
--- a/testcases/repair/Compiler/Compiler5.scala
+++ b/testcases/repair/Compiler/Compiler5.scala
@@ -108,9 +108,9 @@ object Semantics {
def semUntyped( t : Expr) : BigInt = { t match {
case Plus (lhs, rhs) => semUntyped(lhs) + semUntyped(rhs)
case Minus(lhs, rhs) => semUntyped(lhs) - semUntyped(rhs)
- case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else 0
+ case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else BigInt(0)
case Or(lhs, rhs ) =>
- if (semUntyped(lhs) == 0) semUntyped(rhs) else 1
+ if (semUntyped(lhs) == 0) semUntyped(rhs) else BigInt(1)
case Not(e) =>
b2i(semUntyped(e) == 0)
case LessThan(lhs, rhs) =>
diff --git a/testcases/repair/Compiler/Compiler6.scala b/testcases/repair/Compiler/Compiler6.scala
index 0848603a1428bee0aa58d4152bf5779c2d70d9ce..44bf523ec7aff63376ba24312594045296536dcf 100644
--- a/testcases/repair/Compiler/Compiler6.scala
+++ b/testcases/repair/Compiler/Compiler6.scala
@@ -108,9 +108,9 @@ object Semantics {
def semUntyped( t : Expr) : BigInt = { t match {
case Plus (lhs, rhs) => semUntyped(lhs) + semUntyped(rhs)
case Minus(lhs, rhs) => semUntyped(lhs) - semUntyped(rhs)
- case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else 0
+ case And (lhs, rhs) => if (semUntyped(lhs)!=0) semUntyped(rhs) else BigInt(0)
case Or(lhs, rhs ) =>
- if (semUntyped(lhs) == 0) semUntyped(rhs) else 1
+ if (semUntyped(lhs) == 0) semUntyped(rhs) else BigInt(1)
case Not(e) =>
b2i(semUntyped(e) == 0)
case LessThan(lhs, rhs) =>
diff --git a/testcases/repair/Heap/Heap.scala b/testcases/repair/Heap/Heap.scala
index 71f18a7605c28a39fc0288ec47a83a40738c4476..a3c064376563d4584aa76367b1da9faf72592489 100644
--- a/testcases/repair/Heap/Heap.scala
+++ b/testcases/repair/Heap/Heap.scala
@@ -47,7 +47,7 @@ object Heaps {
}
def heapSize(t: Heap): BigInt = { t match {
- case Leaf() => 0
+ case Leaf() => BigInt(0)
case Node(v, l, r) => heapSize(l) + 1 + heapSize(r)
}} ensuring(_ >= 0)
diff --git a/testcases/repair/Heap/Heap1.scala b/testcases/repair/Heap/Heap1.scala
index bb62940303195930d7b6ddb3020c2ead2dd1b9c0..7cd8659614e40551538866c6f929159864344244 100644
--- a/testcases/repair/Heap/Heap1.scala
+++ b/testcases/repair/Heap/Heap1.scala
@@ -47,7 +47,7 @@ object Heaps {
}
def heapSize(t: Heap): BigInt = { t match {
- case Leaf() => 0
+ case Leaf() => BigInt(0)
case Node(v, l, r) => heapSize(l) + 1 + heapSize(r)
}} ensuring(_ >= 0)
diff --git a/testcases/repair/Heap/Heap10.scala b/testcases/repair/Heap/Heap10.scala
index bba2389a395a05b0b093e0e01d504eb17a3fe67e..de5ae51d1796aa2e01101207f63fad657bfe02af 100644
--- a/testcases/repair/Heap/Heap10.scala
+++ b/testcases/repair/Heap/Heap10.scala
@@ -47,7 +47,7 @@ object Heaps {
}
def heapSize(t: Heap): BigInt = { t match {
- case Leaf() => 0
+ case Leaf() => BigInt(0)
case Node(v, l, r) => heapSize(l) + 1 + heapSize(r)
}} ensuring(_ >= 0)
diff --git a/testcases/repair/Heap/Heap2.scala b/testcases/repair/Heap/Heap2.scala
index 75f53a9639195f6568568346595326aa8033dbd4..175f55d194e3379cb3120d7da3cc507c6ce6b923 100644
--- a/testcases/repair/Heap/Heap2.scala
+++ b/testcases/repair/Heap/Heap2.scala
@@ -47,7 +47,7 @@ object Heaps {
}
def heapSize(t: Heap): BigInt = { t match {
- case Leaf() => 0
+ case Leaf() => BigInt(0)
case Node(v, l, r) => heapSize(l) + 1 + heapSize(r)
}} ensuring(_ >= 0)
diff --git a/testcases/repair/Heap/Heap3.scala b/testcases/repair/Heap/Heap3.scala
index b24024ea79607140b0edb47972878faf936b4dd8..5b9fadeeb819a9704aa173a9b8b1bf8b0d956d61 100644
--- a/testcases/repair/Heap/Heap3.scala
+++ b/testcases/repair/Heap/Heap3.scala
@@ -47,7 +47,7 @@ object Heaps {
}
def heapSize(t: Heap): BigInt = { t match {
- case Leaf() => 0
+ case Leaf() => BigInt(0)
case Node(v, l, r) => heapSize(l) + 1 + heapSize(r)
}} ensuring(_ >= 0)
diff --git a/testcases/repair/Heap/Heap4.scala b/testcases/repair/Heap/Heap4.scala
index d277fde61f487b8614abd9dbc4c0910d9f289520..f6176a56ae67e927c2f38d333de253b84bb25b4a 100644
--- a/testcases/repair/Heap/Heap4.scala
+++ b/testcases/repair/Heap/Heap4.scala
@@ -47,7 +47,7 @@ object Heaps {
}
def heapSize(t: Heap): BigInt = { t match {
- case Leaf() => 0
+ case Leaf() => BigInt(0)
case Node(v, l, r) => heapSize(l) + 1 + heapSize(r)
}} ensuring(_ >= 0)
diff --git a/testcases/repair/Heap/Heap5.scala b/testcases/repair/Heap/Heap5.scala
index fcddb9e089cb94b89cd2c5a2bf2f34e5bc13e3bc..5bbccada58e538033e6a12fc51ffc2683f9a1392 100644
--- a/testcases/repair/Heap/Heap5.scala
+++ b/testcases/repair/Heap/Heap5.scala
@@ -47,7 +47,7 @@ object Heaps {
}
def heapSize(t: Heap): BigInt = { t match {
- case Leaf() => 0
+ case Leaf() => BigInt(0)
case Node(v, l, r) => heapSize(l) + 1 + heapSize(r)
}} ensuring(_ >= 0)
diff --git a/testcases/repair/Heap/Heap6.scala b/testcases/repair/Heap/Heap6.scala
index aa9eb7230c57231a62f26bcf68da999eb13aeac7..2760af2fa849bf642908661a0d5c0dba276776da 100644
--- a/testcases/repair/Heap/Heap6.scala
+++ b/testcases/repair/Heap/Heap6.scala
@@ -47,7 +47,7 @@ object Heaps {
}
def heapSize(t: Heap): BigInt = { t match {
- case Leaf() => 0
+ case Leaf() => BigInt(0)
case Node(v, l, r) => heapSize(l) + 1 + heapSize(r)
}} ensuring(_ >= 0)
diff --git a/testcases/repair/Heap/Heap7.scala b/testcases/repair/Heap/Heap7.scala
index 91baf66c4dd55542e5588eafd00805f0d2a7a4e9..b2232fa7b2f59ef9af0b1cddb3d461b7f04ca91f 100644
--- a/testcases/repair/Heap/Heap7.scala
+++ b/testcases/repair/Heap/Heap7.scala
@@ -47,7 +47,7 @@ object Heaps {
}
def heapSize(t: Heap): BigInt = { t match {
- case Leaf() => 0
+ case Leaf() => BigInt(0)
case Node(v, l, r) => heapSize(l) + 1 + heapSize(r)
}} ensuring(_ >= 0)
diff --git a/testcases/repair/Heap/Heap8.scala b/testcases/repair/Heap/Heap8.scala
index 0d21fc36842a7ecf5fd6983ae7453fc072efa2dc..3debf1630a31dbcc3d36ba5c98f22f21a3551647 100644
--- a/testcases/repair/Heap/Heap8.scala
+++ b/testcases/repair/Heap/Heap8.scala
@@ -47,7 +47,7 @@ object Heaps {
}
def heapSize(t: Heap): BigInt = { t match {
- case Leaf() => 0
+ case Leaf() => BigInt(0)
case Node(v, l, r) => heapSize(l) + 1 + heapSize(r)
}} ensuring(_ >= 0)
diff --git a/testcases/repair/Heap/Heap9.scala b/testcases/repair/Heap/Heap9.scala
index 0a9197a34f46e3f7fed010fa5ea3cd4e44389d93..4ed28b8677a40779d9ea586d274808723f1e4d08 100644
--- a/testcases/repair/Heap/Heap9.scala
+++ b/testcases/repair/Heap/Heap9.scala
@@ -47,7 +47,7 @@ object Heaps {
}
def heapSize(t: Heap): BigInt = { t match {
- case Leaf() => 0
+ case Leaf() => BigInt(0)
case Node(v, l, r) => heapSize(l) + 1 + heapSize(r)
}} ensuring(_ >= 0)
diff --git a/testcases/repair/List/List.scala b/testcases/repair/List/List.scala
index 3f1e6581480d4cc1f9eb5e6009823992706c4b77..5f95f7595299a2f2c479efdb26a1b358218f55a0 100644
--- a/testcases/repair/List/List.scala
+++ b/testcases/repair/List/List.scala
@@ -9,8 +9,8 @@ import leon.annotation._
sealed abstract class List[T] {
def size: BigInt = (this match {
- case Nil() => 0
- case Cons(h, t) => 1 + t.size
+ case Nil() => BigInt(0)
+ case Cons(h, t) => BigInt(1) + t.size
}) ensuring (_ >= 0)
def content: Set[T] = this match {
diff --git a/testcases/repair/List/List1.scala b/testcases/repair/List/List1.scala
index 53a496055fa280805ada7bb5ec44253326212126..86910a60424ee14176bf3f467798cfe90e01856c 100644
--- a/testcases/repair/List/List1.scala
+++ b/testcases/repair/List/List1.scala
@@ -9,8 +9,8 @@ import leon.annotation._
sealed abstract class List[T] {
def size: BigInt = (this match {
- case Nil() => 0
- case Cons(h, t) => 1 + t.size
+ case Nil() => BigInt(0)
+ case Cons(h, t) => BigInt(1) + t.size
}) ensuring (_ >= 0)
def content: Set[T] = this match {
diff --git a/testcases/repair/List/List10.scala b/testcases/repair/List/List10.scala
index edef652eb6ca560b6ee56e2a6d7ce714c2f75e2f..61751947dc5e8c149f9c7d756af7d8458bb09655 100644
--- a/testcases/repair/List/List10.scala
+++ b/testcases/repair/List/List10.scala
@@ -9,8 +9,8 @@ import leon.annotation._
sealed abstract class List[T] {
def size: BigInt = (this match {
- case Nil() => 0
- case Cons(h, t) => 3 + t.size //FIXME
+ case Nil() => BigInt(0)
+ case Cons(h, t) => BigInt(3) + t.size //FIXME
}) ensuring { (this, _) passes {
case Cons(_, Nil()) => 1
case Nil() => 0
@@ -143,7 +143,7 @@ sealed abstract class List[T] {
Cons(h, t - e)
}
case Nil() =>
- Nil()
+ Nil[T]()
}
def --(that: List[T]): List[T] = this match {
@@ -154,7 +154,7 @@ sealed abstract class List[T] {
Cons(h, t -- that)
}
case Nil() =>
- Nil()
+ Nil[T]()
}
def &(that: List[T]): List[T] = this match {
@@ -165,7 +165,7 @@ sealed abstract class List[T] {
t & that
}
case Nil() =>
- Nil()
+ Nil[T]()
}
def pad(s: BigInt, e: T): List[T] = { (this, s) match {
diff --git a/testcases/repair/List/List11.scala b/testcases/repair/List/List11.scala
index 12eb4c6a1f027ffe8f1fd2df35944ea08bd36d79..01ea114501a40dc5f9d01740cedfca1d4198cd3e 100644
--- a/testcases/repair/List/List11.scala
+++ b/testcases/repair/List/List11.scala
@@ -9,8 +9,8 @@ import leon.annotation._
sealed abstract class List[T] {
def size: BigInt = (this match {
- case Nil() => 0
- case Cons(h, t) => 1 + t.size
+ case Nil() => BigInt(0)
+ case Cons(h, t) => BigInt(1) + t.size
}) ensuring (_ >= 0)
def content: Set[T] = this match {
@@ -331,8 +331,8 @@ object ListOps {
}
def sum(l: List[BigInt]): BigInt = { l match {
- case Nil() => 0
- case Cons(x, xs) => 1 + sum(xs) // FIXME
+ case Nil() => BigInt(0)
+ case Cons(x, xs) => BigInt(1) + sum(xs) // FIXME
}} ensuring { (l, _) passes {
case Cons(a, Nil()) => a
case Cons(a, Cons(b, Nil())) => a + b
diff --git a/testcases/repair/List/List12.scala b/testcases/repair/List/List12.scala
index 1774d1efd0b33861cf39bec63aad9eeb83cb5ad1..eeada312b1a4cd9e80ad4e735696e3e214ac6612 100644
--- a/testcases/repair/List/List12.scala
+++ b/testcases/repair/List/List12.scala
@@ -9,8 +9,8 @@ import leon.annotation._
sealed abstract class List[T] {
def size: BigInt = (this match {
- case Nil() => 0
- case Cons(h, t) => 1 + t.size
+ case Nil() => BigInt(0)
+ case Cons(h, t) => BigInt(1) + t.size
}) ensuring (_ >= 0)
def content: Set[T] = this match {
@@ -140,7 +140,7 @@ sealed abstract class List[T] {
Cons(h, t - e)
}
case Nil() =>
- Nil()
+ Nil[T]()
}} ensuring { _.content == this.content -- Set(e) }
@@ -152,7 +152,7 @@ sealed abstract class List[T] {
Cons(h, t -- that)
}
case Nil() =>
- Nil()
+ Nil[T]()
}
def &(that: List[T]): List[T] = this match {
@@ -163,7 +163,7 @@ sealed abstract class List[T] {
t & that
}
case Nil() =>
- Nil()
+ Nil[T]()
}
def pad(s: BigInt, e: T): List[T] = { (this, s) match {
diff --git a/testcases/repair/List/List13.scala b/testcases/repair/List/List13.scala
index 96dc9abcc01bce1e09f2493c34a1e1938e0ed17b..dec461f0add16ceccd63f78d7401fef0c84b9057 100644
--- a/testcases/repair/List/List13.scala
+++ b/testcases/repair/List/List13.scala
@@ -9,8 +9,8 @@ import leon.annotation._
sealed abstract class List[T] {
def size: BigInt = (this match {
- case Nil() => 0
- case Cons(h, t) => 1 + t.size
+ case Nil() => BigInt(0)
+ case Cons(h, t) => BigInt(1) + t.size
}) ensuring (_ >= 0)
def content: Set[T] = this match {
diff --git a/testcases/repair/List/List2.scala b/testcases/repair/List/List2.scala
index e5c850130597cb271e6a690e262175b507d53460..77fa7f0f99aecc37a5405d91186d63b2965ed3be 100644
--- a/testcases/repair/List/List2.scala
+++ b/testcases/repair/List/List2.scala
@@ -9,8 +9,8 @@ import leon.annotation._
sealed abstract class List[T] {
def size: BigInt = (this match {
- case Nil() => 0
- case Cons(h, t) => 1 + t.size
+ case Nil() => BigInt(0)
+ case Cons(h, t) => BigInt(1) + t.size
}) ensuring (_ >= 0)
def content: Set[T] = this match {
diff --git a/testcases/repair/List/List3.scala b/testcases/repair/List/List3.scala
index 8fc99b7d260210bdb3c985808e13fb7505a11362..5624d7db964356214dfc2ad6166f3334a7ecc4ca 100644
--- a/testcases/repair/List/List3.scala
+++ b/testcases/repair/List/List3.scala
@@ -9,8 +9,8 @@ import leon.annotation._
sealed abstract class List[T] {
def size: BigInt = (this match {
- case Nil() => 0
- case Cons(h, t) => 1 + t.size
+ case Nil() => BigInt(0)
+ case Cons(h, t) => BigInt(1) + t.size
}) ensuring (_ >= 0)
def content: Set[T] = this match {
diff --git a/testcases/repair/List/List4.scala b/testcases/repair/List/List4.scala
index d48256fe02feaac9fb7fe36980f13f2d3b61cd83..0e0aad1eec0d83a16d12f8e8e8b09ad6d7bdce99 100644
--- a/testcases/repair/List/List4.scala
+++ b/testcases/repair/List/List4.scala
@@ -9,8 +9,8 @@ import leon.annotation._
sealed abstract class List[T] {
def size: BigInt = (this match {
- case Nil() => 0
- case Cons(h, t) => 1 + t.size
+ case Nil() => BigInt(0)
+ case Cons(h, t) => BigInt(1) + t.size
}) ensuring (_ >= 0)
def content: Set[T] = this match {
@@ -79,7 +79,7 @@ sealed abstract class List[T] {
}
def drop(i: BigInt): List[T] = { (this, i) match {
- case (Nil(), _) => Nil()
+ case (Nil(), _) => Nil[T]()
case (Cons(h, t), i) =>
// FIXME
//if (i == 0) {
diff --git a/testcases/repair/List/List5.scala b/testcases/repair/List/List5.scala
index 471bff80009fa36646058205a83f0c5a8647034b..2e8099bce966a6911c44adc77c5f33291c06b24d 100644
--- a/testcases/repair/List/List5.scala
+++ b/testcases/repair/List/List5.scala
@@ -9,8 +9,8 @@ import leon.annotation._
sealed abstract class List[T] {
def size: BigInt = (this match {
- case Nil() => 0
- case Cons(h, t) => 1 + t.size
+ case Nil() => BigInt(0)
+ case Cons(h, t) => BigInt(1) + t.size
}) ensuring (_ >= 0)
def content: Set[T] = this match {
@@ -94,7 +94,7 @@ sealed abstract class List[T] {
}
def replace(from: T, to: T): List[T] = { this match {
- case Nil() => Nil()
+ case Nil() => Nil[T]()
case Cons(h, t) =>
val r = t.replace(from, to)
//if (h == from) { FIXME
diff --git a/testcases/repair/List/List6.scala b/testcases/repair/List/List6.scala
index f7881ff1ea941d683ef6e046f73e3e82c6eff2ab..1cf527cfa280387e49d64384210238a38c2e12cc 100644
--- a/testcases/repair/List/List6.scala
+++ b/testcases/repair/List/List6.scala
@@ -9,8 +9,8 @@ import leon.annotation._
sealed abstract class List[T] {
def size: BigInt = (this match {
- case Nil() => 0
- case Cons(h, t) => 1 + t.size
+ case Nil() => BigInt(0)
+ case Cons(h, t) => BigInt(1) + t.size
}) ensuring (_ >= 0)
def content: Set[T] = this match {
@@ -242,7 +242,7 @@ sealed abstract class List[T] {
t.count(e)
}
case Nil() =>
- 0
+ BigInt(0)
}} ensuring {((this, e), _) passes {
case (Cons(a, Cons(b, Cons(a1, Cons(b2, Nil())))), a2) if a == a1 && a == a2 && b != a2 && b2 != a2 => 2
case (Cons(a, Cons(b, Nil())), c) if a != c && b != c => 0
diff --git a/testcases/repair/List/List7.scala b/testcases/repair/List/List7.scala
index a67f7e5c4616e742b256aaa2d9074fd3ff986158..4a2d34262d383c70e929d3df04f00cb7b2b711d6 100644
--- a/testcases/repair/List/List7.scala
+++ b/testcases/repair/List/List7.scala
@@ -9,8 +9,8 @@ import leon.annotation._
sealed abstract class List[T] {
def size: BigInt = (this match {
- case Nil() => 0
- case Cons(h, t) => 1 + t.size
+ case Nil() => BigInt(0)
+ case Cons(h, t) => BigInt(1) + t.size
}) ensuring (_ >= 0)
def content: Set[T] = this match {
@@ -179,13 +179,13 @@ sealed abstract class List[T] {
}
def find(e: T): Option[BigInt] = { this match {
- case Nil() => None()
+ case Nil() => None[BigInt]()
case Cons(h, t) =>
if (h == e) {
- Some(0)
+ Some(BigInt(0))
} else {
t.find(e) match {
- case None() => None()
+ case None() => None[BigInt]()
case Some(i) => Some(i) // FIXME forgot +1
}
}
diff --git a/testcases/repair/List/List8.scala b/testcases/repair/List/List8.scala
index 0204d4f52e2c803ee9907f483d9a1192c0dfd3b7..3d79f043401117032505980ea6ee2b7f6d501d40 100644
--- a/testcases/repair/List/List8.scala
+++ b/testcases/repair/List/List8.scala
@@ -9,8 +9,8 @@ import leon.annotation._
sealed abstract class List[T] {
def size: BigInt = (this match {
- case Nil() => 0
- case Cons(h, t) => 1 + t.size
+ case Nil() => BigInt(0)
+ case Cons(h, t) => BigInt(1) + t.size
}) ensuring (_ >= 0)
def content: Set[T] = this match {
@@ -179,13 +179,13 @@ sealed abstract class List[T] {
}
def find(e: T): Option[BigInt] = { this match {
- case Nil() => None()
+ case Nil() => None[BigInt]()
case Cons(h, t) =>
if (h == e) {
- Some(0)
+ Some(BigInt(0))
} else {
t.find(e) match {
- case None() => None()
+ case None() => None[BigInt]()
case Some(i) => Some(i+2) // FIXME +1
}
}
diff --git a/testcases/repair/List/List9.scala b/testcases/repair/List/List9.scala
index 176cb595f29fcf632935dfd3f149ef874061103c..c9d528a945c07080469d2591563f3d6a61a4c319 100644
--- a/testcases/repair/List/List9.scala
+++ b/testcases/repair/List/List9.scala
@@ -9,8 +9,8 @@ import leon.annotation._
sealed abstract class List[T] {
def size: BigInt = (this match {
- case Nil() => 0
- case Cons(h, t) => 1 + t.size
+ case Nil() => BigInt(0)
+ case Cons(h, t) => BigInt(1) + t.size
}) ensuring (_ >= 0)
def content: Set[T] = this match {
@@ -179,13 +179,13 @@ sealed abstract class List[T] {
}
def find(e: T): Option[BigInt] = { this match {
- case Nil() => None()
+ case Nil() => None[BigInt]()
case Cons(h, t) =>
if (h != e) { // FIXME
- Some(0)
+ Some(BigInt(0))
} else {
t.find(e) match {
- case None() => None()
+ case None() => None[BigInt]()
case Some(i) => Some(i + 1)
}
}
diff --git a/testcases/repair/MergeSort/MergeSort.scala b/testcases/repair/MergeSort/MergeSort.scala
index aac638b9a6d308dcf2872f2dadb8f3c85edeeea8..1ce4210a52bbe53e911660e9c5cab4cb5dbbaf6c 100644
--- a/testcases/repair/MergeSort/MergeSort.scala
+++ b/testcases/repair/MergeSort/MergeSort.scala
@@ -6,7 +6,7 @@ object MergeSort {
case Cons(a, Cons(b, t)) =>
val (rec1, rec2) = split(t)
(Cons(a, rec1), Cons(b, rec2))
- case other => (other, Nil())
+ case other => (other, Nil[BigInt]())
}} ensuring { res =>
val (l1, l2) = res
l1.size >= l2.size &&
diff --git a/testcases/repair/MergeSort/MergeSort1.scala b/testcases/repair/MergeSort/MergeSort1.scala
index bef7f239105679afe84221f6b604e51bbd46b5e9..88b0319086023675c766cf8f6c74ccd420d2a182 100644
--- a/testcases/repair/MergeSort/MergeSort1.scala
+++ b/testcases/repair/MergeSort/MergeSort1.scala
@@ -6,7 +6,7 @@ object MergeSort {
case Cons(a, Cons(b, t)) =>
val (rec1, rec2) = split(t)
(rec1, rec2) // FIXME: Forgot a,b
- case other => (other, Nil())
+ case other => (other, Nil[BigInt]())
}} ensuring { res =>
val (l1, l2) = res
l1.size >= l2.size &&
diff --git a/testcases/repair/MergeSort/MergeSort2.scala b/testcases/repair/MergeSort/MergeSort2.scala
index 11c3a1cdb2af326c103d48db512987a70346b862..5c186eca76861f679e67e046c987bebd2951ac97 100644
--- a/testcases/repair/MergeSort/MergeSort2.scala
+++ b/testcases/repair/MergeSort/MergeSort2.scala
@@ -6,7 +6,7 @@ object MergeSort {
case Cons(a, Cons(b, t)) =>
val (rec1, rec2) = split(t)
(Cons(a, rec1), Cons(b, rec2))
- case other => (other, Nil())
+ case other => (other, Nil[BigInt]())
}} ensuring { res =>
val (l1, l2) = res
l1.size >= l2.size &&
diff --git a/testcases/repair/MergeSort/MergeSort3.scala b/testcases/repair/MergeSort/MergeSort3.scala
index 3d9c8192a0c4584bbc16c88055f8693e460a4609..ec37db65c053e3ae3db8871640f516747b7da08d 100644
--- a/testcases/repair/MergeSort/MergeSort3.scala
+++ b/testcases/repair/MergeSort/MergeSort3.scala
@@ -6,7 +6,7 @@ object MergeSort {
case Cons(a, Cons(b, t)) =>
val (rec1, rec2) = split(t)
(Cons(a, rec1), Cons(b, rec2))
- case other => (other, Nil())
+ case other => (other, Nil[BigInt]())
}} ensuring { res =>
val (l1, l2) = res
l1.size >= l2.size &&
diff --git a/testcases/repair/MergeSort/MergeSort4.scala b/testcases/repair/MergeSort/MergeSort4.scala
index 4422402b187f1e8fec33825369489f223af7e559..5c3479844d213bf8617f72f9e5dd6aec127f59b2 100644
--- a/testcases/repair/MergeSort/MergeSort4.scala
+++ b/testcases/repair/MergeSort/MergeSort4.scala
@@ -6,7 +6,7 @@ object MergeSort {
case Cons(a, Cons(b, t)) =>
val (rec1, rec2) = split(t)
(Cons(a, rec1), Cons(b, rec2))
- case other => (other, Nil())
+ case other => (other, Nil[BigInt]())
}} ensuring { res =>
val (l1, l2) = res
l1.size >= l2.size &&
diff --git a/testcases/repair/MergeSort/MergeSort5.scala b/testcases/repair/MergeSort/MergeSort5.scala
index 1bf9d50ce3279e5fd6b1876b3c51e4c3bd249fe4..7746d23c7fa58e3e3c60c7ff4e9fe2c62fc8f3a9 100644
--- a/testcases/repair/MergeSort/MergeSort5.scala
+++ b/testcases/repair/MergeSort/MergeSort5.scala
@@ -6,7 +6,7 @@ object MergeSort {
case Cons(a, Cons(b, t)) =>
val (rec1, rec2) = split(t)
(Cons(a, rec1), Cons(b, rec2))
- case other => (other, Nil())
+ case other => (other, Nil[BigInt]())
}} ensuring { res =>
val (l1, l2) = res
l1.size >= l2.size &&
diff --git a/testcases/repair/PropLogic/PropLogic.scala b/testcases/repair/PropLogic/PropLogic.scala
index 2819234ff176f4b0bac2e2b781397dda49edef53..a03dd35b47d7b9abed256a13f9168c8afe666ff0 100644
--- a/testcases/repair/PropLogic/PropLogic.scala
+++ b/testcases/repair/PropLogic/PropLogic.scala
@@ -15,7 +15,7 @@ object SemanticsPreservation {
case And(l,r) => 1 + size(l) + size(r)
case Or(l,r) => 1 + size(l) + size(r)
case Not(e) => 1 + size(e)
- case _ => 1
+ case _ => BigInt(1)
}} ensuring { _ >= 0 }
def eval(formula: Formula)(implicit trueVars : Set[BigInt]): Boolean = formula match {
diff --git a/testcases/repair/PropLogic/PropLogic1.scala b/testcases/repair/PropLogic/PropLogic1.scala
index 93cd6bfbf947c019538deeaaa3620a26f04e7d57..a27d3afe5d0e20668e72ec654c91714bc0aa88a1 100644
--- a/testcases/repair/PropLogic/PropLogic1.scala
+++ b/testcases/repair/PropLogic/PropLogic1.scala
@@ -15,7 +15,7 @@ object SemanticsPreservation {
case And(l,r) => 1 + size(l) + size(r)
case Or(l,r) => 1 + size(l) + size(r)
case Not(e) => 1 + size(e)
- case _ => 1
+ case _ => BigInt(1)
}} ensuring { _ >= 0 }
def eval(formula: Formula)(implicit trueVars : Set[BigInt]): Boolean = formula match {
diff --git a/testcases/repair/PropLogic/PropLogic2.scala b/testcases/repair/PropLogic/PropLogic2.scala
index 2819234ff176f4b0bac2e2b781397dda49edef53..a03dd35b47d7b9abed256a13f9168c8afe666ff0 100644
--- a/testcases/repair/PropLogic/PropLogic2.scala
+++ b/testcases/repair/PropLogic/PropLogic2.scala
@@ -15,7 +15,7 @@ object SemanticsPreservation {
case And(l,r) => 1 + size(l) + size(r)
case Or(l,r) => 1 + size(l) + size(r)
case Not(e) => 1 + size(e)
- case _ => 1
+ case _ => BigInt(1)
}} ensuring { _ >= 0 }
def eval(formula: Formula)(implicit trueVars : Set[BigInt]): Boolean = formula match {
diff --git a/testcases/repair/PropLogic/PropLogic3.scala b/testcases/repair/PropLogic/PropLogic3.scala
index 8f2a62cd8273ed7ee613891de72f567812b4a806..87d78dbc98ae5e4dbbd163f6336e3e8428adbdbc 100644
--- a/testcases/repair/PropLogic/PropLogic3.scala
+++ b/testcases/repair/PropLogic/PropLogic3.scala
@@ -15,7 +15,7 @@ object SemanticsPreservation {
case And(l,r) => 1 + size(l) + size(r)
case Or(l,r) => 1 + size(l) + size(r)
case Not(e) => 1 + size(e)
- case _ => 1
+ case _ => BigInt(1)
}} ensuring { _ >= 0 }
def eval(formula: Formula)(implicit trueVars : Set[BigInt]): Boolean = formula match {
diff --git a/testcases/repair/PropLogic/PropLogic4.scala b/testcases/repair/PropLogic/PropLogic4.scala
index 40cddee807cbba06e33cfe51028a9be7fa6e1a87..29e1c5783d1c8c675c848b9b0101d59539bf71bb 100644
--- a/testcases/repair/PropLogic/PropLogic4.scala
+++ b/testcases/repair/PropLogic/PropLogic4.scala
@@ -15,7 +15,7 @@ object SemanticsPreservation {
case And(l,r) => 1 + size(l) + size(r)
case Or(l,r) => 1 + size(l) + size(r)
case Not(e) => 1 + size(e)
- case _ => 1
+ case _ => BigInt(1)
}} ensuring { _ >= 0 }
def eval(formula: Formula)(implicit trueVars : Set[BigInt]): Boolean = formula match {
diff --git a/testcases/repair/PropLogic/PropLogic5.scala b/testcases/repair/PropLogic/PropLogic5.scala
index 6b24d992663541e6a22fb61ca44520ce0291544f..e89e2c5ae2cfda30e73743aab932f980a95fa46f 100644
--- a/testcases/repair/PropLogic/PropLogic5.scala
+++ b/testcases/repair/PropLogic/PropLogic5.scala
@@ -15,7 +15,7 @@ object SemanticsPreservation {
case And(l,r) => 1 + size(l) + size(r)
case Or(l,r) => 1 + size(l) + size(r)
case Not(e) => 1 + size(e)
- case _ => 1
+ case _ => BigInt(1)
}} ensuring { _ >= 0 }
def eval(formula: Formula)(implicit trueVars : Set[BigInt]): Boolean = formula match {
diff --git a/testcases/repair/inria/FirstIndexOf.scala b/testcases/repair/inria/FirstIndexOf.scala
index 2693d18cd62cdcb52ef924343f47d2c349633ca8..3239632e45a4d15c24f44dea3ee735077690e697 100644
--- a/testcases/repair/inria/FirstIndexOf.scala
+++ b/testcases/repair/inria/FirstIndexOf.scala
@@ -6,15 +6,15 @@ import leon.lang.synthesis._
object FirstIndexOf {
def firstIndexOf(l: List[Int], v: Int): BigInt = {
l match {
- case Cons(h, t) if v == h => 0
+ case Cons(h, t) if v == h => BigInt(0)
case Cons(h, t) =>
if (firstIndexOf(t, v) >= 0) {
firstIndexOf(t, v)+1
} else {
- -1
+ BigInt(-1)
}
case Nil() =>
- -1
+ BigInt(-1)
}
} ensuring {
(res: BigInt) => (if (l.content contains v) {
diff --git a/testcases/verification/Addresses.scala b/testcases/verification/Addresses.scala
index 4eebe934f3f75e11d5d5edb70e8a228d0f000ae6..b6f356fe2a58068847d325071b3959cf25a7d862 100644
--- a/testcases/verification/Addresses.scala
+++ b/testcases/verification/Addresses.scala
@@ -55,7 +55,7 @@ object Addresses {
def max(x:BigInt,y:BigInt) = if (x <= y) x else y
def collectA(x:BigInt,l:List) : (BigInt,BigInt,List) = (l match {
- case Nil() => (0,0,Nil())
+ case Nil() => (BigInt(0),BigInt(0),Nil())
case Cons(a,b,c,l1) if (a==x) => {
val (b2,c2,l2) = collectA(x,l1)
(max(b,b2),max(c,c2),l2)
diff --git a/testcases/verification/higher-order/invalid/Lists2.scala b/testcases/verification/higher-order/invalid/Lists2.scala
index 59faa779becb2c58ec638a4d26621a8b24dca9c4..29285c8a91ccf3f163595fb38028b72b172fd59d 100644
--- a/testcases/verification/higher-order/invalid/Lists2.scala
+++ b/testcases/verification/higher-order/invalid/Lists2.scala
@@ -35,7 +35,7 @@ object Lists2 {
val (tres, sres) = bubble(t1)
(Cons(h1, tres), sres)
case Nil() =>
- (Nil(), false)
+ (Nil[A](), false)
}
} ensuring { _ match {
/*res =>
diff --git a/testcases/verification/higher-order/valid/ListOps1.scala b/testcases/verification/higher-order/valid/ListOps1.scala
index 59903df08b50d9a60ea9e4d0343ede7061e57ad8..8d02e9bea274559aa4cf27bfd738a821f1068e9d 100644
--- a/testcases/verification/higher-order/valid/ListOps1.scala
+++ b/testcases/verification/higher-order/valid/ListOps1.scala
@@ -33,7 +33,7 @@ object ListOps1 {
case Some(b) => Cons(b, collect(f, t))
case None() => collect(f, t)
}
- case Nil() => Nil()
+ case Nil() => Nil[B]()
}
} ensuring {
res => res.size <= l.size
@@ -43,7 +43,7 @@ object ListOps1 {
l match {
case Cons(h, t) =>
f(h).orElse(collectFirst(f, t))
- case Nil() => None()
+ case Nil() => None[B]()
}
} ensuring {
res => !l.isEmpty || res.isEmpty
@@ -64,7 +64,7 @@ object ListOps1 {
l match {
case Cons(h, t) if f(h) => dropWhile(f, t)
case Cons(h, t) if !f(h) => l
- case Nil() => Nil()
+ case Nil() => Nil[A]()
}
} ensuring {
res =>
@@ -103,7 +103,7 @@ object ListOps1 {
def mapWitness[A,B](f: A => B, l: List[A], w: A): List[B] = {
l match {
case Cons(h, t) => f(h) :: mapWitness(f, t, w)
- case Nil() => Nil()
+ case Nil() => Nil[B]()
}
} ensuring {
res => if (l.content contains w) res.content contains f(w) else true
diff --git a/testcases/verification/list-algorithms/TwoSizeFunctions.scala b/testcases/verification/list-algorithms/TwoSizeFunctions.scala
index b5583a70771f363695d144ed16e99315717eccc0..b28e5456160468696ab73e8ea31e9469749e0778 100644
--- a/testcases/verification/list-algorithms/TwoSizeFunctions.scala
+++ b/testcases/verification/list-algorithms/TwoSizeFunctions.scala
@@ -8,7 +8,7 @@ object TwoSizeFunctions {
def size1(l: List) : BigInt = (l match {
case Cons(_, xs) => size1(xs) + 1
- case Nil() => 0
+ case Nil() => BigInt(0)
}) ensuring(_ >= 0)
def size2(l: List) : BigInt = size2acc(l, 0)
diff --git a/testcases/verification/math/Fibonacci.scala b/testcases/verification/math/Fibonacci.scala
index df2b731c5830734f95365f39e7ee7a5f93dbea44..82e3483dbf30f693e13f0d31370d673456026aca 100644
--- a/testcases/verification/math/Fibonacci.scala
+++ b/testcases/verification/math/Fibonacci.scala
@@ -18,7 +18,7 @@ object Fibonacci {
def f(n : BigInt) : BigInt = {
require(n >= 0)
if(n <= 0)
- 1
+ BigInt(1)
else
f(n-1) + g(n-1)
}
@@ -26,7 +26,7 @@ object Fibonacci {
def g(n : BigInt) : BigInt = {
require(n >= 0)
if(n <= 0)
- 1
+ BigInt(1)
else
f(n-1)
} ensuring(_ == fib(n + 1))
diff --git a/testcases/web/demos/02_Lists.scala b/testcases/web/demos/02_Lists.scala
index f4abad115e3cc0f5e1908884f0088c3e21021010..59d3175ba803a0cfcffaf4dac80a3f9521e3681a 100644
--- a/testcases/web/demos/02_Lists.scala
+++ b/testcases/web/demos/02_Lists.scala
@@ -8,7 +8,7 @@ object List {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
+ case Nil => BigInt(0)
case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
diff --git a/testcases/web/demos/03_Splits.scala b/testcases/web/demos/03_Splits.scala
index 740dc34a8cf6ce680b3807779ee70fb97c3fa635..a2bb904d05681d022d698b16f0470d8e5c11bec3 100644
--- a/testcases/web/demos/03_Splits.scala
+++ b/testcases/web/demos/03_Splits.scala
@@ -8,7 +8,7 @@ object List {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
+ case Nil => BigInt(0)
case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
diff --git a/testcases/web/demos/05_OpenDays2.scala b/testcases/web/demos/05_OpenDays2.scala
index c092735fa3dfd3f5fab9b6f93d49991895ce30b4..480d0208070d85f85ca0287de911f976f97e655d 100644
--- a/testcases/web/demos/05_OpenDays2.scala
+++ b/testcases/web/demos/05_OpenDays2.scala
@@ -40,7 +40,7 @@ object EpflOpenDays {
sealed abstract class Liste {
def somme: BigInt = {
this match {
- case Vide => 0
+ case Vide => BigInt(0)
case Elem(p, reste) => p.valeur + reste.somme
}
} ensuring { _ >= 0 }
diff --git a/testcases/web/sav15/03_Exercise3.scala b/testcases/web/sav15/03_Exercise3.scala
index 4dff97756cb94f21b7379c2038d9d323eb14e6aa..ca9d23efbe4a22cf6cdb1fa355da16de65702dbb 100644
--- a/testcases/web/sav15/03_Exercise3.scala
+++ b/testcases/web/sav15/03_Exercise3.scala
@@ -6,7 +6,7 @@ object ListWithSize {
def size: BigInt = {
this match {
case Cons(h, t) => 1 + t.size
- case Nil() => 0
+ case Nil() => BigInt(0)
}
} // TODO: Add appropriate post-condition
@@ -24,7 +24,7 @@ object ListWithSize {
def zip[U](that: List[U]): List[(T, U)] = {
// TODO: Add appropriate pre-condition
this match {
- case Nil() => Nil()
+ case Nil() => Nil[(T,U)]()
case Cons(h1, t1) => that match {
case Cons(h2, t2) => Cons((h1, h2), t1.zip(t2))
}
@@ -70,7 +70,7 @@ object ListWithSize {
}.holds
def drunk[T](l: List[T]): List[T] = (l match {
- case Nil() => Nil()
+ case Nil() => Nil[T]()
case Cons(x,l1) => Cons(x,Cons(x,drunk(l1)))
}) ensuring {
res => true // TODO: find postcondition
diff --git a/testcases/web/sav15/05_Exercise5.scala b/testcases/web/sav15/05_Exercise5.scala
index 787ab6de2f8ce304734c0c31fda5ac22695606ba..a76401c2622bc4cec14b4703e43f01bd8eca4db4 100644
--- a/testcases/web/sav15/05_Exercise5.scala
+++ b/testcases/web/sav15/05_Exercise5.scala
@@ -5,7 +5,7 @@ object SearchList {
sealed abstract class List[T] {
def size: BigInt = {
this match {
- case Nil() => 0
+ case Nil() => BigInt(0)
case Cons(h, t) => 1 + t.size
}
} ensuring { _ >= 0 }
@@ -19,8 +19,8 @@ object SearchList {
def firstPosOf(v: T): BigInt = {
this match {
- case Nil() => -1
- case Cons(h, t) if h == v => 0
+ case Nil() => BigInt(-1)
+ case Cons(h, t) if h == v => BigInt(0)
case Cons(h, t) =>
val p = t.firstPosOf(v)
if (p >= 0) {
@@ -37,8 +37,8 @@ object SearchList {
def take(n: BigInt): List[T] = {
require(n >= 0)
this match {
- case Nil() => Nil()
- case Cons(h, t) if n == 0 => Nil()
+ case Nil() => Nil[T]()
+ case Cons(h, t) if n == 0 => Nil[T]()
case Cons(h, t) => Cons(h, t.take(n - 1))
}
} ensuring {
diff --git a/testcases/web/sav15/06_Exercise6.scala b/testcases/web/sav15/06_Exercise6.scala
index 636abaca00477c95a0b0d195690f54f49ee0d1e1..01aa1d62a13eeb7bc0b7da2fb7268277177323d1 100644
--- a/testcases/web/sav15/06_Exercise6.scala
+++ b/testcases/web/sav15/06_Exercise6.scala
@@ -26,7 +26,7 @@ object BinaryTree {
def size: BigInt = {
this match {
- case Empty => 0
+ case Empty => BigInt(0)
case Node(l, _, r) => l.size + r.size + 1
}
} ensuring { _ >= 0 }
@@ -68,7 +68,7 @@ object BinaryTree {
def toList: List[BigInt] = {
require(isBT)
- Nil() // TODO
+ Nil[BigInt]() // TODO
} ensuring {
res => res.content == this.content && isSorted(res)
}
diff --git a/testcases/web/synthesis/01_List_Insert.scala b/testcases/web/synthesis/01_List_Insert.scala
index 62e91d9b92c1d87008d1192f2f9e5c68580ef1ec..40b7b0c74411d4912d45006f539d0defba125a17 100644
--- a/testcases/web/synthesis/01_List_Insert.scala
+++ b/testcases/web/synthesis/01_List_Insert.scala
@@ -8,8 +8,8 @@ object Insert {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/testcases/web/synthesis/02_List_Delete.scala b/testcases/web/synthesis/02_List_Delete.scala
index a548f46e2507bc4e95754bd1d512175260af1a49..8230af747b9aba872e2281ff1c9cd630b962a7be 100644
--- a/testcases/web/synthesis/02_List_Delete.scala
+++ b/testcases/web/synthesis/02_List_Delete.scala
@@ -8,8 +8,8 @@ object Delete {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/testcases/web/synthesis/03_List_Union.scala b/testcases/web/synthesis/03_List_Union.scala
index 0b21dc0375c63b438f810acb9bdcd4f04ef25b36..b03d4e5a24f18daabb07226d94801bbbd7920163 100644
--- a/testcases/web/synthesis/03_List_Union.scala
+++ b/testcases/web/synthesis/03_List_Union.scala
@@ -8,8 +8,8 @@ object Union {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/testcases/web/synthesis/04_List_Diff.scala b/testcases/web/synthesis/04_List_Diff.scala
index 0943955b170124ef788132a529ae0dd7ee9b55bb..775d440833bf5b545dcb699d041554871a3de669 100644
--- a/testcases/web/synthesis/04_List_Diff.scala
+++ b/testcases/web/synthesis/04_List_Diff.scala
@@ -8,8 +8,8 @@ object Diff {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/testcases/web/synthesis/05_List_Split1.scala b/testcases/web/synthesis/05_List_Split1.scala
index facbda843c5a6349cc6efca052bf104ec63f7156..1838a6bb0471df20c25e3d2ad94d85ef80fa1362 100644
--- a/testcases/web/synthesis/05_List_Split1.scala
+++ b/testcases/web/synthesis/05_List_Split1.scala
@@ -8,8 +8,8 @@ object List {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/testcases/web/synthesis/06_List_Split2.scala b/testcases/web/synthesis/06_List_Split2.scala
index 38c07caf52566eb6f599e2557900b1ed83a53c37..0b917467f8eeb2ec0ba6e3251813e18a56369058 100644
--- a/testcases/web/synthesis/06_List_Split2.scala
+++ b/testcases/web/synthesis/06_List_Split2.scala
@@ -8,8 +8,8 @@ object List {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/testcases/web/synthesis/07_List_Split3.scala b/testcases/web/synthesis/07_List_Split3.scala
index 15c74190e1839abb484b375b28fea1582d8d58ea..8a7897ebbb25faea765cd4487ef33fe54d144fba 100644
--- a/testcases/web/synthesis/07_List_Split3.scala
+++ b/testcases/web/synthesis/07_List_Split3.scala
@@ -8,8 +8,8 @@ object List {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/testcases/web/synthesis/09_SortedList_Insert1.scala b/testcases/web/synthesis/09_SortedList_Insert1.scala
index affc5b45512a0383b49d11ca2c008df3d28b8d06..891c55cae60d9f07e3a949dfacb6e1264763dda4 100644
--- a/testcases/web/synthesis/09_SortedList_Insert1.scala
+++ b/testcases/web/synthesis/09_SortedList_Insert1.scala
@@ -8,8 +8,8 @@ object Complete {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/testcases/web/synthesis/10_SortedList_Insert2.scala b/testcases/web/synthesis/10_SortedList_Insert2.scala
index e44eac286849ac69c19991168398ffad67726f5d..a199c7f28b8198c8b4644cf177919b4e6c16fd7d 100644
--- a/testcases/web/synthesis/10_SortedList_Insert2.scala
+++ b/testcases/web/synthesis/10_SortedList_Insert2.scala
@@ -8,8 +8,8 @@ object Complete {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/testcases/web/synthesis/11_SortedList_Delete.scala b/testcases/web/synthesis/11_SortedList_Delete.scala
index 31305ca094ec78fa6896985fad04729879839baf..1438555d16120a19d43adb87b2320a6759d584be 100644
--- a/testcases/web/synthesis/11_SortedList_Delete.scala
+++ b/testcases/web/synthesis/11_SortedList_Delete.scala
@@ -8,8 +8,8 @@ object Complete {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/testcases/web/synthesis/12_SortedList_Diff.scala b/testcases/web/synthesis/12_SortedList_Diff.scala
index 9e4e32baeebb42ca25bd4dfec41e7b0303c80f53..33d5dc69339048baa2b9e3c178a2c415ec86cb98 100644
--- a/testcases/web/synthesis/12_SortedList_Diff.scala
+++ b/testcases/web/synthesis/12_SortedList_Diff.scala
@@ -8,8 +8,8 @@ object Complete {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/testcases/web/synthesis/13_SortedList_InsertSort.scala b/testcases/web/synthesis/13_SortedList_InsertSort.scala
index 8f5b78247b9877952f9a7e17cdf507f424d16b05..5f4076ac08c4942029549e41d6e56998b79e563e 100644
--- a/testcases/web/synthesis/13_SortedList_InsertSort.scala
+++ b/testcases/web/synthesis/13_SortedList_InsertSort.scala
@@ -8,8 +8,8 @@ object Complete {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/testcases/web/synthesis/14_SortedList_Union.scala b/testcases/web/synthesis/14_SortedList_Union.scala
index 95d17bb61bb48927a2d189ccecf1b7330b4bb46e..a5c4de9c6501de2549cd25257aa0e81294d38342 100644
--- a/testcases/web/synthesis/14_SortedList_Union.scala
+++ b/testcases/web/synthesis/14_SortedList_Union.scala
@@ -8,8 +8,8 @@ object Complete {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/testcases/web/synthesis/15_StrictSortedList_Insert.scala b/testcases/web/synthesis/15_StrictSortedList_Insert.scala
index 6c7543ad3847671bfc8657dc5c99e2bbd236ed93..378ae688eee95f8f17bab2cd56e81d68107e6fc7 100644
--- a/testcases/web/synthesis/15_StrictSortedList_Insert.scala
+++ b/testcases/web/synthesis/15_StrictSortedList_Insert.scala
@@ -8,8 +8,8 @@ object Complete {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/testcases/web/synthesis/16_StrictSortedList_Delete.scala b/testcases/web/synthesis/16_StrictSortedList_Delete.scala
index 81827ed03b80beddf664e2b0c2beb62a43dad078..6a79ccc11b28cf5ebbc8dfcecb519a896f8d37d4 100644
--- a/testcases/web/synthesis/16_StrictSortedList_Delete.scala
+++ b/testcases/web/synthesis/16_StrictSortedList_Delete.scala
@@ -8,8 +8,8 @@ object Delete {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/testcases/web/synthesis/17_StrictSortedList_Union.scala b/testcases/web/synthesis/17_StrictSortedList_Union.scala
index cf2fcd727323d6b5c705522f3d37b884bdfd896d..c4e7d45e0e55eb41a5bc8bb07cc17e2cf959b86a 100644
--- a/testcases/web/synthesis/17_StrictSortedList_Union.scala
+++ b/testcases/web/synthesis/17_StrictSortedList_Union.scala
@@ -8,8 +8,8 @@ object Complete {
case object Nil extends List
def size(l: List) : BigInt = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => BigInt(0)
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[BigInt] = l match {
diff --git a/testcases/web/synthesis/18_UnaryNumerals_Add.scala b/testcases/web/synthesis/18_UnaryNumerals_Add.scala
index 694f76a15a00b1fc666b372336f3d7baaa6b77d7..7bf58114b5c9f4cdeb008f1220af9ab6a7139dac 100644
--- a/testcases/web/synthesis/18_UnaryNumerals_Add.scala
+++ b/testcases/web/synthesis/18_UnaryNumerals_Add.scala
@@ -9,7 +9,7 @@ object Numerals {
def value(n: Num): BigInt = {
n match {
- case Z => 0
+ case Z => BigInt(0)
case S(p) => 1 + value(p)
}
} ensuring (_ >= 0)
diff --git a/testcases/web/synthesis/19_UnaryNumerals_Distinct.scala b/testcases/web/synthesis/19_UnaryNumerals_Distinct.scala
index 827d8d70f8f5a860447897e86f62d5f5f19d529d..d41ef8a03d03782707e993d82e18e11c87f82405 100644
--- a/testcases/web/synthesis/19_UnaryNumerals_Distinct.scala
+++ b/testcases/web/synthesis/19_UnaryNumerals_Distinct.scala
@@ -9,7 +9,7 @@ object Numerals {
def value(n: Num): BigInt = {
n match {
- case Z => 0
+ case Z => BigInt(0)
case S(p) => 1 + value(p)
}
} ensuring (_ >= 0)
diff --git a/testcases/web/synthesis/20_UnaryNumerals_Mult.scala b/testcases/web/synthesis/20_UnaryNumerals_Mult.scala
index 1e58606d07d6bb78de617fa90d6129052007624b..800812e5714e468bdc0bf320dd6491c0e9e4304c 100644
--- a/testcases/web/synthesis/20_UnaryNumerals_Mult.scala
+++ b/testcases/web/synthesis/20_UnaryNumerals_Mult.scala
@@ -9,7 +9,7 @@ object Numerals {
def value(n: Num): BigInt = {
n match {
- case Z => 0
+ case Z => BigInt(0)
case S(p) => 1 + value(p)
}
} ensuring (_ >= 0)
diff --git a/testcases/web/synthesis/21_UnaryNumerals_Squared.scala b/testcases/web/synthesis/21_UnaryNumerals_Squared.scala
index d660c247ea4c68993dd4d59a7fc0f61e913935bc..9dd48fbc1e6d60b0bfe70e8d70fe3fdc6d8f36f7 100644
--- a/testcases/web/synthesis/21_UnaryNumerals_Squared.scala
+++ b/testcases/web/synthesis/21_UnaryNumerals_Squared.scala
@@ -9,7 +9,7 @@ object Numerals {
def value(n:Num) : BigInt = {
n match {
- case Z => 0
+ case Z => BigInt(0)
case S(p) => 1 + value(p)
}
} ensuring (_ >= 0)
diff --git a/testcases/web/verification/01_Amortized_Queue.scala b/testcases/web/verification/01_Amortized_Queue.scala
index e8190385a15d2bba453571671778d1e01850eeb0..e67f9c4c937ae70b1ea2b1a97f129eda49d0a167 100644
--- a/testcases/web/verification/01_Amortized_Queue.scala
+++ b/testcases/web/verification/01_Amortized_Queue.scala
@@ -10,7 +10,7 @@ object AmortizedQueue {
case class Queue(front : List, rear : List) extends AbsQueue
def size(list : List) : BigInt = (list match {
- case Nil => 0
+ case Nil => BigInt(0)
case Cons(_, xs) => 1 + size(xs)
}) ensuring(_ >= 0)
diff --git a/testcases/web/verification/03_Insertion_Sort.scala b/testcases/web/verification/03_Insertion_Sort.scala
index a3a81d75338fdb5456664ce4e663101deb4cce02..e53b89b1732bed1dfb1c1389feacc70d4490285d 100644
--- a/testcases/web/verification/03_Insertion_Sort.scala
+++ b/testcases/web/verification/03_Insertion_Sort.scala
@@ -11,7 +11,7 @@ object InsertionSort {
case object None extends OptInt
def size(l : List) : BigInt = (l match {
- case Nil => 0
+ case Nil => BigInt(0)
case Cons(_, xs) => 1 + size(xs)
}) ensuring(_ >= 0)
diff --git a/testcases/web/verification/04_List_Operations.scala b/testcases/web/verification/04_List_Operations.scala
index f7e6d590c25882d51a51191547b03b3996dad8d1..982b0cefb73805929e2e4a81f9a7e9e328e989ca 100644
--- a/testcases/web/verification/04_List_Operations.scala
+++ b/testcases/web/verification/04_List_Operations.scala
@@ -14,12 +14,12 @@ object ListOperations {
case class IP(fst: BigInt, snd: BigInt) extends IntPair
def size(l: List) : BigInt = (l match {
- case Nil => 0
+ case Nil => BigInt(0)
case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def iplSize(l: IntPairList) : BigInt = (l match {
- case IPNil => 0
+ case IPNil => BigInt(0)
case IPCons(_, xs) => 1 + iplSize(xs)
}) ensuring(_ >= 0)
diff --git a/testcases/web/verification/06_Red-Black_Tree.scala b/testcases/web/verification/06_Red-Black_Tree.scala
index 3adc6c8cb60135e6465d1f13da87a8baca24ce61..9a9553146ef799a91649363c8dbda140f772379d 100644
--- a/testcases/web/verification/06_Red-Black_Tree.scala
+++ b/testcases/web/verification/06_Red-Black_Tree.scala
@@ -20,7 +20,7 @@ object RedBlackTree {
}
def size(t: Tree) : BigInt = t match {
- case Empty => 0
+ case Empty => BigInt(0)
case Node(_, l, v, r) => size(l) + 1 + size(r)
}
diff --git a/testcases/web/verification/07_Search_Linked-List.scala b/testcases/web/verification/07_Search_Linked-List.scala
index 16f1c550e6c620bce328e2ec31e5312838af0cfc..8d743bd21791f50383ade1c933b0ff2f0b57a20e 100644
--- a/testcases/web/verification/07_Search_Linked-List.scala
+++ b/testcases/web/verification/07_Search_Linked-List.scala
@@ -7,7 +7,7 @@ object SearchLinkedList {
case object Nil extends List
def size(list : List) : BigInt = (list match {
- case Nil => 0
+ case Nil => BigInt(0)
case Cons(_, xs) => 1 + size(xs)
}) ensuring(_ >= 0)
@@ -17,8 +17,8 @@ object SearchLinkedList {
})
def firstZero(list : List) : BigInt = (list match {
- case Nil => 0
- case Cons(x, xs) => if (x == 0) 0 else firstZero(xs) + 1
+ case Nil => BigInt(0)
+ case Cons(x, xs) => if (x == 0) BigInt(0) else firstZero(xs) + 1
}) ensuring (res =>
res >= 0 && (if (contains(list, 0)) {
firstZeroAtPos(list, res)
diff --git a/testcases/web/verification/08_Sum_and_Max.scala b/testcases/web/verification/08_Sum_and_Max.scala
index 24d279515cdbc7fe7d3e3f6f056be53d25df61eb..9dcc6d333c1c8015581ae2ba1879030220dc9772 100644
--- a/testcases/web/verification/08_Sum_and_Max.scala
+++ b/testcases/web/verification/08_Sum_and_Max.scala
@@ -18,12 +18,12 @@ object SumAndMax {
}
def sum(list : List) : BigInt = list match {
- case Nil => 0
+ case Nil => BigInt(0)
case Cons(x, xs) => x + sum(xs)
}
def size(list : List) : BigInt = (list match {
- case Nil => 0
+ case Nil => BigInt(0)
case Cons(_, xs) => 1 + size(xs)
}) ensuring(_ >= 0)
diff --git a/testcases/web/verification/14_HeapSort.scala b/testcases/web/verification/14_HeapSort.scala
index 22d9d55f361d6f1d81d0b243cb381b4eeb003351..4537664e7b89a6ae51488843192f353d45d4ba6b 100644
--- a/testcases/web/verification/14_HeapSort.scala
+++ b/testcases/web/verification/14_HeapSort.scala
@@ -8,7 +8,7 @@ object HeapSort {
def rightHeight(h: Heap): BigInt = {
h match {
- case Leaf() => 0
+ case Leaf() => BigInt(0)
case Node(_, _, _, r) => rightHeight(r) + 1
}
} ensuring (_ >= 0)
@@ -40,7 +40,7 @@ object HeapSort {
def heapSize(t: Heap): BigInt = {
(t match {
- case Leaf() => 0
+ case Leaf() => BigInt(0)
case Node(_, v, l, r) => heapSize(l) + 1 + heapSize(r)
})
} ensuring (_ >= 0)
diff --git a/testcases/web/verification/15_LeftistHeap.scala b/testcases/web/verification/15_LeftistHeap.scala
index 356af0154f146e89217f94db3b668b45a61b1dde..9ab1a583afb739cdd079c8014ad0c897cc87b7f6 100644
--- a/testcases/web/verification/15_LeftistHeap.scala
+++ b/testcases/web/verification/15_LeftistHeap.scala
@@ -8,7 +8,7 @@ object HeapSort {
def rightHeight(h: Heap): BigInt = {
h match {
- case Leaf() => 0
+ case Leaf() => BigInt(0)
case Node(_, _, _, r) => rightHeight(r) + 1
}
} ensuring (_ >= 0)
@@ -40,7 +40,7 @@ object HeapSort {
def heapSize(t: Heap): BigInt = {
(t match {
- case Leaf() => 0
+ case Leaf() => BigInt(0)
case Node(_, v, l, r) => heapSize(l) + 1 + heapSize(r)
})
} ensuring (_ >= 0)
@@ -117,7 +117,7 @@ object HeapSort {
def heapElements(t: Heap): List[BigInt] = {
require(hasLeftistProperty(t))
t match {
- case Leaf() => Nil()
+ case Leaf() => Nil[BigInt]()
case Node(_, v, l, r) =>
v :: append(heapElements(l), heapElements(r))
}