diff --git a/lib/z3.jar b/lib/z3.jar
index 2405ab3028d98f39108e0c1e4a21aadb5b195138..ecba23f0612945a40e960b6f83fc97f7fa87cd8a 100644
Binary files a/lib/z3.jar and b/lib/z3.jar differ
diff --git a/src/purescala/Definitions.scala b/src/purescala/Definitions.scala
index 9eaebe171a86fcbbbb6b2d1438d3da15922ec4ad..6f1dcfef95ba104b06fda0ea04fc2822e2576340 100644
--- a/src/purescala/Definitions.scala
+++ b/src/purescala/Definitions.scala
@@ -230,6 +230,7 @@ object Definitions {
     var postcondition: Option[Expr] = None
 
     def hasImplementation : Boolean = body.isDefined
+    def hasBody = hasImplementation
     def hasPrecondition : Boolean = precondition.isDefined
     def hasPostcondition : Boolean = postcondition.isDefined
 
diff --git a/src/purescala/Z3Solver.scala b/src/purescala/Z3Solver.scala
index cf9054da619cc5914043743132086cccb98cc9d1..d372a45d08f9173e3558df90ebd1a4c3b22fa61f 100644
--- a/src/purescala/Z3Solver.scala
+++ b/src/purescala/Z3Solver.scala
@@ -593,6 +593,15 @@ class Z3Solver(val reporter: Reporter) extends Solver(reporter) with Z3ModelReco
       case Z3NumeralAST(Some(v)) => IntLiteral(v)
       case other @ _ => {
         println("Don't know what this is " + other) 
+        if(useInstantiator) {
+          instantiator.dumpFunctionMap
+        } else {
+          println("REVERSE FUNCTION MAP:")
+          println(reverseFunctionMap.toSeq.mkString("\n"))
+        }
+        println("REVERSE CONS MAP:")
+        println(reverseADTConstructors.toSeq.mkString("\n"))
+        System.exit(-1)
         throw new CantTranslateException(t)
       }
     }
diff --git a/src/purescala/z3plugins/instantiator/Instantiator.scala b/src/purescala/z3plugins/instantiator/Instantiator.scala
index 6e6347d7e8f5c1d923d617527e7acadbe0bd1996..2eecf5e8724fb96c664c19d211434042055e3e09 100644
--- a/src/purescala/z3plugins/instantiator/Instantiator.scala
+++ b/src/purescala/z3plugins/instantiator/Instantiator.scala
@@ -6,6 +6,7 @@ import purescala.Common._
 import purescala.Trees._
 import purescala.TypeTrees._
 import purescala.Definitions._
+import purescala.Settings
 
 import purescala.Z3Solver
 
@@ -37,6 +38,10 @@ class Instantiator(val z3Solver: Z3Solver) extends Z3Theory(z3Solver.z3, "Instan
     reverseFunctionMap = reverseFunctionMap + (z3Decl -> funDef)
   }
 
+  def dumpFunctionMap : Unit = {
+    println("REVERSE FUNCTION MAP:")
+    println(reverseFunctionMap.toSeq.mkString("\n"))
+  }
   def isKnownDef(funDef: FunDef) : Boolean = functionMap.isDefinedAt(funDef)
   def functionDefToDecl(funDef: FunDef) : Z3FuncDecl = {
     functionMap.getOrElse(funDef, scala.Predef.error("No Z3 definition found for function symbol "+ funDef.id.name + " in Instantiator."))
@@ -54,6 +59,7 @@ class Instantiator(val z3Solver: Z3Solver) extends Z3Theory(z3Solver.z3, "Instan
 
   }
 
+  private var bodyInlined : Int = 0
   override def newRelevant(ast: Z3AST) : Unit = {
     val aps = fromZ3Formula(ast)
     val fis = functionCallsOf(aps)
@@ -75,6 +81,17 @@ class Instantiator(val z3Solver: Z3Solver) extends Z3Theory(z3Solver.z3, "Instan
         println("As Z3: " + newAxiom)
         assertAxiom(newAxiom)
       }
+
+      if(bodyInlined < Settings.unrollingLevel && fd.hasBody) {
+        bodyInlined += 1
+        val body = matchToIfThenElse(fd.body.get)
+        val substMap = Map[Expr,Expr]((fd.args.map(_.toVariable) zip args) : _*)
+        val newBody = replace(substMap, body)
+        println("I'm going to add this : " + newBody)
+        val newAxiom = z3.mkEq(toZ3Formula(z3, fi).get, toZ3Formula(z3, newBody).get)
+        println("As Z3: " + newAxiom)
+        assertAxiom(newAxiom)
+      }
     }
   }