From f4843e877762174b6be8f3549e6b8215b0ad11a1 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Fri, 22 Apr 2016 15:35:38 +0200
Subject: [PATCH] Increase test timeouts
---
library/collection/List.scala | 4 ++--
.../scala/leon/regression/termination/TerminationSuite.scala | 2 +-
.../leon/regression/verification/XLangVerificationSuite.scala | 2 +-
.../verification/purescala/PureScalaVerificationSuite.scala | 2 +-
4 files changed, 5 insertions(+), 5 deletions(-)
diff --git a/library/collection/List.scala b/library/collection/List.scala
index 1df1115eb..5803bbf99 100644
--- a/library/collection/List.scala
+++ b/library/collection/List.scala
@@ -569,7 +569,7 @@ object List {
@library
def fill[T](n: BigInt)(x: T) : List[T] = {
- if (n <= 0) Nil[T]
+ if (n <= 0) Nil[T]()
else Cons[T](x, fill[T](n-1)(x))
} ensuring(res => (res.content == (if (n <= BigInt(0)) Set.empty[T] else Set(x))) &&
res.size == (if (n <= BigInt(0)) BigInt(0) else n))
@@ -899,7 +899,7 @@ object ListSpecs {
// lemma
((l1 ++ l2).insertAt(i, y) == (
if (i < l1.size) l1.insertAt(i, y) ++ l2
- else l1 ++ l2.insertAt((i - l1.size), y)))
+ else l1 ++ l2.insertAt(i - l1.size, y)))
}.holds
}
diff --git a/src/test/scala/leon/regression/termination/TerminationSuite.scala b/src/test/scala/leon/regression/termination/TerminationSuite.scala
index 94a31ac66..16759a041 100644
--- a/src/test/scala/leon/regression/termination/TerminationSuite.scala
+++ b/src/test/scala/leon/regression/termination/TerminationSuite.scala
@@ -68,7 +68,7 @@ class TerminationSuite extends LeonRegressionSuite {
private def forEachFileIn(files: Iterable[File], forError: Boolean = false)(block : Output=>Unit) {
for(f <- files) {
- mkTest(f, Seq("--solvers=smt-z3", "--timeout=120"), forError)(block)
+ mkTest(f, Seq("--solvers=smt-z3", "--timeout=150"), forError)(block)
}
}
diff --git a/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala b/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala
index a49cf4d3f..104389eb7 100644
--- a/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala
+++ b/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala
@@ -19,7 +19,7 @@ class XLangVerificationSuite extends VerificationSuite {
if (isZ3Available)
List(List("--solvers=smt-z3", "--feelinglucky"))
else Nil
- )).map ("--timeout=120" :: _)
+ )).map ("--timeout=150" :: _)
}
val testDir: String = "regression/verification/xlang/"
diff --git a/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala b/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala
index 95777486d..263f31f0d 100644
--- a/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala
+++ b/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala
@@ -23,7 +23,7 @@ abstract class PureScalaVerificationSuite extends VerificationSuite {
List("--solvers=fairz3,enum", "--codegen", /*"--evalground",*/ "--feelinglucky")) ++
isZ3Available.option(List("--solvers=smt-z3", "--feelinglucky")) ++
isCVC4Available.option(List("--solvers=smt-cvc4", "--feelinglucky")))
- .map( _ :+ "--timeout=120")
+ .map( _ :+ "--timeout=150")
}
}
--
GitLab