From ff702c619112af3cd2a89b3cde96ec5ad1f9d8c2 Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 6 Apr 2016 10:26:45 +0200
Subject: [PATCH] Ignore even more, add timeouts to VerificationSuite
---
.../scala/leon/regression/termination/TerminationSuite.scala | 2 +-
.../verification/purescala/PureScalaVerificationSuite.scala | 1 +
2 files changed, 2 insertions(+), 1 deletion(-)
diff --git a/src/test/scala/leon/regression/termination/TerminationSuite.scala b/src/test/scala/leon/regression/termination/TerminationSuite.scala
index ae8e6725a..52984ac7a 100644
--- a/src/test/scala/leon/regression/termination/TerminationSuite.scala
+++ b/src/test/scala/leon/regression/termination/TerminationSuite.scala
@@ -33,7 +33,7 @@ class TerminationSuite extends LeonRegressionSuite {
}
val ignored = List(
- //"termination/valid/NNF.scala",
+ "termination/valid/NNF.scala",
//"verification/purescala/valid/MergeSort.scala",
"verification/purescala/valid/Nested14.scala"
)
diff --git a/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala b/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala
index e54bfeef6..fb9b608cb 100644
--- a/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala
+++ b/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala
@@ -23,6 +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=60")
}
}
--
GitLab