diff --git a/src/funcheck/AnalysisComponent.scala b/src/funcheck/AnalysisComponent.scala
index 30d73b01546d1344b0b0a16c909f751bcd2287df..7529c3a677af08a14c1891d00d1eefa470e3c912 100644
--- a/src/funcheck/AnalysisComponent.scala
+++ b/src/funcheck/AnalysisComponent.scala
@@ -18,13 +18,6 @@ class AnalysisComponent(val global: Global, val pluginInstance: FunCheckPlugin)
   /** this is initialized when the Funcheck phase starts*/
   var fresh: scala.tools.nsc.util.FreshNameCreator = null 
   
-  protected def stopIfErrors: Unit = {
-    if(reporter.hasErrors) {
-      println("There were errors.")
-      exit(0)
-    }
-  }
-
   def newPhase(prev: Phase) = new AnalysisPhase(prev)
 
   class AnalysisPhase(prev: Phase) extends StdPhase(prev) {
diff --git a/src/funcheck/CLP.scala b/src/funcheck/CP.scala
similarity index 100%
rename from src/funcheck/CLP.scala
rename to src/funcheck/CP.scala
diff --git a/src/funcheck/CodeExtraction.scala b/src/funcheck/CodeExtraction.scala
index 23562e7740363a7c79d76e7ee0ccb575332d3d73..143832488d656d9da9e9c0e10bf15f1d22124645 100644
--- a/src/funcheck/CodeExtraction.scala
+++ b/src/funcheck/CodeExtraction.scala
@@ -9,7 +9,7 @@ import purescala.TypeTrees._
 import purescala.Common._
 
 trait CodeExtraction extends Extractors {
-  self: AnalysisComponent =>
+  // self: AnalysisComponent =>
 
   import global._
   import global.definitions._
@@ -25,6 +25,13 @@ trait CodeExtraction extends Extractors {
     scala.collection.mutable.Map.empty[Symbol,ClassTypeDef]
   private val defsToDefs: scala.collection.mutable.Map[Symbol,FunDef] =
     scala.collection.mutable.Map.empty[Symbol,FunDef]
+  
+  protected def stopIfErrors: Unit = {
+    if(reporter.hasErrors) {
+      println("There were errors.")
+      exit(0)
+    }
+  }
 
   def extractCode(unit: CompilationUnit): Program = { 
     import scala.collection.mutable.HashMap
diff --git a/src/funcheck/FunCheckPlugin.scala b/src/funcheck/FunCheckPlugin.scala
index 09ba190b4042dd9f2e932817ace22b501d883042..e6e26bfe940b0174ccc792536e575a95186b6514 100644
--- a/src/funcheck/FunCheckPlugin.scala
+++ b/src/funcheck/FunCheckPlugin.scala
@@ -68,4 +68,4 @@ class FunCheckPlugin(val global: Global) extends Plugin {
     }
   }
 
-  val components = List[PluginComponent](new AnalysisComponent(global, this))}
+  val components = List[PluginComponent](new AnalysisComponent(global, this), new CPComponent(global, this))}
diff --git a/src/purescala/Common.scala b/src/purescala/Common.scala
index 3c1abef7d9fa2b9173133b32e5283b8c1039ecff..a528df50db387cdc6799c14040c61753259efec3 100644
--- a/src/purescala/Common.scala
+++ b/src/purescala/Common.scala
@@ -5,7 +5,7 @@ object Common {
   import TypeTrees.Typed
 
   // the type is left blank (Untyped) for Identifiers that are not variables
-  class Identifier private[Common](val name: String, val id: Int, alwaysShowUniqueID: Boolean = false) extends Typed {
+  @serializable class Identifier private[Common](val name: String, val id: Int, alwaysShowUniqueID: Boolean = false) extends Typed {
     override def equals(other: Any): Boolean = {
       if(other == null || !other.isInstanceOf[Identifier])
         false
diff --git a/src/purescala/Definitions.scala b/src/purescala/Definitions.scala
index 11e6d35effcd94b4195adfea32b2bf9dc4cf5b26..9faaa6b03db2f8be9951e51251c53fd03b767b55 100644
--- a/src/purescala/Definitions.scala
+++ b/src/purescala/Definitions.scala
@@ -147,7 +147,7 @@ object Definitions {
       if(acd == null) None else Some((acd.id, acd.parent))
     }
   }
-  class AbstractClassDef(val id: Identifier, prnt: Option[AbstractClassDef] = None) extends ClassTypeDef {
+  @serializable class AbstractClassDef(val id: Identifier, prnt: Option[AbstractClassDef] = None) extends ClassTypeDef {
     private var parent_ = prnt
     var fields: VarDecls = Nil
     val isAbstract = true
@@ -187,7 +187,7 @@ object Definitions {
     }
   }
 
-  class CaseClassDef(val id: Identifier, prnt: Option[AbstractClassDef] = None) extends ClassTypeDef with ExtractorTypeDef {
+  @serializable class CaseClassDef(val id: Identifier, prnt: Option[AbstractClassDef] = None) extends ClassTypeDef with ExtractorTypeDef {
     private var parent_ = prnt
     var fields: VarDecls = Nil
     val isAbstract = false
@@ -242,7 +242,7 @@ object Definitions {
       }
     }
   }
-  class FunDef(val id: Identifier, val returnType: TypeTree, val args: VarDecls) extends Definition with ScalacPositional {
+  @serializable class FunDef(val id: Identifier, val returnType: TypeTree, val args: VarDecls) extends Definition with ScalacPositional {
     var body: Option[Expr] = None
     var precondition: Option[Expr] = None
     var postcondition: Option[Expr] = None
diff --git a/src/purescala/Trees.scala b/src/purescala/Trees.scala
index 33e5529004f544fefe4bb40cc1cecb0d841b14d0..ee4f69d10b986d6ba9f5fbd9ba6b31deae18fe4a 100644
--- a/src/purescala/Trees.scala
+++ b/src/purescala/Trees.scala
@@ -50,7 +50,7 @@ object Trees {
     def unapply(me: MatchExpr) : Option[(Expr,Seq[MatchCase])] = if (me == null) None else Some((me.scrutinee, me.cases))
   }
 
-  class MatchExpr(val scrutinee: Expr, val cases: Seq[MatchCase]) extends Expr with ScalacPositional {
+  @serializable class MatchExpr(val scrutinee: Expr, val cases: Seq[MatchCase]) extends Expr with ScalacPositional {
     def scrutineeClassType: ClassType = scrutinee.getType.asInstanceOf[ClassType]
   }
 
@@ -106,7 +106,7 @@ object Trees {
       if(and == null) None else Some(and.exprs)
   }
 
-  class And(val exprs: Seq[Expr]) extends Expr with FixedType {
+  @serializable class And(val exprs: Seq[Expr]) extends Expr with FixedType {
     val fixedType = BooleanType
   }
 
@@ -125,7 +125,7 @@ object Trees {
       if(or == null) None else Some(or.exprs)
   }
 
-  class Or(val exprs: Seq[Expr]) extends Expr with FixedType {
+  @serializable class Or(val exprs: Seq[Expr]) extends Expr with FixedType {
     val fixedType = BooleanType
   }
 
@@ -143,7 +143,7 @@ object Trees {
     }
   }
 
-  class Iff(val left: Expr, val right: Expr) extends Expr with FixedType {
+  @serializable class Iff(val left: Expr, val right: Expr) extends Expr with FixedType {
     val fixedType = BooleanType
   }
 
@@ -160,7 +160,7 @@ object Trees {
       if(imp == null) None else Some(imp.left, imp.right)
   }
 
-  class Implies(val left: Expr, val right: Expr) extends Expr with FixedType {
+  @serializable class Implies(val left: Expr, val right: Expr) extends Expr with FixedType {
     val fixedType = BooleanType
   }
 
@@ -192,7 +192,7 @@ object Trees {
     }
   }
 
-  class Equals(val left: Expr, val right: Expr) extends Expr with FixedType {
+  @serializable class Equals(val left: Expr, val right: Expr) extends Expr with FixedType {
     val fixedType = BooleanType
   }
   
diff --git a/src/purescala/TypeTrees.scala b/src/purescala/TypeTrees.scala
index 3441a0104be6f5cf410a287e9875a7c8b6fae574..da29f67f0ca7ddd79f17f3c6d6945cc3ff600cc3 100644
--- a/src/purescala/TypeTrees.scala
+++ b/src/purescala/TypeTrees.scala
@@ -31,7 +31,7 @@ object TypeTrees {
   }
     
 
-  sealed abstract class TypeTree {
+  @serializable sealed abstract class TypeTree {
     override def toString: String = PrettyPrinter(this)
   }
 
@@ -135,7 +135,7 @@ object TypeTrees {
   case class MapType(from: TypeTree, to: TypeTree) extends TypeTree
   case class OptionType(base: TypeTree) extends TypeTree
 
-  sealed abstract class ClassType extends TypeTree {
+  @serializable sealed abstract class ClassType extends TypeTree {
     val classDef: ClassTypeDef
     val id: Identifier = classDef.id
   }