From 92a3c857b08a222b0826f53cc9dd9860dbf0378e Mon Sep 17 00:00:00 2001
From: Marco Antognini <antognini.marco@gmail.com>
Date: Sun, 3 Jan 2016 18:49:45 +0100
Subject: [PATCH] Update GenCSuite, partially revert "Fix verification
sub-suite for GenC"
---
src/test/scala/leon/genc/GenCSuite.scala | 3 +--
.../scala/leon/regression/verification/VerificationSuite.scala | 2 +-
.../leon/regression/verification/XLangVerificationSuite.scala | 3 ++-
3 files changed, 4 insertions(+), 4 deletions(-)
diff --git a/src/test/scala/leon/genc/GenCSuite.scala b/src/test/scala/leon/genc/GenCSuite.scala
index 4292f9583..df6d30e5c 100644
--- a/src/test/scala/leon/genc/GenCSuite.scala
+++ b/src/test/scala/leon/genc/GenCSuite.scala
@@ -189,8 +189,7 @@ class GenCSuite extends LeonRegressionSuite {
override def suiteName = "Verification Suite For GenC"
// Add a timeout for the verification
- override def optionVariants =
- super.optionVariants map { opts => "--timeout=5" :: opts }
+ override val optionVariants = List(List("--solvers=smt-z3,ground"))
}
// Run verification suite as a nested suite
diff --git a/src/test/scala/leon/regression/verification/VerificationSuite.scala b/src/test/scala/leon/regression/verification/VerificationSuite.scala
index d7eafb38c..f2ae97880 100644
--- a/src/test/scala/leon/regression/verification/VerificationSuite.scala
+++ b/src/test/scala/leon/regression/verification/VerificationSuite.scala
@@ -19,7 +19,7 @@ import org.scalatest.{Reporter => _, _}
// This is because we compile all tests from each folder together.
trait VerificationSuite extends LeonRegressionSuite {
- def optionVariants: List[List[String]]
+ val optionVariants: List[List[String]]
val testDir: String
val ignored: Seq[String] = Seq()
diff --git a/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala b/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala
index 0b6a0c37d..6fe7b0740 100644
--- a/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala
+++ b/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala
@@ -9,7 +9,7 @@ import leon.solvers.SolverFactory
// This is because we compile all tests from each folder together.
class XLangVerificationSuite extends VerificationSuite {
- def optionVariants: List[List[String]] = {
+ val optionVariants: List[List[String]] = {
val isZ3Available = SolverFactory.hasZ3
List(
@@ -25,3 +25,4 @@ class XLangVerificationSuite extends VerificationSuite {
val testDir: String = "regression/verification/xlang/"
override val desugarXLang = true
}
+
--
GitLab