diff --git a/src/test/scala/leon/genc/GenCSuite.scala b/src/test/scala/leon/genc/GenCSuite.scala
index d9fe551bfe5b2e2a3f9abe4acebf6019828a78af..a8e0368eef6baa1416a14fd492f645ffa53078f2 100644
--- a/src/test/scala/leon/genc/GenCSuite.scala
+++ b/src/test/scala/leon/genc/GenCSuite.scala
@@ -180,20 +180,23 @@ class GenCSuite extends LeonRegressionSuite {
     }
   }
 
-  protected def verifyValidTests() = {
-    class AltVerificationSuite(override val testDir: String) extends XLangVerificationSuite {
-      def run() = testValid() // Test only the valid ones
-    }
+  class AltVerificationSuite(override val testDir: String) extends XLangVerificationSuite {
+    override def testAll() = testValid() // Test only the valid ones
 
-    // Use our test dir and not the one from XLangVerificationSuite
-    val verifier = new AltVerificationSuite(testDir)
+    override def suiteName = "Verification Suite For GenC"
 
-    test("verifying test cases") { verifier.run() }
+    // Add a timeout for the verification
+    override def optionVariants =
+      super.optionVariants map { opts => "--timeout=5" :: opts }
   }
 
-  protected def testAll() = {
-    verifyValidTests()
+  // Run verification suite as a nested suite
+  override def nestedSuites = {
+    // Use our test dir and not the one from XLangVerificationSuite
+    scala.collection.immutable.IndexedSeq(new AltVerificationSuite(testDir))
+  }
 
+  protected def testAll() = {
     // Set C compiler according to the platform we're currently running on
     detectCompiler match {
       case Some(cc) => testValid(cc)
diff --git a/src/test/scala/leon/regression/verification/VerificationSuite.scala b/src/test/scala/leon/regression/verification/VerificationSuite.scala
index b23fb0c4e3516121a1489752ed89dcb0835ee2d2..d7eafb38c80075092d4c57ab25e83e9c80b5573d 100644
--- a/src/test/scala/leon/regression/verification/VerificationSuite.scala
+++ b/src/test/scala/leon/regression/verification/VerificationSuite.scala
@@ -19,7 +19,7 @@ import org.scalatest.{Reporter => _, _}
 // This is because we compile all tests from each folder together.
 trait VerificationSuite extends LeonRegressionSuite {
 
-  val optionVariants: List[List[String]]
+  def optionVariants: List[List[String]]
   val testDir: String
 
   val ignored: Seq[String] = Seq()
@@ -81,7 +81,7 @@ trait VerificationSuite extends LeonRegressionSuite {
   private[verification] def forEachFileIn(cat: String)(block: Output => Unit) {
     val fs = filesInResourceDir(testDir + cat, _.endsWith(".scala")).toList
 
-    fs foreach { file => 
+    fs foreach { file =>
       assert(file.exists && file.isFile && file.canRead,
         s"Benchmark ${file.getName} is not a readable file")
     }
diff --git a/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala b/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala
index 0136b7b06643985265c738e39402e6a3d3d33f99..0b6a0c37d99277ce64ba3e095e13e78cb478bd7b 100644
--- a/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala
+++ b/src/test/scala/leon/regression/verification/XLangVerificationSuite.scala
@@ -9,7 +9,7 @@ import leon.solvers.SolverFactory
 // This is because we compile all tests from each folder together.
 class XLangVerificationSuite extends VerificationSuite {
 
-  val optionVariants: List[List[String]] = {
+  def optionVariants: List[List[String]] = {
     val isZ3Available = SolverFactory.hasZ3
 
     List(