diff --git a/src/funcheck/CallTransformation.scala b/src/funcheck/CallTransformation.scala
index f3b95a54b0237633c96693f90df0300dddc6ada2..a2b0705a2d833922f1b3405c976fee246731fe82 100644
--- a/src/funcheck/CallTransformation.scala
+++ b/src/funcheck/CallTransformation.scala
@@ -38,9 +38,9 @@ trait CallTransformation
           fd.body match {
             case None => println("Could not extract choose predicate: " + funBody); super.transform(tree)
             case Some(b) =>
-              val (readProgram, progSym) = codeGen.generateProgramRead(filename)
+              val (programGet, progSym) = codeGen.generateProgramGet(filename)
               val solverInvocation = codeGen.generateSolverInvocation(b, progSym)
-              val code = Block(readProgram :: Nil, solverInvocation)
+              val code = Block(programGet :: Nil, solverInvocation)
 
               typer.typed(atOwner(currentOwner) {
                 code
diff --git a/src/funcheck/CodeGeneration.scala b/src/funcheck/CodeGeneration.scala
index 6850a1679fc928332028a14715f07b5efb2b2dac..c81a2d71b2a6d7a9cc94a25f8fc0170a1ef07433 100644
--- a/src/funcheck/CodeGeneration.scala
+++ b/src/funcheck/CodeGeneration.scala
@@ -7,7 +7,7 @@ trait CodeGeneration {
   import global._
 
   private lazy val serializationModule = definitions.getClass("funcheck.Serialization")
-  private lazy val readProgramFunction = definitions.getMember(serializationModule, "readProgram")
+  private lazy val getProgramFunction = definitions.getMember(serializationModule, "getProgram")
   private lazy val purescalaPackage = definitions.getModule("purescala")
   private lazy val definitionsModule = definitions.getModule("purescala.Definitions")
   private lazy val programClass = definitions.getClass("purescala.Definitions.Program")
@@ -18,26 +18,21 @@ trait CodeGeneration {
   private lazy val defaultReporter = definitions.getClass("purescala.DefaultReporter")
 
   class CodeGenerator(unit: CompilationUnit, owner: Symbol) {
-    /*
-    def exprToTree(expr: Expr) : Tree = expr match {
-      case Variable(id) => 
-    }
-    */
 
-    def generateProgramRead(filename: String) : (Tree, Symbol) = {
+    def generateProgramGet(filename: String) : (Tree, Symbol) = {
       val progSymbol = owner.newValue(NoPosition, unit.fresh.newName(NoPosition, "prog")).setInfo(programClass.tpe)
-      val readStatement =
+      val getStatement =
         ValDef(
           progSymbol,
           Apply(
             Select(
               Ident(serializationModule),
-              readProgramFunction
+              getProgramFunction
             ),
             List(Literal(Constant(filename)))
           )
         )
-      (readStatement, progSymbol)
+      (getStatement, progSymbol)
     }
 
     def generateSolverInvocation(formula: Expr, progSymbol: Symbol) : Tree = {
diff --git a/src/funcheck/Serialization.scala b/src/funcheck/Serialization.scala
index 12d08f4a874c91dac0c25f990b5efe282f52d5e1..addb7e24c08570d0c3fa76c67fa40a4cf0106aaa 100644
--- a/src/funcheck/Serialization.scala
+++ b/src/funcheck/Serialization.scala
@@ -1,41 +1,77 @@
 package funcheck
 
-import java.io.{FileInputStream,FileOutputStream,ObjectInputStream,ObjectOutputStream}
-import purescala.Definitions.Program
-
 trait Serialization {
-  val fileSuffix = ".serialized"
-  val dirName = "serialized"
+  import java.io.{FileInputStream,FileOutputStream,ObjectInputStream,ObjectOutputStream,File}
+  import purescala.Definitions._
+  import purescala.Trees._
 
-  def programFileName(prog : Program) : String = {
-    prog.mainObject.id.toString
-  }
+  private val fileSuffix = ""
+  private val dirName = "serialized"
+  private val directory = new java.io.File(dirName)
 
-  def writeProgram(prog : Program) : String = {
-    val directory = new java.io.File(dirName)
-    directory.mkdir()
+  private var cachedProgram : Option[Program] = None
+  private val exprMap = new scala.collection.mutable.HashMap[String,Expr]()
 
-    val file = java.io.File.createTempFile(programFileName(prog), fileSuffix, directory)
+  def programFileName(prog : Program) : String = {
+    prog.mainObject.id.toString + fileSuffix
+  }
 
+  private def writeObject(file : File, obj : Any) : String = {
     val fos = new FileOutputStream(file)
     val oos = new ObjectOutputStream(fos)
 
-    oos.writeObject(prog)
+    oos.writeObject(obj)
     oos.flush()
     fos.close()
 
     file.getAbsolutePath()
   }
+  def writeProgram(prog : Program) : String = {
+    directory.mkdir()
+
+    val file = new java.io.File(directory, programFileName(prog))
+    file.delete()
 
-  def readProgram(filename : String) : Program = {
+    writeObject(file, prog)
+  }
+
+  def writeExpr(pred : Expr) : String = {
+    directory.mkdir()
+
+    val file = java.io.File.createTempFile("expr", fileSuffix, directory)
+    
+    writeObject(file, pred)
+  }
+
+  private def readObject[A](filename : String) : A = {
     val fis = new FileInputStream(filename)
     val ois = new ObjectInputStream(fis)
 
-    val recovered : Program = ois.readObject().asInstanceOf[Program]
+    val recovered : A = ois.readObject().asInstanceOf[A]
     fis.close()
 
     recovered
   }
+
+  private def readProgram(filename : String) : Program = {
+    readObject[Program](filename)
+  }
+
+  private def readExpr(filename : String) : Expr = {
+    readObject[Expr](filename)
+  }
+
+  def getProgram(filename : String) : Program = cachedProgram match {
+    case None => val r = readProgram(filename); cachedProgram = Some(r); r
+    case Some(cp) => cp
+  }
+
+  def getExpr(filename : String) : Expr = exprMap.get(filename) match {
+    case Some(p) => p
+    case None => val p = readExpr(filename); exprMap += (filename -> p); p
+  }
 }
 
-object Serialization extends Serialization
+object Serialization extends Serialization {
+  
+}
diff --git a/src/purescala/FairZ3Solver.scala b/src/purescala/FairZ3Solver.scala
index 3fc21a5b0797394d29a09cbc5bcf779fcb69f6a4..6945611ad87be9b73a4f0f9b6c0bbc56df189336 100644
--- a/src/purescala/FairZ3Solver.scala
+++ b/src/purescala/FairZ3Solver.scala
@@ -11,7 +11,7 @@ import scala.collection.mutable.{Map => MutableMap}
 import scala.collection.mutable.{Set => MutableSet}
 
 class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with AbstractZ3Solver with Z3ModelReconstruction {
-  assert(Settings.useFairInstantiator)
+  // assert(Settings.useFairInstantiator)
 
   private final val UNKNOWNASSAT : Boolean = false