diff --git a/src/main/scala/leon/package.scala b/src/main/scala/leon/package.scala
index 8a6a6904f3e6c2450f48b30cc939fe1d7f3b4368..bdf3a9e53c0d0425859ecb9ef29133f03925349d 100644
--- a/src/main/scala/leon/package.scala
+++ b/src/main/scala/leon/package.scala
@@ -4,4 +4,8 @@
   *
   * Provides the basic types and definitions for the Leon system.
   */
-package object leon { }
+package object leon {
+  implicit class BooleanToOption(cond: Boolean) {
+    def option[A](v: A) = if (cond) Some(v) else None
+  }
+}
diff --git a/src/main/scala/leon/verification/VerificationPhase.scala b/src/main/scala/leon/verification/VerificationPhase.scala
index c4b1427f04a87d10de6e9a19c56c5d6e46d0a9f3..e9a9fe60122b40d29bc94d7b15c32a6db6995e8e 100644
--- a/src/main/scala/leon/verification/VerificationPhase.scala
+++ b/src/main/scala/leon/verification/VerificationPhase.scala
@@ -7,7 +7,6 @@ import purescala.Definitions._
 import purescala.ExprOps._
 
 import scala.concurrent.duration._
-import java.lang.System
 
 import solvers._
 
diff --git a/src/test/scala/leon/regression/termination/TerminationSuite.scala b/src/test/scala/leon/regression/termination/TerminationSuite.scala
index 7096ad5dd5a2e2137a9f48aa9a98edd116bb1856..47eae872ed974863888987f3299ca6708164599f 100644
--- a/src/test/scala/leon/regression/termination/TerminationSuite.scala
+++ b/src/test/scala/leon/regression/termination/TerminationSuite.scala
@@ -33,6 +33,7 @@ class TerminationSuite extends LeonRegressionSuite {
     }
 
     val ignored = List(
+      "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 5d5679f95cadeb67e72b50532cede757cdf825cc..e54bfeef6c48aaf3d83d44978d597ede0a9c9f14 100644
--- a/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala
+++ b/src/test/scala/leon/regression/verification/purescala/PureScalaVerificationSuite.scala
@@ -1,9 +1,9 @@
 /* Copyright 2009-2016 EPFL, Lausanne */
 
-package leon.regression.verification
+package leon
+package regression.verification
 package purescala
 
-import smtlib.interpreters.{CVC4Interpreter, Z3Interpreter}
 import leon.solvers.SolverFactory
 
 // If you add another regression test, make sure it contains one object whose name matches the file name
@@ -20,16 +20,9 @@ abstract class PureScalaVerificationSuite extends VerificationSuite {
     List(
       List("--feelinglucky"),
       List("--codegen", /*"--evalground",*/ "--feelinglucky"),
-      List("--solvers=fairz3,enum", "--codegen", /*"--evalground",*/ "--feelinglucky")
-    ) ++ (
-      if (isZ3Available) List(
-        List("--solvers=smt-z3", "--feelinglucky")
-      ) else Nil
-    ) ++ (
-      if (isCVC4Available) List(
-        List("--solvers=smt-cvc4", "--feelinglucky")
-      ) else Nil
-    )
+      List("--solvers=fairz3,enum", "--codegen", /*"--evalground",*/ "--feelinglucky")) ++
+      isZ3Available.option(List("--solvers=smt-z3", "--feelinglucky")) ++
+      isCVC4Available.option(List("--solvers=smt-cvc4", "--feelinglucky"))
   }
 
 }
@@ -49,13 +42,25 @@ class PureScalaValidSuite3 extends PureScalaValidSuite {
   override val ignored = Seq("valid/Predicate.scala")
 }
 class PureScalaValidSuiteZ3 extends PureScalaValidSuite {
-  val optionVariants = if (isZ3Available) List(opts(3)) else Nil
+  val optionVariants = isZ3Available.option(opts(3)).toList
 }
 class PureScalaValidSuiteCVC4 extends PureScalaValidSuite {
-  val optionVariants = if (isCVC4Available) opts.takeRight(1) else Nil
+  val optionVariants = isCVC4Available.option(opts.last).toList
 }
 
-class PureScalaInvalidSuite extends PureScalaVerificationSuite {
+trait PureScalaInvalidSuite extends PureScalaVerificationSuite {
   override def testAll() = testInvalid()
-  val optionVariants = opts
+}
+
+class PureScalaInvalidSuiteFairZ3 extends PureScalaInvalidSuite {
+  val optionVariants = opts.take(3)
+}
+
+class PureScalaInvalidSuiteCVC4 extends PureScalaInvalidSuite {
+  val optionVariants = isCVC4Available.option(opts.last).toList
+  override val ignored = List("invalid/BinarySearchTreeQuant.scala", "valid/PropositionalLogic.scala")
+}
+
+class PureScalaInvalidSuiteZ3 extends PureScalaInvalidSuite {
+  val optionVariants = isZ3Available.option(opts(3)).toList
 }