diff --git a/testcases/synthesis/ADTInduction.scala b/testcases/synthesis/ADTInduction.scala
index 0824a9928d71a5fc7d03be9aff39ce723b01193e..5341f1cbab05f3f4e22ba398ca3e8736e03694de 100644
--- a/testcases/synthesis/ADTInduction.scala
+++ b/testcases/synthesis/ADTInduction.scala
@@ -9,8 +9,8 @@ object SortedList {
// proved with unrolling=0
def size(l: List) : Int = (l match {
- case Nil() => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil() => 0
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
//def sizeSynth(l: List): Int = choose{ (i: Int) => i >= 0 && sizeSynth(Cons(0, l)) == i + 1}
diff --git a/testcases/synthesis/CegisExamples.scala b/testcases/synthesis/CegisExamples.scala
index a43a3e948cb8dd4b775094fb349fa69c6968270c..431cfa8ca1dcd1ed9ed1c7af1bcb950e5000d05b 100644
--- a/testcases/synthesis/CegisExamples.scala
+++ b/testcases/synthesis/CegisExamples.scala
@@ -8,8 +8,8 @@ object CegisTests {
// proved with unrolling=0
def size(l: List) : Int = (l match {
- case Nil() => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil() => 0
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[Int] = l match {
diff --git a/testcases/synthesis/ChoosePos.scala b/testcases/synthesis/ChoosePos.scala
index cdacbd72bcabade3420e1ba9d9cfcd3b80956c14..f0db1d91e6f0c826a3ab263d4134a0625692e056 100644
--- a/testcases/synthesis/ChoosePos.scala
+++ b/testcases/synthesis/ChoosePos.scala
@@ -3,17 +3,6 @@ import leon.lang.synthesis._
object ChoosePos {
-
-def c1(x: Int): Int =
- choose {
- (y: Int) => y > x
- }
-
-def c2(x: Int): Int =
- choose (
- (y: Int) => y > x
- )
- def c3(x: Int): Int = choose { (y: Int) => y > x }
- def c4(x: Int): Int = choose { (y: Int) => y > x }; def c5(x: Int): Int = choose { (y: Int) => y > x }
+ def c1(x: BigInt): BigInt = choose { (y: BigInt) => y > x }
}
diff --git a/testcases/synthesis/Sec2Time.scala b/testcases/synthesis/Sec2Time.scala
index 02ab40320580899844504233ffb8bfde2b35b6f9..893f7e67ef8c0d981e478acf0975ad23dc3fc940 100644
--- a/testcases/synthesis/Sec2Time.scala
+++ b/testcases/synthesis/Sec2Time.scala
@@ -3,6 +3,10 @@ import leon.lang.synthesis._
object Sec2Time {
- def s2t(total: Int) : (Int, Int, Int) = choose((h: Int, m: Int, s: Int) => 3600*h + 60*m + s == total && h >= 0 && m >= 0 && m < 60 && s >= 0 && s < 60)
+ def s2t(total: Int) : (Int, Int, Int) =
+ choose((h: Int, m: Int, s: Int) =>
+ 3600*h + 60*m + s == total &&
+ h >= 0 && m >= 0 && m < 60 && s >= 0 && s < 60
+ )
}
diff --git a/testcases/synthesis/Simple.scala b/testcases/synthesis/Simple.scala
deleted file mode 100644
index 0f1d8b76bfc0726d7d37086cd05c9587aacf3233..0000000000000000000000000000000000000000
--- a/testcases/synthesis/Simple.scala
+++ /dev/null
@@ -1,8 +0,0 @@
-import leon.lang._
-import leon.lang.synthesis._
-
-object SimpleSynthesis {
-
- def c1(x: Int): Int = choose { (y: Int) => y > x }
-
-}
diff --git a/testcases/synthesis/SimplestCegis.scala b/testcases/synthesis/SimplestCegis.scala
index 804279046f0063cf8c2e0327799f23a3397f041a..678e3f4f04afbf576db954a4f8fb2e77b44937c8 100644
--- a/testcases/synthesis/SimplestCegis.scala
+++ b/testcases/synthesis/SimplestCegis.scala
@@ -9,8 +9,8 @@ object Injection {
// proved with unrolling=0
def size(l: List) : Int = (l match {
- case Nil() => 0
- case Cons(t) => 1 + size(t)
+ case Nil() => 0
+ case Cons(t) => 1 + size(t)
}) ensuring(res => res >= 0)
def simple(in: List) = choose{out: List => size(out) == size(in) }
diff --git a/testcases/synthesis/Spt.scala b/testcases/synthesis/Spt.scala
index 98cb72e9eefe77316844ca067beead97d9979465..82a286e81f864821bb6998ccff351813188c3196 100644
--- a/testcases/synthesis/Spt.scala
+++ b/testcases/synthesis/Spt.scala
@@ -4,27 +4,21 @@ import leon.lang.synthesis._
// Examples taken from http://lara.epfl.ch/~psuter/spt/
object SynthesisProceduresToolkit {
- def e1(a: Nat, b: Nat, c: Nat): Nat = if ((b == c)) {
- if ((a == c)) {
- (choose { (x: Nat) =>
- (x != a)
- })
- } else {
- (choose { (x: Nat) =>
- ((x != a) && (x != b))
- })
+ def e1(a: Nat, b: Nat, c: Nat): Nat = {
+ if (b == c) {
+ if (a == c) {
+ choose { (x: Nat) => x != a }
+ } else {
+ choose { (x: Nat) => x != a && x != b }
+ }
+ } else {
+ if (a == b) {
+ choose { (x: Nat) => x != a && x != c }
+ } else {
+ choose { (x: Nat) => x != a && x != b && x != c }
+ }
+ }
}
-} else {
- if ((a == b)) {
- (choose { (x: Nat) =>
- ((x != a) && (x != c))
- })
- } else {
- (choose { (x: Nat) =>
- ((x != a) && (x != b) && (x != c))
- })
- }
-}
def e2(): (Nat, Nat, Nat) = (Z(), Succ(Z()), Succ(Succ(Succ(Z()))))
@@ -32,26 +26,30 @@ object SynthesisProceduresToolkit {
def e4(a1 : Nat, a2 : Nat, a3 : Nat, a4 : Nat): (Nat, Nat, NatList) = (Succ(a2), a1, Nil())
- def e5(a1 : NatList, a2 : Nat, a3 : NatList): (Nat, NatList, Nat, NatList) = (choose { (x1: Nat, x2: NatList, x3: Nat, x4: NatList) =>
- ((Cons(Succ(x1), x2) == a1) && (Succ(x1) != a2) && (a3 == Cons(x3, Cons(x3, x4))))
-})
-
- def e6(a: Nat, b: Nat): (Nat, NatList) = if ((a == Succ(b))) {
- (Z(), Nil())
-} else {
- leon.lang.error[(Nat, NatList)]("Precondition failed")
-}
+ def e5(a1 : NatList, a2 : Nat, a3 : NatList): (Nat, NatList, Nat, NatList) =
+ choose { (x1: Nat, x2: NatList, x3: Nat, x4: NatList) =>
+ Cons(Succ(x1), x2) == a1 && Succ(x1) != a2 && a3 == Cons(x3, Cons(x3, x4))
+ }
+
+ def e6(a: Nat, b: Nat): (Nat, NatList) = {
+ if (a == Succ(b)) {
+ (Z(), Nil())
+ } else {
+ leon.lang.error[(Nat, NatList)]("Precondition failed")
+ }
+ }
- def e7(a1 : NatList, a2 : Nat, a3 : NatList): (Nat, NatList, Nat, NatList) = (choose { (x1: Nat, x2: NatList, x3: Nat, x4: NatList) =>
- ((Cons(Succ(x1), x2) == a1) && (Succ(x1) != a2) && (a3 == Cons(x3, Cons(x3, x4))))
-})
+ def e7(a1 : NatList, a2 : Nat, a3 : NatList): (Nat, NatList, Nat, NatList) =
+ choose { (x1: Nat, x2: NatList, x3: Nat, x4: NatList) =>
+ Cons(Succ(x1), x2) == a1 && Succ(x1) != a2 && a3 == Cons(x3, Cons(x3, x4))
+ }
- def e8(a : Nat) = (a match {
- case Succ(n150) =>
- n150
- case _ =>
- leon.lang.error[(Nat)]("Precondition failed")
-})
+ def e8(a : Nat) = a match {
+ case Succ(n150) =>
+ n150
+ case _ =>
+ leon.lang.error[(Nat)]("Precondition failed")
+ }
abstract class Nat
case class Z() extends Nat
diff --git a/testcases/synthesis/condabd/benchmarks/AddressBook/AddressesMakeAddressBook.scala b/testcases/synthesis/condabd/benchmarks/AddressBook/AddressesMakeAddressBook.scala
index e7067c756d047cb101b25dde6a3ae51313ffb8cf..ec721a71fae93a50f863f0760e330453f0af7ecb 100644
--- a/testcases/synthesis/condabd/benchmarks/AddressBook/AddressesMakeAddressBook.scala
+++ b/testcases/synthesis/condabd/benchmarks/AddressBook/AddressesMakeAddressBook.scala
@@ -94,8 +94,7 @@ object Addresses {
// } else true )
// }
- def makeAddressBook(l: List): AddressBook =
- choose {
+ def makeAddressBook(l: List): AddressBook = choose {
(res: AddressBook) =>
size(res) == size(l) && addressBookInvariant(res)
}
diff --git a/testcases/synthesis/condabd/benchmarks/AddressBook/AddressesMakeAddressBookWithHelpers.scala b/testcases/synthesis/condabd/benchmarks/AddressBook/AddressesMakeAddressBookWithHelpers.scala
index 3dfd21465f2743d99a0c2365b49c43ad5827aa32..107f460cb5690181c2cd5de7a6b73c5772549346 100644
--- a/testcases/synthesis/condabd/benchmarks/AddressBook/AddressesMakeAddressBookWithHelpers.scala
+++ b/testcases/synthesis/condabd/benchmarks/AddressBook/AddressesMakeAddressBookWithHelpers.scala
@@ -95,8 +95,7 @@ object Addresses {
// } else true )
// }
- def makeAddressBook(l: List): AddressBook =
- choose {
+ def makeAddressBook(l: List): AddressBook = choose {
(res: AddressBook) =>
size(res) == size(l) &&
allPrivate(res.pers) && allBusiness(res.business) &&
diff --git a/testcases/synthesis/condabd/benchmarks/AddressBook/AddressesMergeAddressBooks.scala b/testcases/synthesis/condabd/benchmarks/AddressBook/AddressesMergeAddressBooks.scala
index 8436ef25f5ba3569b6b181847ed142f818dd63c8..6d1a226ab66f480deb50b424305c6cdfec1ac35b 100644
--- a/testcases/synthesis/condabd/benchmarks/AddressBook/AddressesMergeAddressBooks.scala
+++ b/testcases/synthesis/condabd/benchmarks/AddressBook/AddressesMergeAddressBooks.scala
@@ -43,9 +43,9 @@ object Addresses {
def size(ab: AddressBook): Int = size(ab.business) + size(ab.pers)
- def addToPers(ab: AddressBook, adr: Address) = AddressBook(ab.business, Cons(adr, ab.pers))
+ def addToPers(ab: AddressBook, adr: Address) = AddressBook(ab.business, Cons(adr, ab.pers))
- def addToBusiness(ab: AddressBook, adr: Address) = AddressBook(Cons(adr, ab.business), ab.pers)
+ def addToBusiness(ab: AddressBook, adr: Address) = AddressBook(Cons(adr, ab.business), ab.pers)
def isEmpty(ab: AddressBook) = size(ab) == 0
@@ -72,9 +72,8 @@ object Addresses {
def mergeAddressBooks(ab1: AddressBook, ab2: AddressBook) = {
require(addressBookInvariant(ab1) && addressBookInvariant(ab2))
- choose {
- (res: AddressBook) =>
- (size(res) == size(ab1) + size(ab2)) && addressBookInvariant(res)
+ choose { (res: AddressBook) =>
+ (size(res) == size(ab1) + size(ab2)) && addressBookInvariant(res)
}
}
diff --git a/testcases/synthesis/Simplifier.scala b/testcases/synthesis/future/Simplifier.scala
similarity index 100%
rename from testcases/synthesis/Simplifier.scala
rename to testcases/synthesis/future/Simplifier.scala
diff --git a/testcases/synthesis/Simplifier1.scala b/testcases/synthesis/future/Simplifier1.scala
similarity index 100%
rename from testcases/synthesis/Simplifier1.scala
rename to testcases/synthesis/future/Simplifier1.scala
diff --git a/testcases/synthesis/Simplifier2.scala b/testcases/synthesis/future/Simplifier2.scala
similarity index 100%
rename from testcases/synthesis/Simplifier2.scala
rename to testcases/synthesis/future/Simplifier2.scala
diff --git a/testcases/synthesis/Simplifier3.scala b/testcases/synthesis/future/Simplifier3.scala
similarity index 100%
rename from testcases/synthesis/Simplifier3.scala
rename to testcases/synthesis/future/Simplifier3.scala
diff --git a/testcases/synthesis/SortedList.scala b/testcases/synthesis/future/SortedList.scala
similarity index 98%
rename from testcases/synthesis/SortedList.scala
rename to testcases/synthesis/future/SortedList.scala
index b97642ef36176fbb0a25ca1698b9d96bc05d329a..b71f4f67edc46804c49ba7e41c09ea054e741cec 100644
--- a/testcases/synthesis/SortedList.scala
+++ b/testcases/synthesis/future/SortedList.scala
@@ -9,8 +9,8 @@ object SortedList {
// proved with unrolling=0
def size(l: List) : Int = (l match {
- case Nil() => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil() => 0
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
//def sizeSynth(l: List): Int = choose{ (i: Int) => i >= 0 && sizeSynth(Cons(0, l)) == i + 1}
diff --git a/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBook.scala b/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBook.scala
index cdcb8b1c962e078922e9797999ecd5b7c39fb17c..3d97a6e04f1b71dd075ac63be64f9284e2b2069c 100644
--- a/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBook.scala
+++ b/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBook.scala
@@ -94,8 +94,7 @@ object Addresses {
// } else true )
// }
- def makeAddressBook(l: List): AddressBook =
- choose {
+ def makeAddressBook(l: List): AddressBook = choose {
(res: AddressBook) =>
sizeA(res) == size(l) && addressBookInvariant(res)
}
diff --git a/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookStrong.scala b/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookStrong.scala
index 5d4a788b8fd65aac5faee31e85cc10b4f53d07da..9167ab27829b721c7788c3173b8aef5d115a4bf2 100644
--- a/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookStrong.scala
+++ b/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookStrong.scala
@@ -118,12 +118,11 @@ object Addresses {
}
*/
- def makeAddressBook(l: List): AddressBook =
- choose {
+ def makeAddressBook(l: List): AddressBook = choose {
(res: AddressBook) =>
- sizeA(res) == size(l) &&
- addressBookInvariant(res) &&
- contentA(res) == content(l)
+ sizeA(res) == size(l) &&
+ addressBookInvariant(res) &&
+ contentA(res) == content(l)
}
-
+
}
diff --git a/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookSynthWrong.scala b/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookSynthWrong.scala
index 548bb98494293574668b940362492d4813e901fc..8b2d19384b523c460b74866e5bc93bfdc9c91de3 100644
--- a/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookSynthWrong.scala
+++ b/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookSynthWrong.scala
@@ -97,17 +97,18 @@ object Addresses {
def makeAddressBook(l: List): AddressBook = {
l match {
case Nil => AddressBook(Nil,l)
- case Cons(h,t) => {
- if (allPrivate(t))
- AddressBook(Nil, Cons(Address(h.info, allPrivate(t)), t))
- else
- AddressBook(Cons(Address(h.info, isEmpty(makeAddressBook(t))),
- makeAddressBook(t).business),
- makeAddressBook(t).pers)
- }
+ case Cons(h,t) =>
+ if (allPrivate(t))
+ AddressBook(Nil, Cons(Address(h.info, allPrivate(t)), t))
+ else
+ AddressBook(
+ Cons( Address(h.info, isEmpty(makeAddressBook(t))), makeAddressBook(t).business),
+ makeAddressBook(t).pers
+ )
}
} ensuring ((res: AddressBook) =>
- sizeA(res) == size(l) && addressBookInvariant(res))
+ sizeA(res) == size(l) && addressBookInvariant(res)
+ )
}
diff --git a/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookWithHelpers.scala b/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookWithHelpers.scala
index 194d194c35276356d2122770cbc1889c9647b9b2..88798b9869dbbc01075816fbaf0469d1cd96f9d7 100644
--- a/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookWithHelpers.scala
+++ b/testcases/synthesis/oopsla2013/AddressBook/AddressesMakeAddressBookWithHelpers.scala
@@ -95,11 +95,11 @@ object Addresses {
// } else true )
// }
- def makeAddressBook(l: List): AddressBook =
- choose {
+ def makeAddressBook(l: List): AddressBook = choose {
(res: AddressBook) =>
size(res) == size(l) &&
- allPrivate(res.pers) && allBusiness(res.business) &&
+ allPrivate(res.pers) &&
+ allBusiness(res.business) &&
contentA(res) == content(l)
}
diff --git a/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooks.scala b/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooks.scala
index a281e7423cef6266b00e8a0126b2ea66767dc46e..51836accdf8634c32cf11756d179a76a03a108da 100644
--- a/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooks.scala
+++ b/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooks.scala
@@ -69,8 +69,7 @@ object Addresses {
def mergeAddressBooks(ab1: AddressBook, ab2: AddressBook) = {
require(addressBookInvariant(ab1) && addressBookInvariant(ab2))
- choose {
- (res: AddressBook) =>
+ choose { (res: AddressBook) =>
(sizeA(res) == sizeA(ab1) + sizeA(ab2)) && addressBookInvariant(res)
}
}
diff --git a/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooksStep1.scala b/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooksStep1.scala
index e3b6c8c7ef8130f37ba74800007e1c9a8f2bc857..de80592e981023621e65bfd3e56c279ec28b9cf8 100644
--- a/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooksStep1.scala
+++ b/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooksStep1.scala
@@ -43,9 +43,9 @@ object Addresses {
def size(ab: AddressBook): Int = size(ab.business) + size(ab.pers)
- def addToPers(ab: AddressBook, adr: Address) = AddressBook(ab.business, Cons(adr, ab.pers))
+ def addToPers(ab: AddressBook, adr: Address) = AddressBook(ab.business, Cons(adr, ab.pers))
- def addToBusiness(ab: AddressBook, adr: Address) = AddressBook(Cons(adr, ab.business), ab.pers)
+ def addToBusiness(ab: AddressBook, adr: Address) = AddressBook(Cons(adr, ab.business), ab.pers)
def isEmpty(ab: AddressBook) = size(ab) == 0
diff --git a/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooksStep2.scala b/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooksStep2.scala
index 6729bbb2da63e3233118a9c49f089a0ad45e95ce..9398eb078c968a0a0c3fff26fe819551eb87890a 100644
--- a/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooksStep2.scala
+++ b/testcases/synthesis/oopsla2013/AddressBook/AddressesMergeAddressBooksStep2.scala
@@ -43,9 +43,9 @@ object Addresses {
def size(ab: AddressBook): Int = size(ab.business) + size(ab.pers)
- def addToPers(ab: AddressBook, adr: Address) = AddressBook(ab.business, Cons(adr, ab.pers))
-
- def addToBusiness(ab: AddressBook, adr: Address) = AddressBook(Cons(adr, ab.business), ab.pers)
+ def addToPers(ab: AddressBook, adr: Address) = AddressBook(ab.business, Cons(adr, ab.pers))
+
+ def addToBusiness(ab: AddressBook, adr: Address) = AddressBook(Cons(adr, ab.business), ab.pers)
def isEmpty(ab: AddressBook) = size(ab) == 0
@@ -55,11 +55,10 @@ object Addresses {
def makeAddressBook(l: List): AddressBook = (l match {
case Nil => AddressBook(Nil, Nil)
- case Cons(a, l1) => {
+ case Cons(a, l1) =>
val res = makeAddressBook(l1)
if (a.priv) AddressBook(res.business, Cons(a, res.pers))
else AddressBook(Cons(a, res.business), res.pers)
- }
}) ensuring {
(res: AddressBook) =>
size(res) == size(l) && addressBookInvariant(res)
@@ -74,8 +73,7 @@ object Addresses {
def mergeAddressBooks(ab1: AddressBook, ab2: AddressBook) = {
require(addressBookInvariant(ab1) && addressBookInvariant(ab2))
- choose {
- (res: AddressBook) =>
+ choose { (res: AddressBook) =>
(size(res) == size(ab1) + size(ab2)) && addressBookInvariant(res)
}
}
diff --git a/testcases/synthesis/oopsla2013/List/Batch.scala b/testcases/synthesis/oopsla2013/List/Batch.scala
index c7fcf02d0e0cca67121f132f02426b83ea0d5161..a03ef20334ea840e8f454b22d9a9240d1b24bc36 100644
--- a/testcases/synthesis/oopsla2013/List/Batch.scala
+++ b/testcases/synthesis/oopsla2013/List/Batch.scala
@@ -8,8 +8,8 @@ object List {
case object Nil extends List
def size(l: List) : Int = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[Int] = l match {
diff --git a/testcases/synthesis/oopsla2013/List/Complete.scala b/testcases/synthesis/oopsla2013/List/Complete.scala
index 75377777ecd840af67baff0e6adcd0e2efe2d928..9d52f3181641bbe7ba194c60b29b55a0b1a3e894 100644
--- a/testcases/synthesis/oopsla2013/List/Complete.scala
+++ b/testcases/synthesis/oopsla2013/List/Complete.scala
@@ -8,8 +8,8 @@ object Complete {
case object Nil extends List
def size(l: List) : Int = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[Int] = l match {
diff --git a/testcases/synthesis/oopsla2013/List/Delete.scala b/testcases/synthesis/oopsla2013/List/Delete.scala
index a61e312c9d60adc07c99685408c1f10bb8c81d14..d6c5072aa3280481f212e15cf29adbb199c23c4c 100644
--- a/testcases/synthesis/oopsla2013/List/Delete.scala
+++ b/testcases/synthesis/oopsla2013/List/Delete.scala
@@ -8,8 +8,8 @@ object Delete {
case object Nil extends List
def size(l: List) : Int = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[Int] = l match {
diff --git a/testcases/synthesis/oopsla2013/List/Diff.scala b/testcases/synthesis/oopsla2013/List/Diff.scala
index dcf4f372cd805ed5f7d0f3e83fb9bbc51f77b2dc..45b67f35a8f80678de65f5e79c00afce15f5b230 100644
--- a/testcases/synthesis/oopsla2013/List/Diff.scala
+++ b/testcases/synthesis/oopsla2013/List/Diff.scala
@@ -8,8 +8,8 @@ object Diff {
case object Nil extends List
def size(l: List) : Int = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[Int] = l match {
diff --git a/testcases/synthesis/oopsla2013/List/Insert.scala b/testcases/synthesis/oopsla2013/List/Insert.scala
index 3f6fcd23a5ce47cdc065506c679427b273775337..652190117a85dbf63c02136b0191ba0de969c3c8 100644
--- a/testcases/synthesis/oopsla2013/List/Insert.scala
+++ b/testcases/synthesis/oopsla2013/List/Insert.scala
@@ -8,8 +8,8 @@ object Insert {
case object Nil extends List
def size(l: List) : Int = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[Int] = l match {
diff --git a/testcases/synthesis/oopsla2013/List/Split.scala b/testcases/synthesis/oopsla2013/List/Split.scala
index b4e4c3fe2f5a9cd7839652433838ccb44e96ada7..aca7da75fddb48752ee89864aa918ed70bf444e3 100644
--- a/testcases/synthesis/oopsla2013/List/Split.scala
+++ b/testcases/synthesis/oopsla2013/List/Split.scala
@@ -10,8 +10,8 @@ object Complete {
case object Nil extends List
def size(l: List) : Int = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[Int] = l match {
diff --git a/testcases/synthesis/oopsla2013/List/Union.scala b/testcases/synthesis/oopsla2013/List/Union.scala
index 17dda5cfd9f016d8cfefcd119223b0d742bc5b6f..f33990420bd38a6246d3cf772f09c9cfe72d936a 100644
--- a/testcases/synthesis/oopsla2013/List/Union.scala
+++ b/testcases/synthesis/oopsla2013/List/Union.scala
@@ -8,8 +8,8 @@ object Union {
case object Nil extends List
def size(l: List) : Int = (l match {
- case Nil => 0
- case Cons(_, t) => 1 + size(t)
+ case Nil => 0
+ case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
def content(l: List): Set[Int] = l match {