diff --git a/src/funcheck/Annotations.scala b/src/funcheck/Annotations.scala
index 4d15717df74d8a3c14344beebf8b2e9388917e60..c90e43247bb89039571373cf7d3321f808a16c2d 100644
--- a/src/funcheck/Annotations.scala
+++ b/src/funcheck/Annotations.scala
@@ -2,4 +2,5 @@ package funcheck
 
 object Annotations {
   class induct extends StaticAnnotation
+  class axiomatize extends StaticAnnotation
 }
diff --git a/src/funcheck/CodeExtraction.scala b/src/funcheck/CodeExtraction.scala
index 1cfa5229cb180d7ba3ee627ef229c54098f8d1ba..e86f1938e428d725d4771fa992859cf40bfe5d6c 100644
--- a/src/funcheck/CodeExtraction.scala
+++ b/src/funcheck/CodeExtraction.scala
@@ -179,6 +179,7 @@ trait CodeExtraction extends Extractors {
             for(a <- dd.symbol.annotations) {
               a.atp.safeToString match {
                 case "funcheck.Annotations.induct" => funDef.addAnnotation("induct")
+                case "funcheck.Annotations.axiomatize" => funDef.addAnnotation("axiomatize")
                 case _ => ;
               }
             }
diff --git a/src/purescala/FairZ3Solver.scala b/src/purescala/FairZ3Solver.scala
index 37d8d2f36d026844e36300d4e247ee64f827f96e..e31e1c41f5b4ac129d7f8035937ceb3b1baa83d4 100644
--- a/src/purescala/FairZ3Solver.scala
+++ b/src/purescala/FairZ3Solver.scala
@@ -202,6 +202,12 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
     if(!Settings.noForallAxioms) {
       prepareAxioms
     }
+
+    for(funDef <- program.definedFunctions) {
+      if (funDef.annotations.contains("axiomatize") && !axiomatizedFunctions(funDef)) {
+        reporter.warning("Function " + funDef.id + " was marked for axiomatization but could not be handled.")
+      }
+    }
   }
 
   private def prepareAxioms : Unit = {
@@ -228,9 +234,9 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
             val nameTypePairs = z3ArgSorts.map(s => (z3.mkFreshIntSymbol, s))
             z3.mkForAll(0, List(pattern), nameTypePairs, z3IzedEq)
           }
-          //println("I'll assert now an axiom: " + axiom)
-          //println("Case axiom:")
-          //println(axiom)
+          // println("I'll assert now an axiom: " + axiom)
+          // println("Case axiom:")
+          // println(axiom)
           z3.assertCnstr(axiom)
         }
 
@@ -392,7 +398,7 @@ class FairZ3Solver(val reporter: Reporter) extends Solver(reporter) with Abstrac
 
       reporter.info(" - Running Z3 search...")
       val (answer, model, core) : (Option[Boolean], Z3Model, Seq[Z3AST]) = if(Settings.useCores) {
-        println(blockingSetAsZ3)
+        // println(blockingSetAsZ3)
         z3.checkAssumptions(blockingSetAsZ3 : _*)
       } else {
         z3SearchStopwatch.start
diff --git a/testcases/Test.scala b/testcases/Test.scala
index b4a5fed825e2575796ddc9d3799d4aa43e43e63a..aab09c42df3788dc36ed760fb7983eecb9f6dec8 100644
--- a/testcases/Test.scala
+++ b/testcases/Test.scala
@@ -1,27 +1,32 @@
 import funcheck.Utils._
+import funcheck.Annotations._
 
 object Test {
-  sealed abstract class List
-  case class Cons(head: Int, tail: List) extends List
-  case class Nil() extends List
+    sealed abstract class List
+    case class Cons(head: Int, tail: List) extends List
+    case class Nil() extends List
 
-  def append(value: Int, list: List) : List = list match {
-    case Nil() => Cons(value, Nil())
-    case Cons(x, xs) => Cons(x, append(value, xs))
-  }
+    @axiomatize
+    def size(l: List) : Int = (l match {
+        case Nil() => 0
+        case Cons(_, t) => 1 + size(t)
+    }) ensuring(res => res >= 0)
 
-  def isSorted(list: List) : Boolean = list match {
-    case Nil() => true
-    case Cons(x, Nil()) => true
-    case Cons(x, c @ Cons(y, ys)) => x <= y && isSorted(c)
-  }
+    @axiomatize
+    def isSorted(l : List) : Boolean = l match {
+      case Nil() => true
+      case Cons(x, xs) => xs match {
+        case Nil() => true
+        case Cons(y, _) => x <= y && isSorted(xs)
+      }
+    }
 
-  def isSorted2(list: List) : Boolean = list match {
-    case Cons(x, c @ Cons(y, ys)) => x <= y && isSorted2(c)
-    case _ => true
-  }
+    def valuesWithin(l: List, lower: Int, upper: Int) : Boolean = l match {
+      case Nil() => true
+      case Cons(x, xs) => x >= lower && x <= upper && valuesWithin(xs, lower, upper)
+    }
 
-  def sameSorted(list: List) : Boolean = {
-    isSorted(list) == isSorted2(list)
-  } holds
+    def findOne(l : List) : Boolean = {
+      isSorted(l) && valuesWithin(l, 0, 3) && size(l) == 3
+    } ensuring(res => !res)
 }