diff --git a/src/test/resources/regression/repair/Compiler1.scala b/src/test/resources/regression/repair/Compiler1.scala
index 06d893489b5ebbe4379622194410e496c840bd76..9ff0785d70b9080327890a5af4729a59f5c41edd 100644
--- a/src/test/resources/regression/repair/Compiler1.scala
+++ b/src/test/resources/regression/repair/Compiler1.scala
@@ -15,7 +15,7 @@ object Trees {
case class Not(e : Expr) extends Expr
case class Eq(lhs: Expr, rhs: Expr) extends Expr
case class Ite(cond: Expr, thn: Expr, els: Expr) extends Expr
- case class IntLiteral(v: Int) extends Expr
+ case class IntLiteral(v: BigInt) extends Expr
case class BoolLiteral(b : Boolean) extends Expr
}
@@ -76,14 +76,14 @@ object Semantics {
import Types._
import TypeChecker._
- def semI(t : Expr) : Int = {
+ def semI(t : Expr) : BigInt = {
require( typeOf(t) == ( Some(IntType) : Option[Type] ))
t match {
case Plus(lhs , rhs) => semI(lhs) + semI(rhs)
case Minus(lhs , rhs) => semI(lhs) - semI(rhs)
case Ite(cond, thn, els) =>
if (semB(cond)) semI(thn) else semI(els)
- case IntLiteral(v) => v
+ case IntLiteral(v) => v
}
}
@@ -104,10 +104,10 @@ object Semantics {
}
}
- def b2i(b : Boolean) = if (b) 1 else 0
+ def b2i(b : Boolean): BigInt = if (b) 1 else 0
@induct
- def semUntyped( t : Expr) : Int = { t match {
+ 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
@@ -143,7 +143,7 @@ object Desugar {
case class Ite(cond : SimpleE, thn : SimpleE, els : SimpleE) extends SimpleE
case class Eq(lhs : SimpleE, rhs : SimpleE) extends SimpleE
case class LessThan(lhs : SimpleE, rhs : SimpleE) extends SimpleE
- case class Literal(i : Int) extends SimpleE
+ case class Literal(i : BigInt) extends SimpleE
@induct
def desugar(e : Trees.Expr) : SimpleE = { e match {
@@ -160,13 +160,13 @@ object Desugar {
case Trees.BoolLiteral(b) => Literal(b2i(b))
}} ensuring { res =>
((e, res) passes {
- case Trees.Plus(Trees.IntLiteral(i), Trees.Minus(Trees.IntLiteral(j), Trees.IntLiteral(42))) =>
+ case Trees.Plus(Trees.IntLiteral(i), Trees.Minus(Trees.IntLiteral(j), Trees.IntLiteral(BigInt(42)))) =>
Plus(Literal(i), Plus(Literal(j), Neg(Literal(42))))
}) &&
sem(res) == Semantics.semUntyped(e)
}
- def sem(e : SimpleE) : Int = e match {
+ def sem(e: SimpleE): BigInt = e match {
case Plus (lhs, rhs) => sem(lhs) + sem(rhs)
case Ite(cond, thn, els) => if (sem(cond) != 0) sem(thn) else sem(els)
case Neg(arg) => -sem(arg)
diff --git a/src/test/resources/regression/repair/Heap4.scala b/src/test/resources/regression/repair/Heap4.scala
index b6dc755631d9464b3dec57f0c3505b2cf2cea379..01c8b41f941c31d8a8bf2186bb26ac48c42de42b 100644
--- a/src/test/resources/regression/repair/Heap4.scala
+++ b/src/test/resources/regression/repair/Heap4.scala
@@ -10,20 +10,20 @@ import leon.collection._
object HeapSort {
sealed abstract class Heap {
- val rank : Int = this match {
+ val rank : BigInt = this match {
case Leaf() => 0
case Node(_, l, r) =>
1 + max(l.rank, r.rank)
}
- def content : Set[Int] = this match {
- case Leaf() => Set[Int]()
+ def content : Set[BigInt] = this match {
+ case Leaf() => Set[BigInt]()
case Node(v,l,r) => l.content ++ Set(v) ++ r.content
}
}
case class Leaf() extends Heap
- case class Node(value:Int, left: Heap, right: Heap) extends Heap
+ case class Node(value:BigInt, left: Heap, right: Heap) extends Heap
- def max(i1 : Int, i2 : Int) = if (i1 >= i2) i1 else i2
+ def max(i1 : BigInt, i2 : BigInt) = if (i1 >= i2) i1 else i2
def hasHeapProperty(h : Heap) : Boolean = h match {
case Leaf() => true
@@ -46,7 +46,7 @@ object HeapSort {
l.rank >= r.rank
}
- def heapSize(t: Heap): Int = { t match {
+ def heapSize(t: Heap): BigInt = { t match {
case Leaf() => 0
case Node(v, l, r) => heapSize(l) + 1 + heapSize(r)
}} ensuring(_ >= 0)
@@ -71,7 +71,7 @@ object HeapSort {
h1.content ++ h2.content == res.content
}
- private def makeN(value: Int, left: Heap, right: Heap) : Heap = {
+ private def makeN(value: BigInt, left: Heap, right: Heap) : Heap = {
require(
hasLeftistProperty(left) && hasLeftistProperty(right)
)
@@ -82,7 +82,7 @@ object HeapSort {
} ensuring { res =>
hasLeftistProperty(res) }
- def insert(element: Int, heap: Heap) : Heap = {
+ def insert(element: BigInt, heap: Heap) : Heap = {
require(hasLeftistProperty(heap) && hasHeapProperty(heap))
merge(Node(element, Leaf(), Leaf()), heap)
@@ -93,7 +93,7 @@ object HeapSort {
res.content == heap.content ++ Set(element)
}
- def findMax(h: Heap) : Option[Int] = {
+ def findMax(h: Heap) : Option[BigInt] = {
h match {
case Node(m,_,_) => Some(m)
case Leaf() => None()
diff --git a/src/test/resources/regression/repair/List1.scala b/src/test/resources/regression/repair/List1.scala
index 7bafe7ad0ec10a5a5c08c1149251c1dae8e78d63..ff31089cf42af55b2e8a43331fcfd39cd5f2334e 100644
--- a/src/test/resources/regression/repair/List1.scala
+++ b/src/test/resources/regression/repair/List1.scala
@@ -8,7 +8,7 @@ import leon.annotation._
import leon.collection._
sealed abstract class List0[T] {
- def size: Int = (this match {
+ def size: BigInt = (this match {
case Nil0() => 0
case Cons0(h, t) => 1 + t.size
}) ensuring (_ >= 0)
@@ -43,7 +43,7 @@ sealed abstract class List0[T] {
}
}
- def apply(index: Int): T = {
+ def apply(index: BigInt): T = {
require(0 <= index && index < size)
if (index == 0) {
head
@@ -68,7 +68,7 @@ sealed abstract class List0[T] {
}
} ensuring (res => (res.size == size) && (res.content == content))
- def take(i: Int): List0[T] = (this, i) match {
+ def take(i: BigInt): List0[T] = (this, i) match {
case (Nil0(), _) => Nil0()
case (Cons0(h, t), i) =>
if (i == 0) {
@@ -78,7 +78,7 @@ sealed abstract class List0[T] {
}
}
- def drop(i: Int): List0[T] = (this, i) match {
+ def drop(i: BigInt): List0[T] = (this, i) match {
case (Nil0(), _) => Nil0()
case (Cons0(h, t), i) =>
if (i == 0) {
@@ -88,7 +88,7 @@ sealed abstract class List0[T] {
}
}
- def slice(from: Int, to: Int): List0[T] = {
+ def slice(from: BigInt, to: BigInt): List0[T] = {
require(from < to && to < size && from >= 0)
drop(from).take(to-from)
}
@@ -104,7 +104,7 @@ sealed abstract class List0[T] {
}
}
- private def chunk0(s: Int, l: List0[T], acc: List0[T], res: List0[List0[T]], s0: Int): List0[List0[T]] = l match {
+ private def chunk0(s: BigInt, l: List0[T], acc: List0[T], res: List0[List0[T]], s0: BigInt): List0[List0[T]] = l match {
case Nil0() =>
if (acc.size > 0) {
res :+ acc
@@ -119,7 +119,7 @@ sealed abstract class List0[T] {
}
}
- def chunks(s: Int): List0[List0[T]] = {
+ def chunks(s: BigInt): List0[List0[T]] = {
require(s > 0)
chunk0(s, this, Nil0(), Nil0(), s)
@@ -165,7 +165,7 @@ sealed abstract class List0[T] {
Nil0()
}
- def pad(s: Int, e: T): List0[T] = { (this, s) match {
+ def pad(s: BigInt, e: T): List0[T] = { (this, s) match {
case (_, s) if s <= 0 =>
this
case (Nil0(), s) =>
@@ -174,11 +174,11 @@ sealed abstract class List0[T] {
Cons0(h, t.pad(s-1, e)) // FIXME should be s
}} ensuring { res =>
((this,s,e), res) passes {
- case (Cons0(a,Nil0()), 2, x) => Cons0(a, Cons0(x, Cons0(x, Nil0())))
+ case (Cons0(a,Nil0()), BigInt(2), x) => Cons0(a, Cons0(x, Cons0(x, Nil0())))
}
}
- def find(e: T): Option[Int] = this match {
+ def find(e: T): Option[BigInt] = this match {
case Nil0() => None()
case Cons0(h, t) =>
if (h == e) {
@@ -234,7 +234,7 @@ sealed abstract class List0[T] {
Cons0(Nil0(), Nil0())
}
- def count(e: T): Int = this match {
+ def count(e: T): BigInt = this match {
case Cons0(h, t) =>
if (h == e) {
1 + t.count(e)
@@ -250,7 +250,7 @@ sealed abstract class List0[T] {
(take(c), drop(c))
}
- def insertAt(pos: Int, l: List0[T]): List0[T] = {
+ def insertAt(pos: BigInt, l: List0[T]): List0[T] = {
if(pos < 0) {
insertAt(size + pos, l)
} else if(pos == 0) {
@@ -265,7 +265,7 @@ sealed abstract class List0[T] {
}
}
- def replaceAt(pos: Int, l: List0[T]): List0[T] = {
+ def replaceAt(pos: BigInt, l: List0[T]): List0[T] = {
if(pos < 0) {
replaceAt(size + pos, l)
} else if(pos == 0) {
@@ -280,7 +280,7 @@ sealed abstract class List0[T] {
}
}
- def rotate(s: Int): List0[T] = {
+ def rotate(s: BigInt): List0[T] = {
if (s < 0) {
rotate(size+s)
} else {
@@ -308,19 +308,19 @@ object List0Ops {
case Nil0() => Nil0()
}
- def isSorted(ls: List0[Int]): Boolean = ls match {
+ def isSorted(ls: List0[BigInt]): Boolean = ls match {
case Nil0() => true
case Cons0(_, Nil0()) => true
case Cons0(h1, Cons0(h2, _)) if(h1 > h2) => false
case Cons0(_, t) => isSorted(t)
}
- def sorted(ls: List0[Int]): List0[Int] = ls match {
+ def sorted(ls: List0[BigInt]): List0[BigInt] = ls match {
case Cons0(h, t) => insSort(sorted(t), h)
case Nil0() => Nil0()
}
- def insSort(ls: List0[Int], v: Int): List0[Int] = ls match {
+ def insSort(ls: List0[BigInt], v: BigInt): List0[BigInt] = ls match {
case Nil0() => Cons0(v, Nil0())
case Cons0(h, t) =>
if (v <= h) {
@@ -337,7 +337,7 @@ case class Nil0[T]() extends List0[T]
@library
object List0Specs {
- def snocIndex[T](l : List0[T], t : T, i : Int) : Boolean = {
+ def snocIndex[T](l : List0[T], t : T, i : BigInt) : Boolean = {
require(0 <= i && i < l.size + 1)
// proof:
(l match {
@@ -348,7 +348,7 @@ object List0Specs {
((l :+ t).apply(i) == (if (i < l.size) l(i) else t))
}.holds
- def reverseIndex[T](l : List0[T], i : Int) : Boolean = {
+ def reverseIndex[T](l : List0[T], i : BigInt) : Boolean = {
require(0 <= i && i < l.size)
(l match {
case Nil0() => true
@@ -357,7 +357,7 @@ object List0Specs {
(l.reverse.apply(i) == l.apply(l.size - 1 - i))
}.holds
- def appendIndex[T](l1 : List0[T], l2 : List0[T], i : Int) : Boolean = {
+ def appendIndex[T](l1 : List0[T], l2 : List0[T], i : BigInt) : Boolean = {
require(0 <= i && i < l1.size + l2.size)
(l1 match {
case Nil0() => true
diff --git a/src/test/resources/regression/repair/MergeSort2.scala b/src/test/resources/regression/repair/MergeSort2.scala
index ca22569d80c779b3fce3575b66ae0fd701661062..649582ee282910cfd38e48983cea3a389ce68564 100644
--- a/src/test/resources/regression/repair/MergeSort2.scala
+++ b/src/test/resources/regression/repair/MergeSort2.scala
@@ -5,7 +5,7 @@ import leon.collection._
object MergeSort {
- def split(l : List[Int]) : (List[Int],List[Int]) = { l match {
+ def split(l : List[BigInt]) : (List[BigInt],List[BigInt]) = { l match {
case Cons(a, Cons(b, t)) =>
val (rec1, rec2) = split(t)
(Cons(a, rec1), Cons(b, rec2))
@@ -18,12 +18,12 @@ object MergeSort {
l1.content ++ l2.content == l.content
}
- def isSorted(l : List[Int]) : Boolean = l match {
+ def isSorted(l : List[BigInt]) : Boolean = l match {
case Cons(x, t@Cons(y, _)) => x <= y && isSorted(t)
case _ => true
}
- def merge(l1 : List[Int], l2 : List[Int]) : List[Int] = {
+ def merge(l1 : List[BigInt], l2 : List[BigInt]) : List[BigInt] = {
require(isSorted(l1) && isSorted(l2))
(l1, l2) match {
case (Cons(h1, t1), Cons(h2,t2)) =>
@@ -40,7 +40,7 @@ object MergeSort {
res.content == l1.content ++ l2.content
}
- def mergeSort(l : List[Int]) : List[Int] = { l match {
+ def mergeSort(l : List[BigInt]) : List[BigInt] = { l match {
case Nil() => l
case Cons(_, Nil()) => l
case other =>
diff --git a/src/test/resources/regression/repair/Numerical1.scala b/src/test/resources/regression/repair/Numerical1.scala
index 127a136e425aa571cffa7b43a95cea368e1c7f5e..0fdf8580bc25b70db83c272c3da5ffa108c00cbe 100644
--- a/src/test/resources/regression/repair/Numerical1.scala
+++ b/src/test/resources/regression/repair/Numerical1.scala
@@ -5,7 +5,7 @@ import leon.lang._
import leon.annotation._
object Numerical {
- def power(base: Int, p: Int): Int = {
+ def power(base: BigInt, p: BigInt): BigInt = {
require(p >= 0)
if (p == 0) {
1
@@ -16,14 +16,14 @@ object Numerical {
}
} ensuring {
res => ((base, p), res) passes {
- case (_, 0) => 1
- case (b, 1) => b
- case (2, 7) => 128
- case (2, 10) => 1024
+ case (_, BigInt(0)) => 1
+ case (b, BigInt(1)) => b
+ case (BigInt(2), BigInt(7)) => 128
+ case (BigInt(2), BigInt(10)) => 1024
}
}
- def gcd(a: Int, b: Int): Int = {
+ def gcd(a: BigInt, b: BigInt): BigInt = {
require(a > 0 && b > 0);
if (a == b) {
@@ -35,11 +35,11 @@ object Numerical {
}
} ensuring {
res => (a%res == 0) && (b%res == 0) && (((a,b), res) passes {
- case (468, 24) => 12
+ case (BigInt(468), BigInt(24)) => 12
})
}
- def moddiv(a: Int, b: Int): (Int, Int) = {
+ def moddiv(a: BigInt, b: BigInt): (BigInt, BigInt) = {
require(a >= 0 && b > 0);
if (b > a) {
(a, 0)