diff --git a/.gitignore b/.gitignore
index 12c115fd5406d34c00099a8c03d1fd5b04b575f2..eac146feb701eca372077ae98c07f034477b0573 100644
--- a/.gitignore
+++ b/.gitignore
@@ -7,6 +7,7 @@ target
/leon
/setupenv
/leon-bench
+/.test-history
# synthesis
derivation*.dot
diff --git a/build.sbt b/build.sbt
index 651417296e6121611099096af3ad83b4d2446110..4fe1fed09e3957e2cf28679c6150909b77bb78f4 100644
--- a/build.sbt
+++ b/build.sbt
@@ -24,10 +24,14 @@ resolvers += "Typesafe Repository" at "http://repo.typesafe.com/typesafe/release
libraryDependencies ++= Seq(
"org.scala-lang" % "scala-compiler" % "2.10.2",
- "org.scalatest" %% "scalatest" % "1.9.1" excludeAll(ExclusionRule(organization="org.scala-lang")),
+ "org.scalatest" % "scalatest_2.10" % "2.0.M5b" % "test" excludeAll(ExclusionRule(organization="org.scala-lang")),
"com.typesafe.akka" %% "akka-actor" % "2.2.0" excludeAll(ExclusionRule(organization="org.scala-lang"))
)
fork in run := true
fork in test := true
+
+logBuffered in Test := false
+
+testOptions in Test += Tests.Argument("-oD")
diff --git a/src/test/scala/leon/test/LeonTestSuite.scala b/src/test/scala/leon/test/LeonTestSuite.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2dd0a92ebadd6c0afb58a972853d6c88559a44aa
--- /dev/null
+++ b/src/test/scala/leon/test/LeonTestSuite.scala
@@ -0,0 +1,86 @@
+package leon.test
+import scala.io.Source
+import org.scalatest._
+
+trait LeonTestSuite extends FunSuite {
+ def now() = {
+ System.currentTimeMillis
+ }
+
+ case class Statistics(values: List[Long]) {
+ val n = values.size
+ val avg = values.sum.toDouble/n
+ val stddev = Math.sqrt(Math.abs(values.map(_.toDouble - avg).sum/n))
+
+ def accountsFor(ms: Long) = {
+ if (n < 5) {
+ true
+ } else {
+ val msd = ms.toDouble
+ (msd < avg + 3*stddev + 20)
+ }
+ }
+
+ def withValue(v: Long) = this.copy(v :: values)
+ }
+
+ def testIdentifier(name: String): String = {
+ (this.getClass.getName+"-"+name).replaceAll("[^0-9a-zA-Z-]", "")
+ }
+
+ def bookKeepingFile(id: String) = {
+ import java.io.File
+
+ val f = new File(System.getProperty("user.dir")+"/.test-history/"+id+".log");
+
+ f.getParentFile.mkdirs()
+
+ f
+ }
+
+ def getStats(id: String): Statistics = {
+ val f = bookKeepingFile(id)
+
+ if (f.canRead()) {
+ Statistics(Source.fromFile(f).getLines.flatMap{ line =>
+ val l = line.trim
+ if (l.length > 0) {
+ Some(line.toLong)
+ } else {
+ None
+ }
+ }.toList)
+ } else {
+ Statistics(Nil)
+ }
+ }
+
+ def storeStats(id: String, stats: Statistics) {
+ import java.io.FileWriter
+
+ val f = bookKeepingFile(id)
+
+ val fw = new FileWriter(f, true)
+ fw.write(stats.values.head+"\n")
+ fw.close
+ }
+
+ override def test(name: String, tags: Tag*)(body: => Unit) {
+ super.test(name, tags: _*) {
+ val id = testIdentifier(name)
+ val ts = now()
+
+ body
+
+ val total = now()-ts
+
+ val stats = getStats(id)
+
+ if (!stats.accountsFor(total)) {
+ fail("Test took too long to run: "+total+"ms (avg: "+stats.avg+", stddev: "+stats.stddev+")")
+ }
+
+ storeStats(id, stats.withValue(total))
+ }
+ }
+}
diff --git a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
index 9fd88e13b3583b513f8260b92fd0bd694130b374..edcc0c9b5f1a56ea16e0abdf4877e212b3365f30 100644
--- a/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
+++ b/src/test/scala/leon/test/evaluators/EvaluatorsTests.scala
@@ -14,9 +14,7 @@ import leon.purescala.Definitions._
import leon.purescala.Trees._
import leon.purescala.TypeTrees._
-import org.scalatest.FunSuite
-
-class EvaluatorsTests extends FunSuite {
+class EvaluatorsTests extends LeonTestSuite {
private implicit lazy val leonContext = LeonContext(
settings = Settings(
synthesis = false,
diff --git a/src/test/scala/leon/test/purescala/DataGen.scala b/src/test/scala/leon/test/purescala/DataGen.scala
index b188291bb3a83b8f2184bf13d9cb04460677816f..99659fb690edd55b67641d2117b120dd7b21a4e5 100644
--- a/src/test/scala/leon/test/purescala/DataGen.scala
+++ b/src/test/scala/leon/test/purescala/DataGen.scala
@@ -16,7 +16,7 @@ import leon.evaluators._
import org.scalatest.FunSuite
-class DataGen extends FunSuite {
+class DataGen extends LeonTestSuite {
private implicit lazy val leonContext = LeonContext(
settings = Settings(
synthesis = false,
diff --git a/src/test/scala/leon/test/purescala/LikelyEqSuite.scala b/src/test/scala/leon/test/purescala/LikelyEqSuite.scala
index 3a4fa9371f6dcf36663ea00798aaac7d76900819..54531aa35c6a99caae21268fb0f79ddfab681882 100644
--- a/src/test/scala/leon/test/purescala/LikelyEqSuite.scala
+++ b/src/test/scala/leon/test/purescala/LikelyEqSuite.scala
@@ -1,14 +1,13 @@
/* Copyright 2009-2013 EPFL, Lausanne */
-package leon.test.purescala
-
-import org.scalatest.FunSuite
+package leon.test
+package purescala
import leon.purescala.Common._
import leon.purescala.Trees._
-class LikelyEqSuite extends FunSuite {
+class LikelyEqSuite extends LeonTestSuite {
def i(x: Int) = IntLiteral(x)
val xId = FreshIdentifier("x")
diff --git a/src/test/scala/leon/test/purescala/TreeNormalizationsTests.scala b/src/test/scala/leon/test/purescala/TreeNormalizationsTests.scala
index 42ac12758392346d063ed308d4cb926e39392ba9..5d788ef2e7a34e479d9fe674b0a10e0e86a958c9 100644
--- a/src/test/scala/leon/test/purescala/TreeNormalizationsTests.scala
+++ b/src/test/scala/leon/test/purescala/TreeNormalizationsTests.scala
@@ -10,9 +10,7 @@ import leon.purescala.Trees._
import leon.purescala.TreeOps._
import leon.purescala.TreeNormalizations._
-import org.scalatest.FunSuite
-
-class TreeNormalizationsTests extends FunSuite {
+class TreeNormalizationsTests extends LeonTestSuite {
def i(x: Int) = IntLiteral(x)
val xId = FreshIdentifier("x").setType(Int32Type)
diff --git a/src/test/scala/leon/test/purescala/TreeOpsTests.scala b/src/test/scala/leon/test/purescala/TreeOpsTests.scala
index 42ccca7192a98c8630a12d80596f5c96f9cfb63c..823383baf499e319ccdd66e5ef83c6273eee167c 100644
--- a/src/test/scala/leon/test/purescala/TreeOpsTests.scala
+++ b/src/test/scala/leon/test/purescala/TreeOpsTests.scala
@@ -11,9 +11,7 @@ import leon.purescala.Trees._
import leon.purescala.TypeTrees._
import leon.purescala.TreeOps._
-import org.scalatest.FunSuite
-
-class TreeOpsTests extends FunSuite {
+class TreeOpsTests extends LeonTestSuite {
private val silentContext = LeonContext(reporter = new TestSilentReporter)
test("Path-aware simplifications") {
diff --git a/src/test/scala/leon/test/purescala/TreeTests.scala b/src/test/scala/leon/test/purescala/TreeTests.scala
index 45c341d494d6009c942258f78a553f2a70b2e06b..0d46e8fb96f7230a1290407317e27294d7ce9f0d 100644
--- a/src/test/scala/leon/test/purescala/TreeTests.scala
+++ b/src/test/scala/leon/test/purescala/TreeTests.scala
@@ -1,15 +1,14 @@
/* Copyright 2009-2013 EPFL, Lausanne */
-package leon.test.purescala
+package leon.test
+package purescala
import leon.purescala.Common._
import leon.purescala.Definitions._
import leon.purescala.Trees._
import leon.purescala.TypeTrees._
-import org.scalatest.FunSuite
-
-class TreeTests extends FunSuite {
+class TreeTests extends LeonTestSuite {
test("And- and Or- simplifications") {
val x = Variable(FreshIdentifier("x").setType(BooleanType))
diff --git a/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala b/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala
index 46278779009648037fee20f461c87dade92de699..954d30e65edb7294fa13d0d12d10a85cc5fc530e 100644
--- a/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala
+++ b/src/test/scala/leon/test/solvers/TimeoutSolverTests.scala
@@ -1,8 +1,7 @@
/* Copyright 2009-2013 EPFL, Lausanne */
-package leon.test.solvers
-
-import org.scalatest.FunSuite
+package leon.test
+package solvers
import leon._
import leon.solvers._
@@ -11,7 +10,7 @@ import leon.purescala.Definitions._
import leon.purescala.Trees._
import leon.purescala.TypeTrees._
-class TimeoutSolverTests extends FunSuite {
+class TimeoutSolverTests extends LeonTestSuite {
private class IdioticSolver(ctx : LeonContext) extends Solver(ctx) with NaiveIncrementalSolver {
val name = "Idiotic"
val description = "Loops when it doesn't know"
diff --git a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
index 4e479a835c6be9ea3ac75f800062e96032eeee55..68a41d0ce237d491801fe86fc59b8c75788b87eb 100644
--- a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
+++ b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTests.scala
@@ -14,9 +14,7 @@ import leon.purescala.TypeTrees._
import leon.solvers.Solver
import leon.solvers.z3.FairZ3Solver
-import org.scalatest.FunSuite
-
-class FairZ3SolverTests extends FunSuite {
+class FairZ3SolverTests extends LeonTestSuite {
private var testCounter : Int = 0
private def solverCheck(solver : Solver, expr : Expr, expected : Option[Boolean], msg : String) = {
testCounter += 1
diff --git a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
index 53bac4d7cf0b80a1f2cd722d1b35cdb9062ae48a..802bd13f057f873d764b234dd51e166138b198e0 100644
--- a/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
+++ b/src/test/scala/leon/test/solvers/z3/FairZ3SolverTestsNewAPI.scala
@@ -14,9 +14,7 @@ import leon.purescala.TypeTrees._
import leon.solvers.Solver
import leon.solvers.z3.FairZ3Solver
-import org.scalatest.FunSuite
-
-class FairZ3SolverTestsNewAPI extends FunSuite {
+class FairZ3SolverTestsNewAPI extends LeonTestSuite {
private var testCounter : Int = 0
private def solverCheck(solver : Solver, expr : Expr, expected : Option[Boolean], msg : String) = {
testCounter += 1
diff --git a/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala b/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
index e9d87d641f9046074b52af25ade639096fd5cc39..339d5bf2a0af1aebee6e4231be594cfed8cfe876 100644
--- a/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
+++ b/src/test/scala/leon/test/solvers/z3/UninterpretedZ3SolverTests.scala
@@ -14,9 +14,7 @@ import leon.purescala.TypeTrees._
import leon.solvers.Solver
import leon.solvers.z3.UninterpretedZ3Solver
-import org.scalatest.FunSuite
-
-class UninterpretedZ3SolverTests extends FunSuite {
+class UninterpretedZ3SolverTests extends LeonTestSuite {
private var testCounter : Int = 0
private def solverCheck(solver : Solver, expr : Expr, expected : Option[Boolean], msg : String) = {
testCounter += 1
diff --git a/src/test/scala/leon/test/synthesis/AlgebraSuite.scala b/src/test/scala/leon/test/synthesis/AlgebraSuite.scala
index 88fce145020da5d0fa2e4c39404f44b595b0cd82..aef22779ea5fe3cba9ac4cbbc90779e0196ecefc 100644
--- a/src/test/scala/leon/test/synthesis/AlgebraSuite.scala
+++ b/src/test/scala/leon/test/synthesis/AlgebraSuite.scala
@@ -1,12 +1,11 @@
/* Copyright 2009-2013 EPFL, Lausanne */
-package leon.test.synthesis
-
-import org.scalatest.FunSuite
+package leon.test
+package synthesis
import leon.synthesis.Algebra._
-class AlgebraSuite extends FunSuite {
+class AlgebraSuite extends LeonTestSuite {
test("remainder") {
assert(remainder(1,1) === 0)
diff --git a/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala b/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala
index bd83fba3f93b28a5cdd6309692eea330b650da72..03b3e66a87e68ca8fd126433b10f8442d98d891f 100644
--- a/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala
+++ b/src/test/scala/leon/test/synthesis/LinearEquationsSuite.scala
@@ -1,8 +1,7 @@
/* Copyright 2009-2013 EPFL, Lausanne */
-package leon.test.synthesis
-
-import org.scalatest.FunSuite
+package leon.test
+package synthesis
import leon.purescala.Trees._
import leon.purescala.TypeTrees._
@@ -12,7 +11,7 @@ import leon.test.purescala.LikelyEq
import leon.synthesis.LinearEquations._
-class LinearEquationsSuite extends FunSuite {
+class LinearEquationsSuite extends LeonTestSuite {
def i(x: Int) = IntLiteral(x)
diff --git a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
index 0f512690d094b2a9bdbc3c8ca98e1cc10091fbac..d134c980ed73b2d8ea5c9a0e1686a4f6698d3e2d 100644
--- a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
+++ b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala
@@ -12,12 +12,11 @@ import leon.solvers.Solver
import leon.synthesis._
import leon.synthesis.utils._
-import org.scalatest.FunSuite
import org.scalatest.matchers.ShouldMatchers._
import java.io.{BufferedWriter, FileWriter, File}
-class SynthesisSuite extends FunSuite {
+class SynthesisSuite extends LeonTestSuite {
private var counter : Int = 0
private def nextInt() : Int = {
counter += 1
diff --git a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
index 5dd93cbed0e993046de03d2a3280163139273528..45374ca5e90436eb662fb5a1aff59dcda12af0f8 100644
--- a/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/PureScalaVerificationRegression.scala
@@ -6,13 +6,11 @@ package verification
import leon.verification.{AnalysisPhase,VerificationReport}
-import org.scalatest.FunSuite
-
import java.io.File
import TestUtils._
-class PureScalaVerificationRegression extends FunSuite {
+class PureScalaVerificationRegression extends LeonTestSuite {
private var counter : Int = 0
private def nextInt() : Int = {
counter += 1
diff --git a/src/test/scala/leon/test/verification/XLangVerificationRegression.scala b/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
index d85a5dd6faddb3b231642cb2a0d63a2a3848ffa1..64b523de9efb613d8f12e999e6b7fb96ef026605 100644
--- a/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
+++ b/src/test/scala/leon/test/verification/XLangVerificationRegression.scala
@@ -6,13 +6,11 @@ package verification
import leon.verification.{AnalysisPhase,VerificationReport}
-import org.scalatest.FunSuite
-
import java.io.File
import TestUtils._
-class XLangVerificationRegression extends FunSuite {
+class XLangVerificationRegression extends LeonTestSuite {
private var counter : Int = 0
private def nextInt() : Int = {
counter += 1