Attempt at reducing native-z3 parallelism during tests

.larabot.conf

@@ -2,6 +2,7 @@ commands = [
     "sbt -batch -Dparallel=10 test"
     "sbt -batch -Dparallel=10 integration:test"
     "sbt -batch -Dparallel=10 regression:test"
+    "sbt -batch -Dparallel=10 native:test"
     "sbt -batch -Dparallel=10 genc:test"
     "sbt -batch -Dparallel=10 isabelle:test"
 ]

build.sbt

@@ -148,12 +148,19 @@ lazy val IntegrTest = config("integration") extend(Test)
 testOptions in IntegrTest := Seq(Tests.Argument("-oDF"), Tests.Filter(_ startsWith "leon.integration."))
 
 
+def regressionFilter(name: String, native: Boolean = false): Boolean = name.startsWith("leon.regression") && (name.endsWith("NativeZ3") == native)
 
 // Regression Tests
 lazy val RegressionTest = config("regression") extend(Test)
 
-testOptions in RegressionTest := Seq(Tests.Argument("-oDF"), Tests.Filter(_ startsWith "leon.regression."))
+testOptions in RegressionTest := Seq(Tests.Argument("-oDF"), Tests.Filter(regressionFilter(_)))
 
+// Regression Tests that heavily depend on native Z3
+lazy val NativeZ3RegressionTest = config("native") extend(Test)
+
+testOptions in NativeZ3RegressionTest := Seq(Tests.Argument("-oDF"), Tests.Filter(regressionFilter(_, native = true)))
+
+parallelExecution in NativeZ3RegressionTest := false
 
 
 // Isabelle Tests
@@ -179,9 +186,10 @@ lazy val bonsai      = ghProject("git://github.com/colder/bonsai.git",     "10ea
 lazy val scalaSmtlib = ghProject("git://github.com/regb/scala-smtlib.git", "57834acfe2e3bc36862be52e4d99829bb8ff0ca7")
 
 lazy val root = (project in file(".")).
-  configs(RegressionTest, IsabelleTest, GenCTest, IntegrTest).
+  configs(RegressionTest, NativeZ3RegressionTest, IsabelleTest, GenCTest, IntegrTest).
   dependsOn(bonsai).
   dependsOn(scalaSmtlib).
+  settings(inConfig(NativeZ3RegressionTest)(Defaults.testTasks ++ testSettings): _*).
   settings(inConfig(RegressionTest)(Defaults.testTasks ++ testSettings): _*).
   settings(inConfig(IntegrTest)(Defaults.testTasks ++ testSettings): _*).
   settings(inConfig(IsabelleTest)(Defaults.testTasks ++ testSettings): _*).

src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala

@@ -32,13 +32,13 @@ trait PureScalaValidSuite extends PureScalaVerificationSuite {
   override def testAll() = testValid()
 }
 
-class PureScalaValidSuite1 extends PureScalaValidSuite {
+class PureScalaValidSuiteLuckyNativeZ3 extends PureScalaValidSuite {
   val optionVariants = List(opts(0))
 }
-class PureScalaValidSuite2 extends PureScalaValidSuite {
+class PureScalaValidSuiteCodeGenNativeZ3 extends PureScalaValidSuite {
   val optionVariants = List(opts(1))
 }
-class PureScalaValidSuite3 extends PureScalaValidSuite { // tests verification with --codegen parameter
+class PureScalaValidSuiteEnumNativeZ3 extends PureScalaValidSuite {
   val optionVariants = List(opts(2))
   override val ignored = Seq("valid/Predicate.scala","valid/TraceInductTacticTest.scala")
 }
@@ -53,10 +53,14 @@ trait PureScalaInvalidSuite extends PureScalaVerificationSuite {
   override def testAll() = testInvalid()
 }
 
-class PureScalaInvalidSuiteFairZ3 extends PureScalaInvalidSuite {
+class PureScalaInvalidSuiteNativeZ3 extends PureScalaInvalidSuite {
   val optionVariants = opts.take(3)
 }
 
+class PureScalaInvalidSuiteZ3 extends PureScalaInvalidSuite {
+  val optionVariants = isZ3Available.option(opts(3)).toList
+}
+
 class PureScalaInvalidSuiteCVC4 extends PureScalaInvalidSuite {
   val optionVariants = isCVC4Available.option(opts.last).toList
   override val ignored = List(
@@ -66,6 +70,3 @@ class PureScalaInvalidSuiteCVC4 extends PureScalaInvalidSuite {
   )
 }
 
-class PureScalaInvalidSuiteZ3 extends PureScalaInvalidSuite {
-  val optionVariants = isZ3Available.option(opts(3)).toList
-}