From 4104846bf08947118daac13d6d2aa1e70d3abe2d Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Tue, 1 Sep 2015 17:20:05 +0200
Subject: [PATCH] Tidy up testcases
---
testcases/synthesis/ADTInduction.scala | 4 +-
testcases/synthesis/CegisExamples.scala | 4 +-
testcases/synthesis/ChoosePos.scala | 13 +---
testcases/synthesis/Sec2Time.scala | 6 +-
testcases/synthesis/Simple.scala | 8 --
testcases/synthesis/SimplestCegis.scala | 4 +-
testcases/synthesis/Spt.scala | 74 +++++++++----------
.../AddressesMakeAddressBook.scala | 3 +-
.../AddressesMakeAddressBookWithHelpers.scala | 3 +-
.../AddressesMergeAddressBooks.scala | 9 +--
.../synthesis/{ => future}/Simplifier.scala | 0
.../synthesis/{ => future}/Simplifier1.scala | 0
.../synthesis/{ => future}/Simplifier2.scala | 0
.../synthesis/{ => future}/Simplifier3.scala | 0
.../synthesis/{ => future}/SortedList.scala | 4 +-
.../AddressesMakeAddressBook.scala | 3 +-
.../AddressesMakeAddressBookStrong.scala | 11 ++-
.../AddressesMakeAddressBookSynthWrong.scala | 19 ++---
.../AddressesMakeAddressBookWithHelpers.scala | 6 +-
.../AddressesMergeAddressBooks.scala | 3 +-
.../AddressesMergeAddressBooksStep1.scala | 4 +-
.../AddressesMergeAddressBooksStep2.scala | 12 ++-
.../synthesis/oopsla2013/List/Batch.scala | 4 +-
.../synthesis/oopsla2013/List/Complete.scala | 4 +-
.../synthesis/oopsla2013/List/Delete.scala | 4 +-
.../synthesis/oopsla2013/List/Diff.scala | 4 +-
.../synthesis/oopsla2013/List/Insert.scala | 4 +-
.../synthesis/oopsla2013/List/Split.scala | 4 +-
.../synthesis/oopsla2013/List/Union.scala | 4 +-
29 files changed, 97 insertions(+), 121 deletions(-)
delete mode 100644 testcases/synthesis/Simple.scala
rename testcases/synthesis/{ => future}/Simplifier.scala (100%)
rename testcases/synthesis/{ => future}/Simplifier1.scala (100%)
rename testcases/synthesis/{ => future}/Simplifier2.scala (100%)
rename testcases/synthesis/{ => future}/Simplifier3.scala (100%)
rename testcases/synthesis/{ => future}/SortedList.scala (98%)
diff --git a/testcases/synthesis/ADTInduction.scala b/testcases/synthesis/ADTInduction.scala
index 0824a9928..5341f1cba 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 a43a3e948..431cfa8ca 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 cdacbd72b..f0db1d91e 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 02ab40320..893f7e67e 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 0f1d8b76b..000000000
--- 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 804279046..678e3f4f0 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 98cb72e9e..82a286e81 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 e7067c756..ec721a71f 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 3dfd21465..107f460cb 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 8436ef25f..6d1a226ab 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 b97642ef3..b71f4f67e 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 cdcb8b1c9..3d97a6e04 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 5d4a788b8..9167ab278 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 548bb9849..8b2d19384 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 194d194c3..88798b986 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 a281e7423..51836accd 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 e3b6c8c7e..de80592e9 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 6729bbb2d..9398eb078 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 c7fcf02d0..a03ef2033 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 75377777e..9d52f3181 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 a61e312c9..d6c5072aa 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 dcf4f372c..45b67f35a 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 3f6fcd23a..652190117 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 b4e4c3fe2..aca7da75f 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 17dda5cfd..f33990420 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 {
--
GitLab