diff --git a/benchmark/case_0.c b/benchmark/case_0.c
index e954c07a..ad0a186e 100644
--- a/benchmark/case_0.c
+++ b/benchmark/case_0.c
@@ -1,12 +1,11 @@
 #include <stdlib.h>
 
 int main(){
-    int whatever;
+    // int whatever;
     int * data = malloc(sizeof(int));
-    int data2[10];
-    *(data + 1) = whatever;
-    int n = *(data + 1);
-    if(n > 0) {
-        free(data);
-    }
+    // // *(data + 1) = whatever;
+    // int n = *data;
+    // if(n > 0) {
+    //     free(data);
+    // }
 }
diff --git a/src/goto-symex/builtin_functions.cpp b/src/goto-symex/builtin_functions.cpp
index a593e0a5..7f4385cb 100644
--- a/src/goto-symex/builtin_functions.cpp
+++ b/src/goto-symex/builtin_functions.cpp
@@ -237,7 +237,6 @@ expr2tc goto_symext::symex_mem(
 
   expr2tc ptr_obj = pointer_object2tc(pointer_type2(), ptr_rhs);
   track_new_pointer(ptr_obj, new_type);
-  ptr_obj->dump();
   dynamic_memory.emplace_back(
     rhs_copy, alloc_guard, !is_malloc, symbol.name.as_string());
 
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index 69f8b5da..1832263c 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -169,15 +169,11 @@ void goto_symext::symex_assign(
   {
     symex_printf(lhs, rhs);
   }
-  // log_status("ZZZZZZZZZZ assign lhs after dereference and replace: ");
-  // lhs->dump();
-  // log_status("ZZZZZZZZZZ assign rhs after dereference and replace: ");
-  // rhs->dump();
   if (is_sideeffect2t(rhs))
   {
     // check what symex_mem represent
 
-    log_status("is side effect rhs: ");
+    log_status("is side effect rhs ");
     const sideeffect2t &effect = to_sideeffect2t(rhs);
     // effect.dump();
     switch (effect.kind)
@@ -235,46 +231,57 @@ void goto_symext::symex_assign_rec(
 {
   if (is_symbol2t(lhs))
   {
+    log_status("symex_assign_symbol");
     symex_assign_symbol(lhs, full_lhs, rhs, full_rhs, guard, hidden);
   }
   else if (is_index2t(lhs))
   {
+    log_status("symex_assign_array");
     symex_assign_array(lhs, full_lhs, rhs, full_rhs, guard, hidden);
   }
   else if (is_member2t(lhs))
   {
+    log_status("symex_assign_member");
     symex_assign_member(lhs, full_lhs, rhs, full_rhs, guard, hidden);
   }
   else if (is_if2t(lhs))
   {
+    log_status("symex_assign_if");
     symex_assign_if(lhs, full_lhs, rhs, full_rhs, guard, hidden);
   }
   else if (is_typecast2t(lhs) || is_bitcast2t(lhs))
   {
+    log_status("symex_assign_typecast");
     symex_assign_typecast(lhs, full_lhs, rhs, full_rhs, guard, hidden);
   }
   else if (is_constant_string2t(lhs) || is_null_object2t(lhs))
   {
+    log_status("is_constant_string2t(lhs) || is_null_object2t(lhs)");
     // ignore
   }
   else if (is_byte_extract2t(lhs))
   {
+    log_status("symex_assign_byte_extract");
     symex_assign_byte_extract(lhs, full_lhs, rhs, full_rhs, guard, hidden);
   }
   else if (is_concat2t(lhs))
   {
+    log_status("symex_assign_concat");
     symex_assign_concat(lhs, full_lhs, rhs, full_rhs, guard, hidden);
   }
   else if (is_constant_struct2t(lhs))
   {
+    log_status("symex_assign_structure");
     symex_assign_structure(lhs, full_lhs, rhs, full_rhs, guard, hidden);
   }
   else if (is_extract2t(lhs))
   {
+    log_status("symex_assign_extract");
     symex_assign_extract(lhs, full_lhs, rhs, full_rhs, guard, hidden);
   }
   else if (is_bitand2t(lhs))
   {
+    log_status("symex_assign_bitfield");
     symex_assign_bitfield(lhs, full_lhs, rhs, full_rhs, guard, hidden);
   }
   else
diff --git a/src/irep2/irep2.h b/src/irep2/irep2.h
index 5fb1debe..4a8439d3 100644
--- a/src/irep2/irep2.h
+++ b/src/irep2/irep2.h
@@ -40,6 +40,8 @@
 // clang-format off
 #define ESBMC_LIST_OF_EXPRS                                                    \
   BOOST_PP_LIST_CONS(constant_int,                                             \
+  BOOST_PP_LIST_CONS(constant_intloc,                                          \
+  BOOST_PP_LIST_CONS(constant_intheap,                                          \
   BOOST_PP_LIST_CONS(constant_fixedbv,                                         \
   BOOST_PP_LIST_CONS(constant_floatbv,                                         \
   BOOST_PP_LIST_CONS(constant_bool,                                            \
@@ -101,6 +103,8 @@
   BOOST_PP_LIST_CONS(with,                                                     \
   BOOST_PP_LIST_CONS(member,                                                   \
   BOOST_PP_LIST_CONS(index,                                                    \
+  BOOST_PP_LIST_CONS(points_to,                                                    \
+  BOOST_PP_LIST_CONS(uplus,                                                    \
   BOOST_PP_LIST_CONS(isnan,                                                    \
   BOOST_PP_LIST_CONS(overflow,                                                 \
   BOOST_PP_LIST_CONS(overflow_cast,                                            \
@@ -141,7 +145,7 @@
   BOOST_PP_LIST_CONS(signbit,                                                  \
   BOOST_PP_LIST_CONS(concat,                                                   \
   BOOST_PP_LIST_CONS(extract,                                                  \
-  BOOST_PP_LIST_NIL))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
+  BOOST_PP_LIST_NIL))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
 
 #define ESBMC_LIST_OF_TYPES                                                    \
   BOOST_PP_LIST_CONS(bool,                                                     \
@@ -158,8 +162,10 @@
   BOOST_PP_LIST_CONS(fixedbv,                                                  \
   BOOST_PP_LIST_CONS(string,                                                   \
   BOOST_PP_LIST_CONS(cpp_name,                                                 \
-  BOOST_PP_LIST_NIL))))))))))))))
-// clang-format on
+  BOOST_PP_LIST_CONS(intheap,                                                  \
+  BOOST_PP_LIST_CONS(intloc,                                                  \
+  BOOST_PP_LIST_NIL))))))))))))))))
+// clang-format ondata
 
 // Even crazier forward decs,
 namespace esbmct
@@ -424,6 +430,8 @@ class type2t : public irep2t
     fixedbv_id,
     floatbv_id,
     cpp_name_id,
+    intheap_id,
+    intloc_id,
     end_type_id
   };
 
diff --git a/src/irep2/irep2_expr.cpp b/src/irep2/irep2_expr.cpp
index e6228ec5..55dd0ca8 100644
--- a/src/irep2/irep2_expr.cpp
+++ b/src/irep2/irep2_expr.cpp
@@ -11,6 +11,8 @@
 
 static const char *expr_names[] = {
   "constant_int",
+  "constant_intloc",
+  "constant_intheap",
   "constant_fixedbv",
   "constant_floatbv",
   "constant_bool",
@@ -72,6 +74,8 @@ static const char *expr_names[] = {
   "with",
   "member",
   "index",
+  "points_to",
+  "uplus",
   "isnan",
   "overflow",
   "overflow_cast",
diff --git a/src/irep2/irep2_expr.h b/src/irep2/irep2_expr.h
index 61f35af5..cf2d65ad 100644
--- a/src/irep2/irep2_expr.h
+++ b/src/irep2/irep2_expr.h
@@ -48,6 +48,48 @@ class constant_int_data : public constant2t
   typedef esbmct::expr2t_traits<value_field> traits;
 };
 
+
+
+class constant_intloc_data : public constant2t 
+{
+
+public:
+  constant_intloc_data(const type2tc &t, expr2t::expr_ids id, const BigInt &bint)
+    : constant2t(t, id), value(bint)
+  {
+  }
+  constant_intloc_data(const constant_intloc_data &ref) = default;
+
+  BigInt value;
+
+  // Type mangling:
+  typedef esbmct::
+    field_traits<BigInt, constant_intloc_data, &constant_intloc_data::value>
+      value_field;
+  typedef esbmct::expr2t_traits<value_field> traits;
+};
+
+
+class constant_intheap_data : public constant2t 
+{
+
+public:
+  constant_intheap_data(const type2tc &t, expr2t::expr_ids id, const bool e)
+    : constant2t(t, id), is_emp(e)
+  {
+  }
+  constant_intheap_data(const constant_intheap_data &ref) = default;
+
+  bool is_emp;
+
+  // Type mangling:
+  typedef esbmct::
+    field_traits<bool, constant_intheap_data, &constant_intheap_data::is_emp>
+      value_field;
+  typedef esbmct::expr2t_traits<value_field> traits;
+};
+
+
 class constant_fixedbv_data : public constant2t
 {
 public:
@@ -857,6 +899,63 @@ class index_data : public datatype_ops
   typedef esbmct::expr2t_traits<source_value_field, index_field> traits;
 };
 
+class points_to_data : public expr2t 
+{
+public:
+  points_to_data(
+    const type2tc &t,
+    datatype_ops::expr_ids id,
+    const expr2tc &addrloc,
+    const expr2tc &content,
+    bool is_loc) : expr2t(t, id), addr(addrloc), content(content), is_loc_content(is_loc) {
+
+    }
+  points_to_data(const points_to_data& ref) = default;
+
+
+  expr2tc addr;
+  expr2tc content;
+  bool is_loc_content;
+
+  // Type mangling:
+  typedef esbmct::field_traits<expr2tc, points_to_data, &points_to_data::addr>
+    addr_field;
+  typedef esbmct::field_traits<expr2tc, points_to_data, &points_to_data::content>
+    content_field;
+  typedef esbmct::field_traits<bool, points_to_data, &points_to_data::is_loc_content>
+    is_loc_content_field;
+  typedef esbmct::expr2t_traits<addr_field, content_field, is_loc_content_field> traits;
+
+};
+
+
+class uplus_data : public expr2t
+{
+public:
+
+  uplus_data(
+    const type2tc &t,
+    datatype_ops::expr_ids id,
+    std::vector<expr2tc> members, 
+    unsigned int m_num) : expr2t(t, id), uplus_members(std::move(members)), member_num(m_num) 
+    {
+
+    }
+  uplus_data(const uplus_data& ref) = default;
+
+
+  std::vector<expr2tc> uplus_members;
+  unsigned int member_num;
+
+  // Type mangling:
+  typedef esbmct::field_traits<std::vector<expr2tc>, uplus_data, &uplus_data::uplus_members>
+    uplus_members_field;
+  typedef esbmct::field_traits<unsigned int, uplus_data, &uplus_data::member_num>
+    member_num_field;
+  typedef esbmct::expr2t_traits<uplus_members_field, member_num_field> traits;
+
+};
+
 class string_ops : public expr2t
 {
 public:
@@ -1423,6 +1522,8 @@ class extract_data : public expr2t
 // magic because the mapping between top level expr class and it's data holding
 // object isn't regular: the data class depends on /what/ the expression /is/.
 irep_typedefs(constant_int, constant_int_data);
+irep_typedefs(constant_intloc, constant_intloc_data);
+irep_typedefs(constant_intheap, constant_intheap_data);
 irep_typedefs(constant_fixedbv, constant_fixedbv_data);
 irep_typedefs(constant_floatbv, constant_floatbv_data);
 irep_typedefs(constant_struct, constant_datatype_data);
@@ -1481,6 +1582,8 @@ irep_typedefs(byte_update, byte_update_data);
 irep_typedefs(with, with_data);
 irep_typedefs(member, member_data);
 irep_typedefs(index, index_data);
+irep_typedefs(points_to, points_to_data);
+irep_typedefs(uplus, uplus_data);
 irep_typedefs(isnan, bool_1op);
 irep_typedefs(overflow, overflow_ops);
 irep_typedefs(overflow_cast, overflow_cast_data);
@@ -1552,6 +1655,28 @@ class constant_int2t : public constant_int_expr_methods
   static std::string field_names[esbmct::num_type_fields];
 };
 
+class constant_intloc2t : public constant_intloc_expr_methods
+{
+  public:
+  constant_intloc2t(const type2tc &type, const BigInt &input)
+    : constant_intloc_expr_methods(type, constant_intloc_id, input)
+  {
+  }
+  unsigned long as_ulong() const;
+  static std::string field_names[esbmct::num_type_fields];
+};
+
+class constant_intheap2t : public constant_intheap_expr_methods
+{
+  public:
+  constant_intheap2t(const type2tc &type, bool is_emp)
+    : constant_intheap_expr_methods(type, constant_intheap_id, is_emp)
+  {
+  }
+  bool get_is_emp() const;
+  static std::string field_names[esbmct::num_type_fields];
+};
+
 /** Constant fixedbv class. Records a fixed-width number in what I assume
  *  to be mantissa/exponent form, but which is described throughout CBMC code
  *  as fraction/integer parts. Stored in a fixedbvt.
@@ -2915,6 +3040,34 @@ class index2t : public index_expr_methods
   static std::string field_names[esbmct::num_type_fields];
 };
 
+class points_to2t : public points_to_expr_methods
+{
+public:
+  points_to2t(const type2tc &type, const expr2tc addr, const expr2tc& content, bool is_loc) : points_to_expr_methods(type, points_to_id, addr, content, is_loc) {
+
+  }
+  points_to2t(const points_to2t &ref) = default;
+
+
+  static std::string field_names[esbmct::num_type_fields];
+
+};
+
+
+class uplus2t : public uplus_expr_methods
+{
+public:
+  uplus2t(const type2tc &type, 
+  std::vector<expr2tc> uplus_members) : uplus_expr_methods(type, uplus_id, std::move(uplus_members), uplus_members.size()) {
+
+  }
+  uplus2t(const uplus2t &ref) = default;
+
+  
+  static std::string field_names[esbmct::num_type_fields];
+
+};
+
 /** Is operand not-a-number. Used to implement C library isnan function for
  *  float/double values. Boolean result. @extends arith_1op */
 class isnan2t : public isnan_expr_methods
diff --git a/src/irep2/irep2_type.cpp b/src/irep2/irep2_type.cpp
index 21b6514e..78008ae7 100644
--- a/src/irep2/irep2_type.cpp
+++ b/src/irep2/irep2_type.cpp
@@ -27,6 +27,8 @@ static const char *type_names[] = {
   "signedbv",
   "fixedbv",
   "floatbv",
+  "intheap",
+  "intloc",
   "cpp_name"};
 // If this fires, you've added/removed a type id, and need to update the list
 // above (which is ordered according to the enum list)
@@ -181,6 +183,14 @@ unsigned int empty_type2t::get_width() const
 {
   throw symbolic_type_excp();
 }
+unsigned int intheap_type2t::get_width() const
+{
+  throw symbolic_type_excp();
+}
+unsigned int intloc_type2t::get_width() const
+{
+  throw symbolic_type_excp();
+}
 
 unsigned int symbol_type2t::get_width() const
 {
diff --git a/src/irep2/irep2_type.h b/src/irep2/irep2_type.h
index c80435cb..a57692c0 100644
--- a/src/irep2/irep2_type.h
+++ b/src/irep2/irep2_type.h
@@ -21,6 +21,8 @@ class pointer_type2t;
 class fixedbv_type2t;
 class floatbv_type2t;
 class cpp_name_type2t;
+class intheap_type2t;
+class intloc_type2t;
 
 // We also require in advance, the actual classes that store type data.
 
@@ -201,6 +203,7 @@ class array_data : public type2t
       traits;
 };
 
+
 class pointer_data : public type2t
 {
 public:
@@ -286,6 +289,7 @@ class cpp_name_data : public type2t
   typedef esbmct::type2t_traits<name_field, template_args_field> traits;
 };
 
+
 // Then give them a typedef name
 
 #define irep_typedefs(basename, superclass)                                    \
@@ -315,6 +319,8 @@ irep_typedefs(fixedbv, fixedbv_data);
 irep_typedefs(floatbv, floatbv_data);
 irep_typedefs(cpp_name, cpp_name_data);
 irep_typedefs(vector, array_data);
+irep_typedefs(intheap, type2t);
+irep_typedefs(intloc, type2t);
 #undef irep_typedefs
 
 /** Boolean type.
@@ -349,6 +355,30 @@ class empty_type2t : public empty_type_methods
   static std::string field_names[esbmct::num_type_fields];
 };
 
+class intheap_type2t : public intheap_type_methods
+{
+public:
+  intheap_type2t() : intheap_type_methods(intheap_id)
+  {
+  }
+  intheap_type2t(const intheap_type2t &ref) = default;
+  unsigned int get_width() const override;
+
+  static std::string field_names[esbmct::num_type_fields];
+};
+
+class intloc_type2t : public intloc_type_methods
+{
+public:
+  intloc_type2t() : intloc_type_methods(intloc_id)
+  {
+  }
+  intloc_type2t(const intloc_type2t &ref) = default;
+  unsigned int get_width() const override;
+
+  static std::string field_names[esbmct::num_type_fields];
+};
+
 /** Symbolic type.
  *  Temporary, prior to linking up types after parsing, or when a struct/array
  *  contains a recursive pointer to its own type.
@@ -713,6 +743,8 @@ class cpp_name_type2t : public cpp_name_type_methods
 
 type_macros(bool);
 type_macros(empty);
+type_macros(intheap);
+type_macros(intloc);
 type_macros(symbol);
 type_macros(struct);
 type_macros(union);
diff --git a/src/irep2/irep2_utils.h b/src/irep2/irep2_utils.h
index 6919d53f..5fc0eca7 100644
--- a/src/irep2/irep2_utils.h
+++ b/src/irep2/irep2_utils.h
@@ -271,6 +271,17 @@ inline expr2tc gen_slong(signed long val)
   return constant_int2tc(get_int_type(config.ansi_c.word_size), BigInt(val));
 }
 
+
+inline expr2tc gen_emp() 
+{
+  return constant_intheap2tc(get_intheap_type(), true);
+}
+
+inline expr2tc gen_intloc_constant(unsigned long val)
+{
+  return constant_intloc2tc(get_intloc_type(), BigInt(val));
+}
+
 inline const type2tc &get_array_subtype(const type2tc &type)
 {
   return to_array_type(type).subtype;
@@ -290,6 +301,7 @@ inline const type2tc &get_base_array_subtype(const type2tc &type)
   return subtype;
 }
 
+
 inline bool simplify(expr2tc &expr)
 {
   expr2tc tmp = expr->simplify();
diff --git a/src/irep2/templates/irep2_templates.cpp b/src/irep2/templates/irep2_templates.cpp
index 22a7b4bf..7ed3de87 100644
--- a/src/irep2/templates/irep2_templates.cpp
+++ b/src/irep2/templates/irep2_templates.cpp
@@ -9,6 +9,10 @@ std::string bool_type2t::field_names[esbmct::num_type_fields] =
   {"", "", "", "", ""};
 std::string empty_type2t::field_names[esbmct::num_type_fields] =
   {"", "", "", "", ""};
+std::string intloc_type2t::field_names[esbmct::num_type_fields] =
+  {"", "", "", "", ""};
+std::string intheap_type2t::field_names[esbmct::num_type_fields] =
+  {"", "", "", "", ""};
 std::string symbol_type2t::field_names[esbmct::num_type_fields] =
   {"symbol_name", "", "", "", ""};
 std::string struct_type2t::field_names[esbmct::num_type_fields] =
@@ -38,6 +42,8 @@ std::string cpp_name_type2t::field_names[esbmct::num_type_fields] =
 
 std::string constant_int2t::field_names[esbmct::num_type_fields] =
   {"value", "", "", "", ""};
+std::string constant_intloc2t::field_names[esbmct::num_type_fields] = {"value" , "", "", "", ""};
+std::string constant_intheap2t::field_names[esbmct::num_type_fields] = {"is_emp" , "", "", "", ""};
 std::string constant_fixedbv2t::field_names[esbmct::num_type_fields] =
   {"value", "", "", "", ""};
 std::string constant_floatbv2t::field_names[esbmct::num_type_fields] =
diff --git a/src/irep2/templates/irep2_templates_type.cpp b/src/irep2/templates/irep2_templates_type.cpp
index 0c28226e..6e7307a4 100644
--- a/src/irep2/templates/irep2_templates_type.cpp
+++ b/src/irep2/templates/irep2_templates_type.cpp
@@ -2,6 +2,8 @@
 
 type_typedefs_empty(bool_type, type2t);
 type_typedefs_empty(empty_type, type2t);
+type_typedefs_empty(intheap_type, type2t);
+type_typedefs_empty(intloc_type, type2t);
 type_typedefs1(symbol_type, symbol_type_data);
 type_typedefs5(struct_type, struct_union_data);
 type_typedefs5(union_type, struct_union_data);
diff --git a/src/util/c_types.cpp b/src/util/c_types.cpp
index 43a2a672..53da0d67 100644
--- a/src/util/c_types.cpp
+++ b/src/util/c_types.cpp
@@ -393,3 +393,14 @@ type2tc get_empty_type()
   static type2tc empty_type = empty_type2tc();
   return empty_type;
 }
+
+type2tc get_intheap_type() {
+  static type2tc intheap_type = intheap_type2tc();
+  return intheap_type;
+}
+
+type2tc get_intloc_type() {
+  static type2tc intloc_type = intloc_type2tc();
+  return intloc_type;
+}
+
diff --git a/src/util/c_types.h b/src/util/c_types.h
index f50e1fdb..66886eea 100644
--- a/src/util/c_types.h
+++ b/src/util/c_types.h
@@ -72,6 +72,8 @@ type2tc get_uint_type(unsigned int sz);
 type2tc get_int_type(unsigned int sz);
 type2tc get_bool_type();
 type2tc get_empty_type();
+type2tc get_intheap_type();
+type2tc get_intloc_type();
 
 type2tc size_type2();
 type2tc signed_size_type2();
diff --git a/src/util/type.cpp b/src/util/type.cpp
index 7a7da5ad..15e559b2 100644
--- a/src/util/type.cpp
+++ b/src/util/type.cpp
@@ -32,6 +32,8 @@ irep_idt typet::t_union = dstring("union");
 irep_idt typet::t_class = dstring("class");
 irep_idt typet::t_code = dstring("code");
 irep_idt typet::t_array = dstring("array");
+irep_idt typet::t_intheap = dstring("intheap");
+irep_idt typet::t_intloc = dstring("intloc");
 irep_idt typet::t_pointer = dstring("pointer");
 irep_idt typet::t_reference = dstring("#reference");
 irep_idt typet::t_bv = dstring("bv");
diff --git a/src/util/type.h b/src/util/type.h
index c270418e..7a3a33d8 100644
--- a/src/util/type.h
+++ b/src/util/type.h
@@ -100,6 +100,8 @@ class typet : public irept
   static irep_idt t_reference;
   static irep_idt t_bv;
   static irep_idt t_vector;
+  static irep_idt t_intheap;
+  static irep_idt t_intloc;
 
   static irep_idt t_intcap;
   static irep_idt t_uintcap;