diff --git a/backend/cn/baseTypes.ml b/backend/cn/baseTypes.ml
index ecd27c4bf..8f0a1d321 100644
--- a/backend/cn/baseTypes.ml
+++ b/backend/cn/baseTypes.ml
@@ -5,6 +5,7 @@ type basetype =
   | Bool
   | Integer
   | Real
+  | Alloc_id
   | Loc
   | CType
   | Struct of Sym.t
@@ -47,6 +48,7 @@ let rec pp = function
   | Integer -> !^"integer"
   | Real -> !^"real"
   | Loc -> !^"pointer"
+  | Alloc_id -> !^"alloc_id"
   | CType -> !^"ctype"
   | Struct sym -> !^"struct" ^^^ Sym.pp sym
   | Datatype sym -> !^"datatype" ^^^ Sym.pp sym
@@ -117,11 +119,12 @@ let rec hash = function
   | Bool -> 1
   | Integer -> 2
   | Real -> 3
-  | Loc -> 4
-  | CType -> 5
-  | List _ -> 6
-  | Tuple _ -> 7
-  | Set _ -> 8
+  | Alloc_id -> 4
+  | Loc -> 5
+  | CType -> 6
+  | List _ -> 7
+  | Tuple _ -> 8
+  | Set _ -> 9
   (* | Option _ -> 8 *)
   | Struct tag -> 1000 + Sym.num tag
   | Datatype tag -> 4000 + Sym.num tag
diff --git a/backend/cn/context.ml b/backend/cn/context.ml
index 8d5a89d47..30b5327b2 100644
--- a/backend/cn/context.ml
+++ b/backend/cn/context.ml
@@ -48,9 +48,15 @@ type t = {
   }
 
 
-let empty = {
+let empty =
+  let alloc_id = Sym.fresh_named "__cn_alloc_history" in
+  let loc_str = __FILE__ ^ ":" ^ string_of_int __LINE__ in
+  let l_info = (Locations.other loc_str, lazy (Pp.string loc_str)) in
+  let bt = (BT.Map(Alloc_id, Record [(Id.id "base", Loc); (Id.id "len", Integer)])) in
+  let logical = SymMap.(empty |> add alloc_id (BaseType bt, l_info)) in
+  {
     computational = SymMap.empty;
-    logical = SymMap.empty;
+    logical;
     resources = ([], 0);
     resource_history = IntMap.empty;
     constraints = LCSet.empty;
diff --git a/backend/cn/solver.ml b/backend/cn/solver.ml
index da2d2923d..025e95b10 100644
--- a/backend/cn/solver.ml
+++ b/backend/cn/solver.ml
@@ -311,6 +311,11 @@ module Translate = struct
            (string (bt_name Loc))
            [string "loc_to_integer"] 
            [sort BT.Integer]
+      | Alloc_id ->
+         Z3.Tuple.mk_sort context
+           (string (bt_name Alloc_id))
+           [string "alloc_id_to_integer"]
+           [sort BT.Integer]
       | CType -> (* the ctype type is represented as an uninterpreted sort *)
         Z3.Sort.mk_uninterpreted_s context (bt_name CType)
       | List bt -> (* lists are represented as uninterpreted sorts *)
@@ -388,6 +393,9 @@ module Translate = struct
     Z3.Tuple.get_mk_decl (sort context global Loc)
   
 
+  let integer_to_alloc_id_fundecl context global =
+    Z3.Tuple.get_mk_decl (sort context global Alloc_id)
+
 
   let term ?(warn_lambda=true) context global : IT.t -> expr =
 
@@ -406,6 +414,10 @@ module Translate = struct
       Z3.Expr.mk_app context 
         (integer_to_loc_fundecl context global) [i] 
     in
+    let integer_to_alloc_id i =
+      Z3.Expr.mk_app context
+        (integer_to_alloc_id_fundecl context global) [i]
+    in
 
 
     let apply_matching_func sym_role fds args =
@@ -429,6 +441,9 @@ module Translate = struct
       | Const (Pointer z) -> 
          integer_to_loc
            (Z3.Arithmetic.Integer.mk_numeral_s context (Z.to_string z))
+      | Const (Alloc_id z) ->
+         integer_to_alloc_id
+           (Z3.Arithmetic.Integer.mk_numeral_s context (Z.to_string z))
       | Const (Bool true) -> 
          Z3.Boolean.mk_true context
       | Const (Bool false) -> 
diff --git a/backend/cn/surfaceBaseTypes.ml b/backend/cn/surfaceBaseTypes.ml
index 2568f294d..271b6483d 100644
--- a/backend/cn/surfaceBaseTypes.ml
+++ b/backend/cn/surfaceBaseTypes.ml
@@ -8,6 +8,7 @@ type basetype =
   | Integer
   | Real
   | CType
+  | Alloc_id
   | Loc of Sctypes.t option
   | Struct of Sym.t
   | Datatype of Sym.t
@@ -49,6 +50,7 @@ let rec pp = function
   | Integer -> !^"integer"
   | Real -> !^"real"
   | CType -> !^"ctype"
+  | Alloc_id -> !^"alloc_id"
   | Loc (Some ct) -> !^"pointer" ^^ angles (Sctypes.pp ct)
   | Loc None -> !^"pointer"
   | Struct sym -> !^"struct" ^^^ Sym.pp sym
@@ -114,6 +116,7 @@ let rec of_basetype = function
   | BT.Integer -> Integer
   | BT.Real -> Real
   | BT.CType -> CType
+  | BT.Alloc_id -> Alloc_id
   | BT.Loc -> Loc None
   | BT.Struct tag -> Struct tag
   | BT.Datatype tag -> Datatype tag
@@ -130,6 +133,7 @@ let rec to_basetype = function
   | Integer -> BT.Integer
   | Real -> BT.Real
   | CType -> BT.CType
+  | Alloc_id -> BT.Alloc_id
   | Loc _ -> BT.Loc
   | Struct tag -> BT.Struct tag
   | Datatype tag -> BT.Datatype tag
diff --git a/backend/cn/terms.ml b/backend/cn/terms.ml
index 5754679d1..1af6b4d6e 100644
--- a/backend/cn/terms.ml
+++ b/backend/cn/terms.ml
@@ -5,6 +5,7 @@ type const =
   | Z of Z.t
   | Q of Q.t
   | Pointer of Z.t
+  | Alloc_id of Z.t
   | Bool of bool
   | Unit
   | Null
@@ -146,6 +147,7 @@ let pp : 'bt 'a. ?atomic:bool -> ?f:('bt term -> Pp.doc -> Pp.doc) -> 'bt term -
           |  Dec -> !^(Z.to_string i)
           | _ -> !^("0X" ^ (Z.format "016X" i))
           end
+       | Alloc_id i -> !^("@" ^ Z.to_string i)
        | Bool true -> !^"true"
        | Bool false -> !^"false"
        | Unit -> !^"void"
diff --git a/backend/cn/wellTyped.ml b/backend/cn/wellTyped.ml
index ce7b4c4d9..3856b93b7 100644
--- a/backend/cn/wellTyped.ml
+++ b/backend/cn/wellTyped.ml
@@ -101,6 +101,7 @@ module WBT = struct
       | Bool -> return ()
       | Integer -> return ()
       | Real -> return ()
+      | Alloc_id -> return ()
       | Loc -> return ()
       | CType -> return ()
       | Struct tag -> let@ _struct_decl = get_struct_decl loc tag in return ()
@@ -194,6 +195,8 @@ module WIT = struct
          return (IT (Const (Q q), Real))
       | Const (Pointer p) ->
          return (IT (Const (Pointer p), Loc))
+      | Const (Alloc_id p) ->
+         return (IT (Const (Alloc_id p), BT.Alloc_id))
       | Const (Bool b) ->
          return (IT (Const (Bool b), BT.Bool))
       | Const Unit ->