diff --git a/library/instrumentation/package.scala b/library/instrumentation/package.scala
index dc8ee71b..17d69ebd 100644
--- a/library/instrumentation/package.scala
+++ b/library/instrumentation/package.scala
@@ -21,4 +21,7 @@ package object instrumentation {
 
   @library
   def tpr: BigInt = 0
+
+  @library
+  def alloc: BigInt = 0
 }
diff --git a/src/main/scala/leon/transformations/AllocInstPhase.scala b/src/main/scala/leon/transformations/AllocInstPhase.scala
new file mode 100644
index 00000000..f0366eb4
--- /dev/null
+++ b/src/main/scala/leon/transformations/AllocInstPhase.scala
@@ -0,0 +1,60 @@
+/* Copyright 2009-2016 EPFL, Lausanne */
+
+package leon
+package transformations
+
+import purescala.Common._
+import purescala.Definitions._
+import purescala.Extractors._
+import purescala.Expressions._
+import purescala.ExprOps._
+import purescala.Types._
+import leon.utils._
+import invariant.util.Util._
+
+object allocCostModel {
+  def costOf(e: Expr): Int = e match {
+  	case CaseClass(_, _) => 1
+    case t: Terminal => 0
+    case _ => 0
+  }
+
+  def costOfExpr(e: Expr) = InfiniteIntegerLiteral(costOf(e))
+}
+
+class AllocInstrumenter(p: Program, si: SerialInstrumenter) extends Instrumenter(p, si) {
+  import allocCostModel._
+
+  def inst = Alloc
+
+  def functionsToInstrument(): Map[FunDef, List[Instrumentation]] = {
+    //find all functions transitively called from rootFuncs (here ignore functions called via pre/post conditions)
+    val instFunSet = getRootFuncs().foldLeft(Set[FunDef]())((acc, fd) => acc ++ cg.transitiveCallees(fd)).filter(_.hasBody) // ignore uninterpreted functions
+    //println("Root funs: "+getRootFuncs().map(_.id).mkString(",")+" All funcs: "+ instFunSet.map(_.id).mkString(","))
+    instFunSet.map(x => (x, List(Alloc))).toMap
+  }
+
+  def additionalfunctionsToAdd() = Seq()
+
+  def instrumentMatchCase(me: MatchExpr, mc: MatchCase,
+    caseExprCost: Expr, scrutineeCost: Expr): Expr = {
+    val costMatch = costOfExpr(me)
+    def totalCostOfMatchPatterns(me: MatchExpr, mc: MatchCase): BigInt = 0
+    Plus(costMatch, Plus(caseExprCost, scrutineeCost))
+  }
+
+  def instrument(e: Expr, subInsts: Seq[Expr], funInvResVar: Option[Variable] = None)
+  	(implicit fd: FunDef, letIdMap: Map[Identifier,Identifier]): Expr = e match {
+    case t: Terminal => costOfExpr(t)
+    case _ =>
+      subInsts.foldLeft(costOfExpr(e) : Expr)(
+        (acc: Expr, subeObjAlloc: Expr) => Plus(subeObjAlloc, acc))
+  }
+
+  def instrumentIfThenElseExpr(e: IfExpr, condInst: Option[Expr],
+      thenInst: Option[Expr], elzeInst: Option[Expr]): (Expr, Expr) = {    
+  	val costIf = costOfExpr(e)
+    (Plus(costIf, Plus(condInst.get, thenInst.get)),
+      Plus(costIf, Plus(condInst.get, elzeInst.get)))
+  }
+}
diff --git a/src/main/scala/leon/transformations/InstrumentationUtil.scala b/src/main/scala/leon/transformations/InstrumentationUtil.scala
index 5c26b194..9dafd60e 100644
--- a/src/main/scala/leon/transformations/InstrumentationUtil.scala
+++ b/src/main/scala/leon/transformations/InstrumentationUtil.scala
@@ -54,11 +54,16 @@ object Stack extends Instrumentation {
   override val getType = IntegerType
   override val name = "stack"
 }
+
+object Alloc extends Instrumentation {
+  override val getType = IntegerType
+  override val name = "alloc"
+}
 //add more instrumentation variables
 
 object InstUtil {
 
-  val InstTypes = Seq(Time, Depth, Rec, TPR, Stack)
+  val InstTypes = Seq(Time, Depth, Rec, TPR, Stack, Alloc)
 
   val maxFun = {
     val xid = FreshIdentifier("x", IntegerType)
diff --git a/src/main/scala/leon/transformations/SerialInstrumentationPhase.scala b/src/main/scala/leon/transformations/SerialInstrumentationPhase.scala
index c90325ec..4b04733c 100644
--- a/src/main/scala/leon/transformations/SerialInstrumentationPhase.scala
+++ b/src/main/scala/leon/transformations/SerialInstrumentationPhase.scala
@@ -46,7 +46,8 @@ class SerialInstrumenter(program: Program,
       Depth -> new DepthInstrumenter(program, this),
       Rec -> new RecursionCountInstrumenter(program, this),
       Stack -> new StackSpaceInstrumenter(program, this),
-      TPR -> new TPRInstrumenter(program, this))
+      TPR -> new TPRInstrumenter(program, this),
+      Alloc -> new AllocInstrumenter(program, this))
 
   // a map from functions to the list of instrumentations to be performed for the function
   val funcInsts = {
diff --git a/src/main/scala/leon/transformations/TimeStepsPhase.scala b/src/main/scala/leon/transformations/TimeStepsPhase.scala
index 5efb6f06..4e62182b 100644
--- a/src/main/scala/leon/transformations/TimeStepsPhase.scala
+++ b/src/main/scala/leon/transformations/TimeStepsPhase.scala
@@ -104,4 +104,4 @@ class TimeInstrumenter(p: Program, si: SerialInstrumenter) extends Instrumenter(
     (Plus(costIf, Plus(condInst.get, thenInst.get)),
       Plus(costIf, Plus(condInst.get, elzeInst.get)))
   }
-}
\ No newline at end of file
+}
diff --git a/testcases/orb-testcases/objAlloc/AmortizedQueue.scala b/testcases/orb-testcases/objAlloc/AmortizedQueue.scala
new file mode 100644
index 00000000..013c355e
--- /dev/null
+++ b/testcases/orb-testcases/objAlloc/AmortizedQueue.scala
@@ -0,0 +1,90 @@
+package orb
+
+import leon._
+import invariant._
+import instrumentation._
+
+object AmortizedQueue {
+  sealed abstract class List {
+    val size: BigInt = this match {
+      case Nil()       => 0
+      case Cons(_, xs) => 1 + xs.size
+    }
+  }
+  case class Cons(head: BigInt, tail: List) extends List
+  case class Nil() extends List
+
+  def length(l: List): BigInt = {
+    l match {
+      case Nil()       => BigInt(0)
+      case Cons(_, xs) => 1 + length(xs)
+    }
+  } ensuring(res => res >= 0 && alloc <= ?)
+
+  def concat(l1: List, l2: List): List = (l1 match {
+    case Nil()       => l2
+    case Cons(x, xs) => Cons(x, concat(xs, l2))
+
+  }) ensuring (res => res.size == l1.size + l2.size && alloc <= ? * l1.size + ?)
+
+  def reverseRec(l1: List, l2: List): List = (l1 match {
+    case Nil()       => l2
+    case Cons(x, xs) => reverseRec(xs, Cons(x, l2))
+  }) ensuring (res => l1.size + l2.size == res.size && alloc <= ? * l1.size + ?)
+
+  def listRev(l: List): List = {
+    reverseRec(l, Nil())
+  } ensuring (res => l.size == res.size && alloc <= ? * l.size + ?)
+
+  def removeLast(l: List): List = {
+    require(l != Nil())
+    l match {
+      case Cons(x, Nil()) => Nil()
+      case Cons(x, xs)    => Cons(x, removeLast(xs))
+      case _              => Nil()
+    }
+  } ensuring (res => res.size <= l.size && tmpl((a, b) => alloc <= a * l.size + b))
+
+  case class Queue(front: List, rear: List) {
+    def qsize: BigInt = front.size + rear.size
+
+    def asList: List = concat(front, listRev(rear))
+
+    def isAmortized: Boolean = length(front) >= length(rear)
+
+    def isEmpty: Boolean = this match {
+      case Queue(Nil(), Nil()) => true
+      case _                   => false
+    }
+
+    def amortizedQueue(front: List, rear: List): Queue = {
+      if (length(rear) <= length(front))
+        Queue(front, rear)
+      else
+        Queue(concat(front, listRev(rear)), Nil())
+    }
+
+    def enqueue(elem: BigInt): Queue = ({
+      amortizedQueue(front, Cons(elem, rear))
+    }) ensuring (_ => alloc <= ? * qsize + ?)
+
+    def dequeue: Queue = {
+      require(isAmortized && !isEmpty)
+      front match {
+        case Cons(f, fs) => amortizedQueue(fs, rear)
+        case _           => Queue(Nil(), Nil())
+      }
+    } ensuring (_ => alloc <= ? * qsize + ?)
+
+    def head: BigInt = {
+      require(isAmortized && !isEmpty)
+      front match {
+        case Cons(f, _) => f
+      }
+    }
+
+    def reverse: Queue = { // this lets the queue perform deque operation (but they no longer have efficient constant alloc amortized bounds)
+      amortizedQueue(rear, front)
+    }
+  }
+}
diff --git a/testcases/orb-testcases/objAlloc/BinaryTrie.scala b/testcases/orb-testcases/objAlloc/BinaryTrie.scala
new file mode 100644
index 00000000..41832713
--- /dev/null
+++ b/testcases/orb-testcases/objAlloc/BinaryTrie.scala
@@ -0,0 +1,119 @@
+import leon.invariant._
+import leon.instrumentation._
+
+object BinaryTrie {
+  sealed abstract class Tree
+  case class Leaf() extends Tree
+  case class Node(nvalue: BigInt, left: Tree, right: Tree) extends Tree
+
+  sealed abstract class IList
+  case class Cons(head: BigInt, tail: IList) extends IList
+  case class Nil() extends IList
+
+  def listSize(l: IList): BigInt = (l match {
+    case Nil() => 0
+    case Cons(x, xs) => 1 + listSize(xs)
+  })
+
+  def height(t: Tree): BigInt = {
+    t match {
+      case Leaf() => 0
+      case Node(x, l, r) => {
+        val hl = height(l)
+        val hr = height(r)
+        if (hl > hr) hl + 1 else hr + 1
+      }
+    }
+  }
+
+  def find(inp: IList, t: Tree): Tree = {
+    inp match {
+      case Nil() => t
+      case Cons(x, Nil()) => t
+      case Cons(x, xs @ Cons(y, _)) => {
+        t match {
+          case Leaf() => t
+          case Node(v, l, r) => {
+            if (y > 0) find(xs, l) else find(xs, r)
+          }
+        }
+      }
+      case _ => t
+    }
+  } ensuring (_ => alloc <= ? * listSize(inp) + ?)
+
+  def insert(inp: IList, t: Tree): Tree = {
+    t match {
+      case Leaf() => {
+        inp match {
+          case Nil() => t
+          case Cons(x, xs) => {
+            val newch = insert(xs, Leaf())
+            newch match {
+              case Leaf() => Node(x, Leaf(), Leaf())
+              case Node(y, _, _) => if (y > 0) Node(x, newch, Leaf()) else Node(y, Leaf(), newch)
+            }
+          }
+        }
+
+      }
+      case Node(v, l, r) => {
+        inp match {
+          case Nil() => t
+          case Cons(x, Nil()) => t
+          case Cons(x, xs @ Cons(y, _)) => {
+            val ch = if (y > 0) l else r
+            if (y > 0)
+              Node(v, insert(xs, ch), r)
+            else
+              Node(v, l, insert(xs, ch))
+          }
+          case _ => t
+        }
+      }
+    }
+  } ensuring (_ => alloc <= ? * listSize(inp) + ?)
+
+  def create(inp: IList): Tree = {
+    insert(inp, Leaf())
+  } ensuring (res => true && tmpl((a, c) => alloc <= a * listSize(inp) + c))
+
+  def delete(inp: IList, t: Tree): Tree = {
+    t match {
+        case Leaf() => {
+          inp match {
+            case Nil() => Leaf()
+            case Cons(x ,xs) => {
+              //the input is not in the tree, so do nothing
+              Leaf()
+            }
+          }
+        }
+        case Node(v, l, r) => {
+          inp match {
+            case Nil() => {
+              //the tree has extensions of the input list so do nothing
+              t
+            }
+            case Cons(x, Nil()) => {
+              //if "l" and "r" are nil, remove the node
+              if(l == Leaf() && r == Leaf()) Leaf()
+              else t
+            }
+            case Cons(x ,xs@Cons(y, _)) => {
+              val ch = if(y > 0) l else r
+              val newch = delete(xs, ch)
+              if(newch == Leaf() && ((y > 0 && r == Leaf()) || (y <= 0 && l == Leaf()))) Leaf()
+              else {
+                if(y > 0)
+        		  Node(v, newch, r)
+        	    else
+        	      Node(v, l, newch)
+              }
+            }
+            case _ => t
+        }
+      }
+    }
+  } ensuring (_ => alloc <= ? * listSize(inp) + ?)
+}
diff --git a/testcases/orb-testcases/objAlloc/BinomialHeap.scala b/testcases/orb-testcases/objAlloc/BinomialHeap.scala
new file mode 100644
index 00000000..7c668276
--- /dev/null
+++ b/testcases/orb-testcases/objAlloc/BinomialHeap.scala
@@ -0,0 +1,181 @@
+import leon.invariant._
+import leon.instrumentation._
+
+object BinomialHeap {
+  //sealed abstract class TreeNode
+  case class TreeNode(rank: BigInt, elem: Element, children: BinomialHeap)
+  case class Element(n: BigInt)
+
+  sealed abstract class BinomialHeap
+  case class ConsHeap(head: TreeNode, tail: BinomialHeap) extends BinomialHeap
+  case class NilHeap() extends BinomialHeap
+
+  sealed abstract class List
+  case class NodeL(head: BinomialHeap, tail: List) extends List
+  case class NilL() extends List
+
+  sealed abstract class OptionalTree
+  case class Some(t : TreeNode) extends OptionalTree
+  case class None() extends OptionalTree
+
+  /* Lower or Equal than for Element structure */
+  private def leq(a: Element, b: Element) : Boolean = {
+    a match {
+      case Element(a1) => {
+        b match {
+          case Element(a2) => {
+            if(a1 <= a2) true
+            else false
+          }
+        }
+      }
+    }
+  }
+
+  /* isEmpty function of the Binomial Heap */
+  def isEmpty(t: BinomialHeap) = t match {
+    case ConsHeap(_,_) => false
+    case _ => true
+  }
+
+  /* Helper function to determine rank of a TreeNode */
+  def rank(t: TreeNode) : BigInt = t.rank /*t match {
+    case TreeNode(r, _, _) => r
+  }*/
+
+  /* Helper function to get the root element of a TreeNode */
+  def root(t: TreeNode) : Element = t.elem /*t match {
+    case TreeNode(_, e, _) => e
+  }*/
+
+  /* Linking trees of equal ranks depending on the root element */
+  def link(t1: TreeNode, t2: TreeNode): TreeNode = {
+    if (leq(t1.elem, t2.elem)) {
+      TreeNode(t1.rank + 1, t1.elem, ConsHeap(t2, t1.children))
+    } else {
+      TreeNode(t1.rank + 1, t2.elem, ConsHeap(t1, t2.children))
+    }
+  }
+
+  def treeNum(h: BinomialHeap) : BigInt = {
+    h match {
+      case ConsHeap(head, tail) =>  1 + treeNum(tail)
+      case _ => 0
+    }
+  }
+
+  /* Insert a tree into a binomial heap. The tree should be correct in relation to the heap */
+  def insTree(t: TreeNode, h: BinomialHeap) : BinomialHeap = {
+    h match {
+      case ConsHeap(head, tail) =>  {
+        if (rank(t) < rank(head)) {
+          ConsHeap(t, h)
+        } else if (rank(t) > rank(head)) {
+          ConsHeap(head, insTree(t,tail))
+        } else {
+          insTree(link(t,head), tail)
+        }
+      }
+      case _ => ConsHeap(t, NilHeap())
+    }
+  } ensuring(_ => alloc <= ? * treeNum(h) + ?)
+
+  /* Merge two heaps together */
+  def merge(h1: BinomialHeap, h2: BinomialHeap): BinomialHeap = {
+    h1 match {
+      case ConsHeap(head1, tail1) => {
+        h2 match {
+          case ConsHeap(head2, tail2) => {
+            if (rank(head1) < rank(head2)) {
+              ConsHeap(head1, merge(tail1, h2))
+            } else if (rank(head2) < rank(head1)) {
+              ConsHeap(head2, merge(h1, tail2))
+            } else {
+              mergeWithCarry(link(head1, head2), tail1, tail2)
+            }
+          }
+          case _ => h1
+        }
+      }
+      case _ => h2
+    }
+  } ensuring(_ => alloc <= ? * treeNum(h1) + ? * treeNum(h2) + ?)
+
+  def mergeWithCarry(t: TreeNode, h1: BinomialHeap, h2: BinomialHeap): BinomialHeap = {
+    h1 match {
+      case ConsHeap(head1, tail1) => {
+        h2 match {
+          case ConsHeap(head2, tail2) => {
+            if (rank(head1) < rank(head2)) {
+
+              if (rank(t) < rank(head1))
+                ConsHeap(t, ConsHeap(head1, merge(tail1, h2)))
+              else
+                mergeWithCarry(link(t, head1), tail1, h2)
+
+            } else if (rank(head2) < rank(head1)) {
+
+              if (rank(t) < rank(head2))
+                ConsHeap(t, ConsHeap(head2, merge(h1, tail2)))
+              else
+                mergeWithCarry(link(t, head2), h1, tail2)
+
+            } else {
+              ConsHeap(t, mergeWithCarry(link(head1, head2), tail1, tail2))
+            }
+          }
+          case _ => {
+            insTree(t, h1)
+          }
+        }
+      }
+      case _ => insTree(t, h2)
+    }
+  } ensuring (_ => alloc <= ? * treeNum(h1) + ? * treeNum(h2) + ?)
+
+  //Auxiliary helper function to simplefy findMin and deleteMin
+  def removeMinTree(h: BinomialHeap): (OptionalTree, BinomialHeap) = {
+    h match {
+      case ConsHeap(head, NilHeap()) => (Some(head), NilHeap())
+      case ConsHeap(head1, tail1) => {
+        val (opthead2, tail2) = removeMinTree(tail1)
+        opthead2 match {
+          case Some(head2) =>
+            if (leq(root(head1), root(head2))) {
+              (Some(head1), tail1)
+            } else {
+              (Some(head2), ConsHeap(head1, tail2))
+            }
+          case _ => (Some(head1), tail1)
+        }
+      }
+      case _ => (None(), NilHeap())
+    }
+  } ensuring (res => treeNum(res._2) <= treeNum(h) && alloc <= ? * treeNum(h) + ?)
+
+  def findMin(h: BinomialHeap) : Element = {
+	  val (opt, _) = removeMinTree(h)
+	  opt match {
+	    case Some(TreeNode(_,e,ts1)) => e
+	    case _ => Element(-1)
+	  }
+  } ensuring(res => true && tmpl((a,b) => alloc <= a*treeNum(h) + b))
+
+  def minTreeChildren(h: BinomialHeap) : BigInt = {
+    val (min, _) = removeMinTree(h)
+    min match {
+      case Some(TreeNode(_,_,ch)) => treeNum(ch)
+      case _ => 0
+    }
+  }
+
+  // Discard the minimum element of the extracted min tree and put its children back into the heap
+  def deleteMin(h: BinomialHeap) : BinomialHeap = {
+    val (min, ts2) = removeMinTree(h)
+    min match {
+      case Some(TreeNode(_,_,ts1)) => merge(ts1, ts2)
+      case _ => h
+    }
+  } ensuring(_ => alloc <= ? * minTreeChildren(h) + ? * treeNum(h) + ?)
+
+}
diff --git a/testcases/orb-testcases/objAlloc/InsertionSort.scala b/testcases/orb-testcases/objAlloc/InsertionSort.scala
new file mode 100644
index 00000000..3f5f84d4
--- /dev/null
+++ b/testcases/orb-testcases/objAlloc/InsertionSort.scala
@@ -0,0 +1,28 @@
+import leon.invariant._
+import leon.instrumentation._
+
+object InsertionSort {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail:List) extends List
+  case class Nil() extends List
+
+  def size(l : List): BigInt = {
+    l match {
+      case Cons(_, xs) => 1 + size(xs)
+      case _ => BigInt(0)
+    }
+  } ensuring(res => res >= 0 && alloc <= ?)
+
+  def sortedIns(e: BigInt, l: List): List = {
+    l match {
+      case Cons(x,xs) => if (x < e) Cons(x,sortedIns(e, xs)) else Cons(e, l)
+      case _ => Cons(e,Nil())
+    }
+  } ensuring(res => size(res) == size(l) + 1 && alloc <= ? * size(res) + ?)
+
+    def sort(l: List): List = (l match {
+      case Cons(x,xs) => sortedIns(x, sort(xs))
+      case _ => Nil()
+    }) ensuring(res => size(res) == size(l) && alloc <= ? *(size(res) * size(res)) + ? * size(res) + ?)
+}
+
diff --git a/testcases/orb-testcases/objAlloc/ListOperations.scala b/testcases/orb-testcases/objAlloc/ListOperations.scala
new file mode 100644
index 00000000..96985076
--- /dev/null
+++ b/testcases/orb-testcases/objAlloc/ListOperations.scala
@@ -0,0 +1,60 @@
+import leon.invariant._
+import leon.instrumentation._
+
+object ListOperations {
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case class Nil() extends List
+
+  def size(l: List): BigInt = (l match {
+    case Nil() => 0
+    case Cons(_, t) => 1 + size(t)
+  })
+
+  def append(l1: List, l2: List): List = (l1 match {
+    case Nil() => l2
+    case Cons(x, xs) => Cons(x, append(xs, l2))
+
+  }) ensuring (res =>  size(l1) + size(l2) == size(res) && tmpl((a,b) => alloc <= a*size(l1) + b))
+
+  def reverseRec(l1: List, l2: List): List = (l1 match {
+    case Nil() => l2
+    case Cons(x, xs) => reverseRec(xs, Cons(x, l2))
+
+  }) ensuring (res =>  size(l1) + size(l2) == size(res) && tmpl((a,b) => alloc <= a*size(l1) + b))
+
+  def reverse(l: List): List = {
+    reverseRec(l, Nil())
+
+  } ensuring (res => size(l) == size(res) && tmpl((a,b) => alloc <= a*size(l) + b))
+
+  def reverse2(l: List): List = {
+    l match {
+      case Nil() => l
+      case Cons(hd, tl) => append(reverse2(tl), Cons(hd, Nil()))
+    }
+  } ensuring (res => size(res) == size(l) && tmpl((a,b) => alloc <= a*(size(l)*size(l)) + b))
+
+  def remove(elem: BigInt, l: List): List = {
+    l match {
+      case Nil() => Nil()
+      case Cons(hd, tl) => if (hd == elem) remove(elem, tl) else Cons(hd, remove(elem, tl))
+    }
+  } ensuring (res => size(l) >= size(res) && tmpl((a,b) => alloc <= a*size(l) + b))
+
+  def contains(list: List, elem: BigInt): Boolean = (list match {
+    case Nil() => false
+    case Cons(x, xs) => x == elem || contains(xs, elem)
+
+  }) ensuring (res => true && tmpl((a,b) => alloc <= a*size(list) + b))
+
+  def distinct(l: List): List = (
+    l match {
+      case Nil() => Nil()
+      case Cons(x, xs) => {
+        val newl = distinct(xs)
+        if (contains(newl, x)) newl
+        else Cons(x, newl)
+      }
+   }) ensuring (res => size(l) >= size(res) && tmpl((a,b) => alloc <= a*(size(l)*size(l)) + b))
+}
diff --git a/testcases/orb-testcases/objAlloc/PropositionLogic.scala b/testcases/orb-testcases/objAlloc/PropositionLogic.scala
new file mode 100644
index 00000000..6bd66e16
--- /dev/null
+++ b/testcases/orb-testcases/objAlloc/PropositionLogic.scala
@@ -0,0 +1,115 @@
+import scala.collection.immutable.Set
+import leon.invariant._
+import leon.instrumentation._
+
+object PropositionalLogic {
+
+  sealed abstract class Formula
+  case class And(lhs: Formula, rhs: Formula) extends Formula
+  case class Or(lhs: Formula, rhs: Formula) extends Formula
+  case class Implies(lhs: Formula, rhs: Formula) extends Formula
+  case class Not(f: Formula) extends Formula
+  case class Literal(id: BigInt) extends Formula
+  case class True() extends Formula
+  case class False() extends Formula
+
+  case class Pair(f: Formula, b: Boolean)
+
+  sealed abstract class List
+  case class Cons(x: Pair, xs: List) extends List
+  case class Nil() extends List
+
+  def size(f : Formula) : BigInt = (f match {
+    case And(lhs, rhs) => size(lhs) + size(rhs) + 1
+    case Or(lhs, rhs) => size(lhs) + size(rhs) + 1
+    case Implies(lhs, rhs) => size(lhs) + size(rhs) + 1
+    case Not(f) => size(f) + 1
+    case _ => 1
+  })
+
+  def removeImplies(f: Formula): Formula = (f match {
+    case And(lhs, rhs) => And(removeImplies(lhs), removeImplies(rhs))
+    case Or(lhs, rhs) => Or(removeImplies(lhs), removeImplies(rhs))
+    case Implies(lhs, rhs) => Or(Not(removeImplies(lhs)),removeImplies(rhs))
+    case Not(f) => Not(removeImplies(f))
+    case _ => f
+
+  }) ensuring(_ => alloc <= ? * size(f) + ?)
+
+  def nnf(formula: Formula): Formula = (formula match {
+    case And(lhs, rhs) => And(nnf(lhs), nnf(rhs))
+    case Or(lhs, rhs) => Or(nnf(lhs), nnf(rhs))
+    case Implies(lhs, rhs) => Implies(nnf(lhs), nnf(rhs))
+    case Not(And(lhs, rhs)) => Or(nnf(Not(lhs)), nnf(Not(rhs)))
+    case Not(Or(lhs, rhs)) => And(nnf(Not(lhs)), nnf(Not(rhs)))
+    case Not(Implies(lhs, rhs)) => And(nnf(lhs), nnf(Not(rhs)))
+    case Not(Not(f)) => nnf(f)
+    case Not(Literal(_)) => formula
+    case Literal(_) => formula
+    case Not(True()) => False()
+    case Not(False()) => True()
+    case _ => formula
+  }) ensuring(_ => alloc <= ? * size(formula) + ?)
+
+  def isNNF(f: Formula): Boolean = { f match {
+    case And(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
+    case Or(lhs, rhs) => isNNF(lhs) && isNNF(rhs)
+    case Implies(lhs, rhs) => false
+    case Not(Literal(_)) => true
+    case Not(_) => false
+    case _ => true
+  }} ensuring(_ => alloc <= ? * size(f) + ?)
+
+  def simplify(f: Formula): Formula = (f match {
+    case And(lhs, rhs) => {
+      val sl = simplify(lhs)
+      val sr = simplify(rhs)
+
+      //if lhs or rhs is false, return false
+      //if lhs is true return rhs
+      //if rhs is true return lhs
+      (sl,sr) match {
+        case (False(), _) => False()
+        case (_, False()) => False()
+        case (True(), _) => sr
+        case (_, True()) => sl
+        case _ => And(sl, sr)
+      }
+    }
+    case Or(lhs, rhs) => {
+      val sl = simplify(lhs)
+      val sr = simplify(rhs)
+
+      //if lhs or rhs is true, return true
+      //if lhs is false return rhs
+      //if rhs is false return lhs
+      (sl,sr) match {
+        case (True(), _) => True()
+        case (_, True()) => True()
+        case (False(), _) => sr
+        case (_, False()) => sl
+        case _ => Or(sl, sr)
+      }
+    }
+    case Implies(lhs, rhs) => {
+      val sl = simplify(lhs)
+      val sr = simplify(rhs)
+
+      //if lhs is false return true
+      //if rhs is true return true
+      //if lhs is true return rhs
+      //if rhs is false return Not(rhs)
+      (sl,sr) match {
+        case (False(), _) => True()
+        case (_, True()) => True()
+        case (True(), _) => sr
+        case (_, False()) => Not(sl)
+        case _ => Implies(sl, sr)
+      }
+    }
+    case Not(True()) => False()
+    case Not(False()) => True()
+    case _ => f
+
+  }) ensuring(_ => alloc <= ? *size(f) + ?)
+}
diff --git a/testcases/orb-testcases/objAlloc/QuickSort.scala b/testcases/orb-testcases/objAlloc/QuickSort.scala
new file mode 100644
index 00000000..291fbd16
--- /dev/null
+++ b/testcases/orb-testcases/objAlloc/QuickSort.scala
@@ -0,0 +1,43 @@
+import leon.invariant._
+import leon.instrumentation._
+
+object QuickSort {
+  sealed abstract class List
+  case class Cons(head:BigInt,tail:List) extends List
+  case class Nil() extends List
+
+  def size(l:List): BigInt = {l match {
+    case Nil() => 0
+    case Cons(x,xs) => 1 + size(xs)
+  }}
+
+  case class Triple(fst:List,snd:List, trd: List)
+
+  def append(aList:List,bList:List): List = {aList match {
+    case Nil() => bList
+    case Cons(x, xs) => Cons(x,append(xs,bList))
+  }} ensuring(res => size(res) == size(aList) + size(bList) && alloc <= ? * (size(aList) + size(bList)) + ?)
+
+  def partition(n:BigInt,l:List) : Triple = (l match {
+    case Nil() => Triple(Nil(), Nil(), Nil())
+    case Cons(x,xs) => {
+      val t = partition(n,xs)
+      if (n < x) Triple(t.fst, t.snd, Cons(x,t.trd))
+      else if(n == x) Triple(t.fst, Cons(x,t.snd), t.trd)
+      else Triple(Cons(x,t.fst), t.snd, t.trd)
+    }
+  }) ensuring(res => (size(l) == size(res.fst) + size(res.snd) + size(res.trd)) && alloc <= ? * (size(l)) + ?)
+
+  // alloc bound doesn't work too :-(
+  def quickSort(l:List): List = (l match {
+    case Nil() => Nil()
+    case Cons(x,Nil()) => l
+    case Cons(x,xs) => {
+      val t = partition(x, xs)
+      append(append(quickSort(t.fst), Cons(x, t.snd)), quickSort(t.trd))
+    }
+    case _ => l
+  }) ensuring(res => size(l) == size(res))
+  // ensuring(res => size(l) == size(res) && alloc <= ? *(size(res)*size(res)) + ? * size(res) + ?)
+}
+
diff --git a/testcases/orb-testcases/objAlloc/RedBlackTree.scala b/testcases/orb-testcases/objAlloc/RedBlackTree.scala
new file mode 100644
index 00000000..0e119081
--- /dev/null
+++ b/testcases/orb-testcases/objAlloc/RedBlackTree.scala
@@ -0,0 +1,112 @@
+import leon.invariant._
+import leon.instrumentation._
+import scala.collection.immutable.Set
+
+object RedBlackTree {
+  sealed abstract class Color
+  case class Red() extends Color
+  case class Black() extends Color
+
+  sealed abstract class Tree
+  case class Empty() extends Tree
+  case class Node(color: Color, left: Tree, value: BigInt, right: Tree) extends Tree
+
+  def twopower(x: BigInt) : BigInt = {
+    require(x >= 0)
+    if(x < 1) 1
+    else
+      2* twopower(x - 1)
+  }
+
+  def size(t: Tree): BigInt = {
+    require(blackBalanced(t))
+    (t match {
+      case Empty() => BigInt(0)
+      case Node(_, l, v, r) => size(l) + 1 + size(r)
+    })
+  } ensuring (res => tmpl((a,b) => twopower(blackHeight(t)) <= a*res + b))
+
+  def blackHeight(t : Tree) : BigInt = {
+    t match {
+      case Node(Black(), l, _, _) => blackHeight(l) + 1
+      case Node(Red(), l, _, _) => blackHeight(l)
+      case _ => 0
+    }
+  }
+
+  //We consider leaves to be black by definition
+  def isBlack(t: Tree) : Boolean = t match {
+    case Empty() => true
+    case Node(Black(),_,_,_) => true
+    case _ => false
+  }
+
+  def redNodesHaveBlackChildren(t: Tree) : Boolean = t match {
+    case Empty() => true
+    case Node(Black(), l, _, r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+    case Node(Red(), l, _, r) => isBlack(l) && isBlack(r) && redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+    case _ => false
+  }
+
+  def redDescHaveBlackChildren(t: Tree) : Boolean = t match {
+    case Node(_,l,_,r) => redNodesHaveBlackChildren(l) && redNodesHaveBlackChildren(r)
+    case _ => true
+  }
+
+  def blackBalanced(t : Tree) : Boolean = t match {
+    case Node(_,l,_,r) => blackBalanced(l) && blackBalanced(r) && blackHeight(l) == blackHeight(r)
+    case _ => true
+  }
+
+  // <<insert element x BigInto the tree t>>
+  def ins(x: BigInt, t: Tree): Tree = {
+    require(redNodesHaveBlackChildren(t) && blackBalanced(t))
+
+    t match {
+      case Empty() => Node(Red(),Empty(),x,Empty())
+      case Node(c,a,y,b) =>
+        if(x < y) {
+          val t1 = ins(x, a)
+          balance(c, t1, y, b)
+        }
+        else if (x == y){
+          Node(c,a,y,b)
+        }
+        else{
+          val t1 = ins(x, b)
+          balance(c,a,y,t1)
+        }
+    }
+  } ensuring(res => tmpl((a,b) => alloc <= a*blackHeight(t) + b))
+
+  def makeBlack(n: Tree): Tree = {
+    n match {
+      case Node(Red(),l,v,r) => Node(Black(),l,v,r)
+      case _ => n
+    }
+  }
+
+  def add(x: BigInt, t: Tree): Tree = {
+    require(redNodesHaveBlackChildren(t) && blackBalanced(t) )
+    val t1 =  ins(x, t)
+    makeBlack(t1)
+
+  } ensuring(res => tmpl((a,b) => alloc <= a*blackHeight(t) + b))
+
+  def balance(co: Color, l: Tree, x: BigInt, r: Tree): Tree = {
+    Node(co,l,x,r)
+    match {
+      case Node(Black(),Node(Red(),Node(Red(),a,xV,b),yV,c),zV,d) =>
+        Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+      case Node(Black(),Node(Red(),a,xV,Node(Red(),b,yV,c)),zV,d) =>
+        Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+      case Node(Black(),a,xV,Node(Red(),Node(Red(),b,yV,c),zV,d)) =>
+        Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+      case Node(Black(),a,xV,Node(Red(),b,yV,Node(Red(),c,zV,d))) =>
+        Node(Red(),Node(Black(),a,xV,b),yV,Node(Black(),c,zV,d))
+      case _ => Node(co,l,x,r)
+    }
+  }
+
+
+}
diff --git a/testcases/orb-testcases/objAlloc/TreeOperations.scala b/testcases/orb-testcases/objAlloc/TreeOperations.scala
new file mode 100644
index 00000000..1b6e5438
--- /dev/null
+++ b/testcases/orb-testcases/objAlloc/TreeOperations.scala
@@ -0,0 +1,93 @@
+import leon.invariant._
+import leon.instrumentation._
+
+
+object TreeOperations {
+
+  sealed abstract class List
+  case class Cons(head: BigInt, tail: List) extends List
+  case class Nil() extends List
+
+  sealed abstract class Tree
+  case class Node(left: Tree, value: BigInt, right: Tree) extends Tree
+  case class Leaf() extends Tree
+
+  def listSize(l: List): BigInt = (l match {
+    case Nil() => 0
+    case Cons(_, t) => 1 + listSize(t)
+  })
+
+  def size(t: Tree): BigInt = {
+    t match {
+      case Leaf() => 0
+      case Node(l, x, r) => {
+        size(l) + size(r) + 1
+      }
+    }
+  }
+
+  def height(t: Tree): BigInt = {
+    t match {
+      case Leaf() => 0
+      case Node(l, x, r) => {
+        val hl = height(l)
+        val hr = height(r)
+        if (hl > hr) hl + 1 else hr + 1
+      }
+    }
+  } 
+
+  def insert(elem: BigInt, t: Tree): Tree = {
+    t match {
+      case Leaf() => Node(Leaf(), elem, Leaf())
+      case Node(l, x, r) => if (x <= elem) Node(l, x, insert(elem, r))
+      else Node(insert(elem, l), x, r)
+    }
+  } ensuring (res => height(res) <= height(t) + 1 && tmpl((a,b) => alloc <= a*height(t) + b))
+
+  def addAll(l: List, t: Tree): Tree = {
+    l match {
+      case Nil() => t
+      case Cons(x, xs) =>{
+        val newt = insert(x, t)
+        addAll(xs, newt)
+      }
+    }
+  } ensuring(res => tmpl((a,b,c) => alloc <= a*(listSize(l) * (height(t) + listSize(l))) + b*listSize(l) + c))
+
+  def remove(elem: BigInt, t: Tree): Tree = {
+    t match {
+      case Leaf() => Leaf()
+      case Node(l, x, r) => {
+
+        if (x < elem) Node(l, x, remove(elem, r))
+        else if (x > elem) Node(remove(elem, l), x, r)
+        else {
+          t match {
+            case Node(Leaf(), x, Leaf()) => Leaf()
+            case Node(Leaf(), x, Node(_, rx, _)) => Node(Leaf(), rx, remove(rx, r))
+            case Node(Node(_, lx, _), x, r) => Node(remove(lx, l), lx, r)
+            case _ => Leaf()
+          }
+        }
+      }
+    }
+  } ensuring (res => height(res) <= height(t) && tmpl ((a, b, c) => alloc <= a*height(t) + b))
+
+  def removeAll(l: List, t: Tree): Tree = {
+    l match {
+      case Nil() => t
+      case Cons(x, xs) => removeAll(xs, remove(x, t))
+    }
+  } ensuring(res => tmpl((a,b,c) => alloc <= a*(listSize(l) * height(t)) + b*listSize(l) + c))
+
+  def contains(elem : BigInt, t : Tree) : Boolean = {
+    t match {
+      case Leaf() => false
+      case Node(l, x, r) =>
+        if(x == elem) true
+        else if (x < elem) contains(elem, r)
+        else contains(elem, l)
+    }
+  } ensuring (res => tmpl((a,b) => alloc <= a*height(t) + b))
+}
\ No newline at end of file