diff --git a/src/test/scala/leon/regression/termination/TerminationSuite.scala b/src/test/scala/leon/regression/termination/TerminationSuite.scala index 5be322e1dc19f33edc8c01ffde51f3ee9612bc5a..321160563a2b0348bb7a52bd740c36d1071ea1a0 100644 --- a/src/test/scala/leon/regression/termination/TerminationSuite.scala +++ b/src/test/scala/leon/regression/termination/TerminationSuite.scala @@ -34,6 +34,7 @@ class TerminationSuite extends LeonRegressionSuite { val ignored = List( "verification/purescala/valid/MergeSort.scala", + "verification/purescala/valid/Nested14.scala", "verification/purescala/valid/InductiveQuantification.scala" ) diff --git a/src/test/scala/leon/regression/verification/PureScalaVerificationSuite.scala b/src/test/scala/leon/regression/verification/PureScalaVerificationSuite.scala index 541056449db2188e84a79f2f86ae6fd553ef7b45..d72e74f2633e3713839622e95582d1f06f399383 100644 --- a/src/test/scala/leon/regression/verification/PureScalaVerificationSuite.scala +++ b/src/test/scala/leon/regression/verification/PureScalaVerificationSuite.scala @@ -15,6 +15,12 @@ class PureScalaVerificationSuite extends VerificationSuite { val testDir = "regression/verification/purescala/" val pipeFront = xlang.NoXLangFeaturesChecking val pipeBack = AnalysisPhase + + override val ignored = Seq( + "verification/purescala/valid/Nested15.scala", + "verification/purescala/invalid/Nested15.scala" + ) + val optionVariants: List[List[String]] = { val isZ3Available = try { Z3Interpreter.buildDefault.free() diff --git a/src/test/scala/leon/regression/verification/VerificationSuite.scala b/src/test/scala/leon/regression/verification/VerificationSuite.scala index 4bf89cee8f78b76a686cfca004c9b8d8f83ae6c8..63bf613d18083e1e9296ac5f00e025eda863716b 100644 --- a/src/test/scala/leon/regression/verification/VerificationSuite.scala +++ b/src/test/scala/leon/regression/verification/VerificationSuite.scala @@ -19,6 +19,8 @@ trait VerificationSuite extends LeonRegressionSuite { val optionVariants: List[List[String]] val testDir: String + val ignored: Seq[String] = Seq() + private var counter: Int = 0 private def nextInt(): Int = { counter += 1 @@ -42,11 +44,19 @@ trait VerificationSuite extends LeonRegressionSuite { val (ctx2, ast) = extraction.run(ctx, files) val programs = { val (user, lib) = ast.units partition { _.isMainUnit } - user map { u => (u.id, Program(u :: lib)) } + user map ( u => Program(u :: lib) ) } - for ((id, p) <- programs; options <- optionVariants) { + for ( p <- programs; options <- optionVariants) { + + val displayName = s"$cat/${p.units.head.id.name}.scala" + val index = nextInt() - test(f"$index%3d: ${id.name} ${options.mkString(" ")}") { + val ts = if (ignored exists (_.endsWith(displayName))) + ignore _ + else + test _ + + ts(f"$index%3d: $displayName ${options.mkString(" ")}", Seq()) { val ctx = createLeonContext(options: _*) if (forError) { intercept[LeonFatalError] { diff --git a/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala b/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala index 83730cc760abb29776027b2ef152b9afccbd861a..26513352be7221aa54864e15112c8a7936c78090 100644 --- a/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala +++ b/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala @@ -38,9 +38,7 @@ class XLangVerificationSuite extends LeonRegressionSuite { fullName } - val ignored = List( - "regression/verification/xlang/valid/Nested15.scala" - ) + val ignored = List() val t = if (ignored.exists(displayName endsWith _)) { ignore _