From be0b137ebb42b422635dca27229ef7f6e6e78c2e Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Thu, 12 May 2016 10:03:44 +0200
Subject: [PATCH] Move more tests to smt-z3
---
.../leon/regression/repair/RepairSuite.scala | 19 +++----------------
.../synthesis/SynthesisRegressionSuite.scala | 2 +-
2 files changed, 4 insertions(+), 17 deletions(-)
diff --git a/src/test/scala/leon/regression/repair/RepairSuite.scala b/src/test/scala/leon/regression/repair/RepairSuite.scala
index 16f1ddb88..254c6a2f5 100644
--- a/src/test/scala/leon/regression/repair/RepairSuite.scala
+++ b/src/test/scala/leon/regression/repair/RepairSuite.scala
@@ -2,12 +2,10 @@
package leon.regression.repair
-import leon._
import leon.test._
import leon.utils._
import leon.frontends.scalac.ExtractionPhase
import leon.repair._
-import leon.verification.VerificationPhase
class RepairSuite extends LeonRegressionSuite {
val pipeline = ExtractionPhase andThen
@@ -31,23 +29,12 @@ class RepairSuite extends LeonRegressionSuite {
val path = file.getAbsoluteFile.toString
val name = file.getName
- val reporter = new TestSilentReporter
- //val reporter = new DefaultReporter(Set(utils.DebugSectionRepair))
-
- val ctx = new LeonContext(
- reporter = reporter,
- interruptManager = new InterruptManager(reporter),
- options = Seq(
- LeonOption(GlobalOptions.optFunctions)(Seq(fileToFun(name))),
- LeonOption(VerificationPhase.optParallelVCs)(true),
- LeonOption(GlobalOptions.optTimeout)(180L)
- )
- )
+ val ctx = createLeonContext("--parallel", "--timeout=180", "--solvers=smt-z3")
test(name) {
pipeline.run(ctx, List(path))
- if(reporter.errorCount > 0) {
- fail("Errors during repair:\n"+reporter.lastErrors.mkString("\n"))
+ if(ctx.reporter.errorCount > 0) {
+ fail("Errors during repair:\n"+ctx.reporter.asInstanceOf[TestSilentReporter].lastErrors.mkString("\n"))
}
}
}
diff --git a/src/test/scala/leon/regression/synthesis/SynthesisRegressionSuite.scala b/src/test/scala/leon/regression/synthesis/SynthesisRegressionSuite.scala
index 723c8319d..06abffdef 100644
--- a/src/test/scala/leon/regression/synthesis/SynthesisRegressionSuite.scala
+++ b/src/test/scala/leon/regression/synthesis/SynthesisRegressionSuite.scala
@@ -20,7 +20,7 @@ class SynthesisRegressionSuite extends LeonRegressionSuite {
}
private def testSynthesis(cat: String, f: File, bound: Int) {
- val ctx = createLeonContext("--synthesis")
+ val ctx = createLeonContext("--synthesis", "--solvers=smt-z3")
val pipeline = leon.frontends.scalac.ExtractionPhase andThen new leon.utils.PreprocessingPhase
--
GitLab