diff --git a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
index 811b4a2b980de6ffcc2d5484ebfaf8a9c31972fd..7a77450a7b41a8248b85fdddc3d19448588a9035 100644
--- a/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
+++ b/src/main/scala/leon/frontends/scalac/CodeExtraction.scala
@@ -527,6 +527,12 @@ trait CodeExtraction extends ASTExtractors {
 
         acd
       } else {
+        val ccd = CaseClassDef(id, tparams, parent, sym.isModuleClass).setPos(sym.pos)
+
+        parent.foreach(_.classDef.registerChildren(ccd))
+
+
+        classesToClasses += sym -> ccd
 
         val fields = args.map { case (symbol, t) =>
           val tpt = t.tpt
@@ -534,11 +540,7 @@ trait CodeExtraction extends ASTExtractors {
           LeonValDef(FreshIdentifier(symbol.name.toString, tpe).setPos(t.pos)).setPos(t.pos)
         }
 
-        val ccd = CaseClassDef(id, tparams, fields, parent, sym.isModuleClass).setPos(sym.pos)
-
-        parent.foreach(_.classDef.registerChildren(ccd))
-
-        classesToClasses += sym -> ccd
+        ccd.setFields(fields)
 
         // Validates type parameters
         parent foreach { pct =>
diff --git a/src/main/scala/leon/purescala/DefOps.scala b/src/main/scala/leon/purescala/DefOps.scala
index e7acc9a42f34f3b014ded101a86484d8747cac83..881a491f7074abbf6a183dca288ae2ba7eaf0ffa 100644
--- a/src/main/scala/leon/purescala/DefOps.scala
+++ b/src/main/scala/leon/purescala/DefOps.scala
@@ -22,7 +22,7 @@ object DefOps {
     case other => pgm.units.find(_.containsDef(df))
   }
 
-  private def pathFromRoot(df: Definition)(implicit pgm: Program): List[Definition] = {
+  private def pathFromRoot(df: Definition)(implicit pgm: Program): List[Definition] ={
     def rec(from: Definition): List[Definition] = {
       from :: (if (from == df) {
         Nil
diff --git a/src/main/scala/leon/purescala/Definitions.scala b/src/main/scala/leon/purescala/Definitions.scala
index eda9e8d3e65a9668885ec07927ea318c411784ee..21359f8ba7622c1f21ab6f71dbd50f524138fc01 100644
--- a/src/main/scala/leon/purescala/Definitions.scala
+++ b/src/main/scala/leon/purescala/Definitions.scala
@@ -207,11 +207,11 @@ object Definitions {
     }
 
     lazy val algebraicDataTypes : Map[AbstractClassDef, Seq[CaseClassDef]] = defs.collect {
-      case c@CaseClassDef(_, _, _, Some(p), _) => c
+      case c@CaseClassDef(_, _, Some(p), _) => c
     }.groupBy(_.parent.get.classDef)
 
     lazy val singleCaseClasses : Seq[CaseClassDef] = defs.collect {
-      case c @ CaseClassDef(_, _, _, None, _) => c
+      case c @ CaseClassDef(_, _, None, _) => c
     }
     
     def duplicate = copy(defs = defs map {
@@ -282,6 +282,7 @@ object Definitions {
       case cc : CaseClassDef => {
         val cc2 = cc.copy() 
         cc.methods foreach { m => cc2.registerMethod(m.duplicate) }
+        cc2.setFields(cc.fields map { _.copy() })
         cc2
       }
     }
@@ -307,12 +308,21 @@ object Definitions {
   /** Case classes/objects. */
   case class CaseClassDef(id: Identifier,
                           tparams: Seq[TypeParameterDef],
-                          fields: Seq[ValDef],
                           parent: Option[AbstractClassType],
                           isCaseObject: Boolean) extends ClassDef {
 
+    private var _fields = Seq[ValDef]()
+
+    def fields = _fields
+
+    def setFields(fields: Seq[ValDef]) {
+      _fields = fields
+    }
+
+
     val isAbstract = false
 
+
     def selectorID2Index(id: Identifier) : Int = {
       val index = fields.zipWithIndex.find(_._1.id == id).map(_._2)
 
diff --git a/src/main/scala/leon/purescala/PrettyPrinter.scala b/src/main/scala/leon/purescala/PrettyPrinter.scala
index bbee52fbfe443e1284b45de9f6ef0f56f4f700f7..e273e9e62f9e6b953602b0c0e9b29854d83bbdc6 100644
--- a/src/main/scala/leon/purescala/PrettyPrinter.scala
+++ b/src/main/scala/leon/purescala/PrettyPrinter.scala
@@ -487,7 +487,7 @@ class PrettyPrinter(opts: PrinterOptions,
               |}"""
         }
 
-      case ccd @ CaseClassDef(id, tparams, fields, parent, isObj) =>
+      case ccd @ CaseClassDef(id, tparams, parent, isObj) =>
         if (isObj) {
           p"case object $id"
         } else {
@@ -499,7 +499,7 @@ class PrettyPrinter(opts: PrinterOptions,
         }
 
         if (!isObj) {
-          p"($fields)"
+          p"(${ccd.fields})"
         }
 
         parent.foreach{ par =>
diff --git a/src/test/resources/regression/frontends/passing/ClassFields.scala b/src/test/resources/regression/frontends/passing/ClassFields.scala
new file mode 100644
index 0000000000000000000000000000000000000000..eda170f5074ec93cb5fbe6a159fb4006feeda0d6
--- /dev/null
+++ b/src/test/resources/regression/frontends/passing/ClassFields.scala
@@ -0,0 +1,6 @@
+import leon.lang._
+
+object ClassFields {
+  case class Foo(f : Option[Foo])
+}
+
diff --git a/src/test/scala/leon/test/verification/XLangVerificationSuite.scala b/src/test/scala/leon/test/verification/XLangVerificationSuite.scala
index aee24688750fd1547bf4f70f671efbd7d98cdcf4..4792a2b425471eeac9fe8bb10b1733ff8dafb96a 100644
--- a/src/test/scala/leon/test/verification/XLangVerificationSuite.scala
+++ b/src/test/scala/leon/test/verification/XLangVerificationSuite.scala
@@ -66,24 +66,14 @@ class XLangVerificationSuite extends LeonTestSuite {
       _.endsWith(".scala"))
 
     val isZ3Available = try {
-      Z3Interpreter.buildDefault
+      Z3Interpreter.buildDefault.free()
       true
     } catch {
       case e: java.io.IOException =>
         false
     }
 
-    val isCVC4Available = try {
-      CVC4Interpreter.buildDefault
-      // @EK: CVC4 works on most testcases already, but not all and thus cannot be used in regression.
-      true
-    } catch {
-      case e: java.io.IOException =>
-        false
-    }
-
-
-    for(f <- fs) {
+       for(f <- fs) {
       mkTest(f, List(), forError)(block)
       mkTest(f, List("--feelinglucky"), forError)(block)
       if (isZ3Available) {
@@ -100,7 +90,7 @@ class XLangVerificationSuite extends LeonTestSuite {
   }
 
   forEachFileIn("invalid") { output =>
-    val Output(report, reporter) = output
+    val Output(report, _) = output
     assert(report.totalInvalid > 0,
            "There should be at least one invalid verification condition.")
     assert(report.totalUnknown === 0,