Skip to content
Snippets Groups Projects
Commit e04ac67a authored by Nicolas Voirol's avatar Nicolas Voirol Committed by Ravi
Browse files

Re-enabled AbstractEvaluator test and reset TerminationSuite to smt-z3

parent a73533f1
No related branches found
No related tags found
No related merge requests found
...@@ -65,7 +65,7 @@ object AbstractTests { ...@@ -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 testFd = funDef("AbstractTests.test2")
val Leaf = cc("AbstractTests.Leaf")() val Leaf = cc("AbstractTests.Leaf")()
def Node(left: Expr, n: Expr, right: Expr) = cc("AbstractTests.Node")(left, n, right) def Node(left: Expr, n: Expr, right: Expr) = cc("AbstractTests.Node")(left, n, right)
......
...@@ -68,7 +68,7 @@ class TerminationSuite extends LeonRegressionSuite { ...@@ -68,7 +68,7 @@ class TerminationSuite extends LeonRegressionSuite {
private def forEachFileIn(files: Iterable[File], forError: Boolean = false)(block : Output=>Unit) { private def forEachFileIn(files: Iterable[File], forError: Boolean = false)(block : Output=>Unit) {
for(f <- files) { for(f <- files) {
mkTest(f, Seq(), forError)(block) mkTest(f, Seq("--solvers=smt-z3"), forError)(block)
} }
} }
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment