diff --git a/src/test/scala/leon/regression/termination/TerminationSuite.scala b/src/test/scala/leon/regression/termination/TerminationSuite.scala index ae8e6725a75133ce50ab7734198efa56ebdcaffd..52984ac7a781fd1c8b4e058bbadd094337260f87 100644 --- a/src/test/scala/leon/regression/termination/TerminationSuite.scala +++ b/src/test/scala/leon/regression/termination/TerminationSuite.scala @@ -33,7 +33,7 @@ class TerminationSuite extends LeonRegressionSuite { } val ignored = List( - //"termination/valid/NNF.scala", + "termination/valid/NNF.scala", //"verification/purescala/valid/MergeSort.scala", "verification/purescala/valid/Nested14.scala" ) diff --git a/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala b/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala index e54bfeef6c48aaf3d83d44978d597ede0a9c9f14..fb9b608cb39431ea06462482df0643d111806f38 100644 --- a/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala +++ b/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala @@ -23,6 +23,7 @@ abstract class PureScalaVerificationSuite extends VerificationSuite { List("--solvers=fairz3,enum", "--codegen", /*"--evalground",*/ "--feelinglucky")) ++ isZ3Available.option(List("--solvers=smt-z3", "--feelinglucky")) ++ isCVC4Available.option(List("--solvers=smt-cvc4", "--feelinglucky")) + .map( _ :+ "--timeout=60") } }