diff --git a/project/build/funcheck.scala b/project/build/funcheck.scala
index d4b148c4f39b9f1f45e953ea30830ebea3f8d847..7c70f935db8222c3fda6e9ba3714c830606e55c1 100644
--- a/project/build/funcheck.scala
+++ b/project/build/funcheck.scala
@@ -30,20 +30,23 @@ class FunCheckProject(info: ProjectInfo) extends DefaultProject(info) with FileT
       val f = scriptPath.asFile
       val fw = new java.io.FileWriter(f)
       fw.write("#!/bin/bash" + nl)
-      fw.write("FUNCHECKCLASSPATH=")
+      fw.write("FUNCHECKCLASSPATH=\"")
       fw.write(buildLibraryJar.absolutePath + ":")
       fw.write(buildCompilerJar.absolutePath + ":")
       fw.write(purescala.jarPath.absolutePath + ":")
       fw.write(plugin.jarPath.absolutePath + ":")
       fw.write(("lib" / "z3.jar").absolutePath)
-      fw.write(nl + nl)
+      fw.write("\"" + nl + nl)
       fw.write("for f in " + extensionJars.map(_.absolutePath).map(n => "\"" + n + "\"").mkString(" ") + "; do" + nl)
       fw.write("  if [ -e ${f} ]" + nl)
       fw.write("  then" + nl)
       fw.write("    FUNCHECKCLASSPATH=${FUNCHECKCLASSPATH}:${f}" + nl)
       fw.write("  fi" + nl)
       fw.write("done" + nl + nl)
-      fw.write("SCALACCLASSPATH=\"" + (multisetsLib.jarPath.absolutePath) + "\"" + nl)
+      fw.write("SCALACCLASSPATH=\"")
+      fw.write(multisetsLib.jarPath.absolutePath + ":")
+      fw.write(plugin.jarPath.absolutePath)
+      fw.write("\"" + nl + nl)
       fw.write("LD_LIBRARY_PATH=" + ("." / "lib-bin").absolutePath + " \\" + nl)
       fw.write("java \\" + nl)
 
diff --git a/src/funcheck/Annotations.scala b/src/funcheck/Annotations.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4d15717df74d8a3c14344beebf8b2e9388917e60
--- /dev/null
+++ b/src/funcheck/Annotations.scala
@@ -0,0 +1,5 @@
+package funcheck
+
+object Annotations {
+  class induct extends StaticAnnotation
+}
diff --git a/src/funcheck/CodeExtraction.scala b/src/funcheck/CodeExtraction.scala
index c6caa595e6f44ce2b888f3db449ca08397eafbaf..e996e7bf84e86217037a8929f929f2c42c206ed7 100644
--- a/src/funcheck/CodeExtraction.scala
+++ b/src/funcheck/CodeExtraction.scala
@@ -155,7 +155,16 @@ trait CodeExtraction extends Extractors {
         _ match {
           case ExMainFunctionDef() => ;
           case dd @ ExFunctionDef(n,p,t,b) => {
-            defsToDefs += (dd.symbol -> extractFunSig(n, p, t))
+            val mods = dd.mods
+            val funDef = extractFunSig(n, p, t)
+            if(mods.isPrivate) funDef.addAnnotation("private")
+            for(a <- dd.symbol.annotations) {
+              a.atp.safeToString match {
+                case "funcheck.Annotations.induct" => funDef.addAnnotation("induct")
+                case _ => ;
+              }
+            }
+            defsToDefs += (dd.symbol -> funDef)
           }
           case _ => ;
         }
diff --git a/src/purescala/Definitions.scala b/src/purescala/Definitions.scala
index 67fe9fd5b185891e7598a40f4888f1a720a8c4cb..9eaebe171a86fcbbbb6b2d1438d3da15922ec4ad 100644
--- a/src/purescala/Definitions.scala
+++ b/src/purescala/Definitions.scala
@@ -232,6 +232,14 @@ object Definitions {
     def hasImplementation : Boolean = body.isDefined
     def hasPrecondition : Boolean = precondition.isDefined
     def hasPostcondition : Boolean = postcondition.isDefined
-  }
 
+    private var annots: Set[String] = Set.empty[String]
+    def addAnnotation(as: String*) : FunDef = {
+      annots = annots ++ as
+      this
+    }
+    def annotations : Set[String] = annots
+
+    def isPrivate : Boolean = annots.contains("private")
+  }
 }
diff --git a/src/purescala/PrettyPrinter.scala b/src/purescala/PrettyPrinter.scala
index 4b82075624e281e3b6b8718fdfade14b8928864d..c073757ce13a1a089a675e550204d1bafa1b215a 100644
--- a/src/purescala/PrettyPrinter.scala
+++ b/src/purescala/PrettyPrinter.scala
@@ -268,9 +268,14 @@ object PrettyPrinter {
         nsb
       }
 
-      case FunDef(id, rt, args, body, pre, post) => {
+      case fd @ FunDef(id, rt, args, body, pre, post) => {
         var nsb = sb
 
+        for(a <- fd.annotations) {
+          ind(nsb, lvl)
+          nsb.append("@" + a + "\n")
+        }
+
         pre.foreach(prec => {
           ind(nsb, lvl)
           nsb.append("@pre : ")
diff --git a/src/purescala/Z3ModelReconstruction.scala b/src/purescala/Z3ModelReconstruction.scala
new file mode 100644
index 0000000000000000000000000000000000000000..77688b2178aba5fe88be50fdf9f2c461aebeb12f
--- /dev/null
+++ b/src/purescala/Z3ModelReconstruction.scala
@@ -0,0 +1,14 @@
+package purescala
+
+import z3.scala._
+import Common._
+import Definitions._
+import Extensions._
+import Trees._
+import TypeTrees._
+
+trait Z3ModelReconstruction {
+  self: Z3Solver =>
+
+
+}
diff --git a/testcases/ListWithSize.scala b/testcases/ListWithSize.scala
index b9425d80402b61d9fc93f448cdd4b329ebbd3960..130955bc664c72a02963c83910b3a9262e873e00 100644
--- a/testcases/ListWithSize.scala
+++ b/testcases/ListWithSize.scala
@@ -1,4 +1,5 @@
 import scala.collection.immutable.Set
+import funcheck.Annotations._
 
 object ListWithSize {
     sealed abstract class List
@@ -34,9 +35,10 @@ object ListWithSize {
       case Cons(x,xs) => Cons(x, append(xs, l2))
     })
 
+    @induct
     def propAppend1(l : List) : Boolean = {
       append(l, Nil()) == l
-    }
+    } ensuring(_ == true)
 
     def propAppend2(l : List) : Boolean = (l match {
       case Nil() => propAppend1(l)