From e04ac67a3d84a37fc4ff43a6ed16183df3be8c94 Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Wed, 27 Apr 2016 22:37:05 +0200
Subject: [PATCH] Re-enabled AbstractEvaluator test and reset TerminationSuite
to smt-z3
---
.../leon/integration/evaluators/AbstractEvaluatorSuite.scala | 2 +-
.../scala/leon/regression/termination/TerminationSuite.scala | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/test/scala/leon/integration/evaluators/AbstractEvaluatorSuite.scala b/src/test/scala/leon/integration/evaluators/AbstractEvaluatorSuite.scala
index 583bb3230..385d407e0 100644
--- a/src/test/scala/leon/integration/evaluators/AbstractEvaluatorSuite.scala
+++ b/src/test/scala/leon/integration/evaluators/AbstractEvaluatorSuite.scala
@@ -65,7 +65,7 @@ object AbstractTests {
}
}
- ignore("Abstract evaluator should correctly handle boolean and recursive") { implicit fix =>
+ test("Abstract evaluator should correctly handle boolean and recursive") { implicit fix =>
val testFd = funDef("AbstractTests.test2")
val Leaf = cc("AbstractTests.Leaf")()
def Node(left: Expr, n: Expr, right: Expr) = cc("AbstractTests.Node")(left, n, right)
diff --git a/src/test/scala/leon/regression/termination/TerminationSuite.scala b/src/test/scala/leon/regression/termination/TerminationSuite.scala
index 5aa1d7891..876ad77bd 100644
--- a/src/test/scala/leon/regression/termination/TerminationSuite.scala
+++ b/src/test/scala/leon/regression/termination/TerminationSuite.scala
@@ -68,7 +68,7 @@ class TerminationSuite extends LeonRegressionSuite {
private def forEachFileIn(files: Iterable[File], forError: Boolean = false)(block : Output=>Unit) {
for(f <- files) {
- mkTest(f, Seq(), forError)(block)
+ mkTest(f, Seq("--solvers=smt-z3"), forError)(block)
}
}
--
GitLab