diff --git a/library/collection/List.scala b/library/collection/List.scala index 1df1115eb34fb89bcd63b8f78e0060c668a9948c..5803bbf993def9d80019a7f7839860cf249db729 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 94a31ac66f7cbcbf70e4acf9607b6f3e489699e3..16759a041978f903babcf430c90a5cc14c4a3db7 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 a49cf4d3fbdf0e8bb1ad1a00d1660ce8f8d7c52f..104389eb7e9a1b8d7878d09d678a31448ed5b283 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 95777486dbc1a6032028cfd57cf306ef029fa58c..263f31f0d709c427a18ad17037737b1d47c64764 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") } }