diff --git a/src/it/scala/inox/ResourceUtils.scala b/src/it/scala/inox/ResourceUtils.scala index c43039166cd3392a50e8093042e291c25b1fd3c0..3c8a910b68e6461d1c29c88db937442bb05b38c8 100644 --- a/src/it/scala/inox/ResourceUtils.scala +++ b/src/it/scala/inox/ResourceUtils.scala @@ -11,8 +11,6 @@ import utils._ trait ResourceUtils { - val resourcesDir = "src/it/resources" - def resourceFiles(dir: String, filter: String => Boolean = (s: String) => true, recursive: Boolean = false): Seq[File] = { Option(getClass.getResource(s"/$dir")).toSeq.flatMap { url => val baseDir = new File(url.getPath) diff --git a/src/it/scala/inox/InoxTestSuite.scala b/src/it/scala/inox/TestSuite.scala similarity index 50% rename from src/it/scala/inox/InoxTestSuite.scala rename to src/it/scala/inox/TestSuite.scala index d94fcca6009063943a9b2bc7682b9051029e9f2c..229e55c40cf9560156f3643816f3f419d53ee2d3 100644 --- a/src/it/scala/inox/InoxTestSuite.scala +++ b/src/it/scala/inox/TestSuite.scala @@ -7,15 +7,18 @@ import org.scalatest.concurrent._ import utils._ -trait InoxTestSuite extends FunSuite with Matchers with Timeouts { +trait TestSuite extends FunSuite with Matchers with Timeouts { val configurations: Seq[Seq[OptionValue[_]]] = Seq(Seq.empty) - private def optionsString(options: Options): String = { - "solver=" + options.findOptionOrDefault(optSelectedSolvers).head + " " + - "feelinglucky=" + options.findOptionOrDefault(solvers.unrolling.optFeelingLucky) + " " + - "checkmodels=" + options.findOptionOrDefault(solvers.optCheckModels) + " " + - "unrollassumptions=" + options.findOptionOrDefault(solvers.unrolling.optUnrollAssumptions) + private val counter = new UniqueCounter[Unit] + counter.nextGlobal // Start at 1 + + protected def optionsString(options: Options): String = { + "solvr=" + options.findOptionOrDefault(optSelectedSolvers).head + " " + + "lucky=" + options.findOptionOrDefault(solvers.unrolling.optFeelingLucky) + " " + + "check=" + options.findOptionOrDefault(solvers.optCheckModels) + " " + + "assum=" + options.findOptionOrDefault(solvers.unrolling.optUnrollAssumptions) } protected def test(name: String, tags: Tag*)(body: Context => Unit): Unit = { @@ -23,7 +26,8 @@ trait InoxTestSuite extends FunSuite with Matchers with Timeouts { val reporter = new TestSilentReporter val ctx = Context(reporter, new InterruptManager(reporter), Options(config)) try { - super.test(name + " " + optionsString(ctx.options))(body(ctx)) + val index = counter.nextGlobal + super.test(f"$index%3d: $name ${optionsString(ctx.options)}")(body(ctx)) } catch { case err: FatalError => reporter.lastErrors :+= err.msg @@ -34,7 +38,8 @@ trait InoxTestSuite extends FunSuite with Matchers with Timeouts { protected def ignore(name: String, tags: Tag*)(body: Context => Unit): Unit = { for (config <- configurations) { - super.ignore(name + " " + optionsString(Options(config)))(()) + val index = counter.nextGlobal + super.ignore(f"$index%3d: $name ${optionsString(Options(config))}")(()) } } } diff --git a/src/it/scala/inox/solvers/SolvingTestSuite.scala b/src/it/scala/inox/solvers/SolvingTestSuite.scala index 17b9c8630f0649b11972ee21abeba31e315dcee0..2fe9c90e3b2fcc46cb7fc6266fb2f70861210f35 100644 --- a/src/it/scala/inox/solvers/SolvingTestSuite.scala +++ b/src/it/scala/inox/solvers/SolvingTestSuite.scala @@ -3,7 +3,7 @@ package inox package solvers -trait SolvingTestSuite extends InoxTestSuite { +trait SolvingTestSuite extends TestSuite { override val configurations = for { solverName <- Seq("nativez3", "unrollz3", "smt-z3", "smt-cvc4") diff --git a/src/it/scala/inox/solvers/unrolling/AssociativeQuantifiersSuite.scala b/src/it/scala/inox/solvers/unrolling/AssociativeQuantifiersSuite.scala index 4ebc09cb94215a38beaa8012bafde9346e880b8f..bb914c0536ec0418264b5d56af4479149f665673 100644 --- a/src/it/scala/inox/solvers/unrolling/AssociativeQuantifiersSuite.scala +++ b/src/it/scala/inox/solvers/unrolling/AssociativeQuantifiersSuite.scala @@ -4,7 +4,7 @@ package inox package solvers package unrolling -class AssociativeQuantifiersSuite extends InoxTestSuite { +class AssociativeQuantifiersSuite extends TestSuite { import inox.trees._ import dsl._