diff --git a/src/goto-symex/builtin_functions.cpp b/src/goto-symex/builtin_functions.cpp
index 2f107035..9422f210 100644
--- a/src/goto-symex/builtin_functions.cpp
+++ b/src/goto-symex/builtin_functions.cpp
@@ -281,10 +281,7 @@ expr2tc goto_symext::symex_mem(
     symbol.mode = "C";
     new_context.add(symbol);
 
-    expr2tc rhs_heap = symbol2tc(heap_type, symbol.id);
-    guardt rhs_guard = cur_state->guard;
-
-    // set a location for new heap region
+    // create a new location for new heap region
     symbolt heap_region_loc;
     heap_region_loc.name = "heap_region_loc_"+ i2string(dynamic_counter);
     
@@ -301,6 +298,12 @@ expr2tc goto_symext::symex_mem(
     // use l2 symbol, do not need to be renamed
     cur_state->rename(rhs_base_loc);
 
+    // store base location in intheap type
+    _heap_type.location = rhs_base_loc;
+
+    expr2tc rhs_heap = symbol2tc(heap_type, symbol.id);
+    guardt rhs_guard = cur_state->guard;
+
     expr2tc rhs_region = heap_region2tc(heap_type, rhs_heap, rhs_base_loc);
     
     log_status("symex assign in symex_mem: allocated_heap = heaplet");
@@ -320,7 +323,7 @@ expr2tc goto_symext::symex_mem(
     );
 
     log_status("create valueset base loc symbol and assign");
-    symex_assign(code_assign2tc(lhs, locationof2tc(rhs_region)));
+    symex_assign(code_assign2tc(lhs, locationof2tc(rhs_heap)));
 
     return expr2tc();
   }
@@ -459,14 +462,12 @@ void goto_symext::symex_free(const expr2tc &expr)
     // set each heap region to empty, guarded by item.gurad
     for(auto const& item : internal_deref_items)
     {
-      assert(is_heap_region2t(item.object));
+      assert(is_intheap_type(item.object));
       log_status("free object guard");
       item.guard->dump();
-      
-      const heap_region2t& heap_region = to_heap_region2t(item.object);
-      expr2tc free_heap = heap_region.flag;
+
       guardt g; g.add(item.guard);
-      symex_assign(code_assign2tc(free_heap, gen_emp()), false, g);
+      symex_assign(code_assign2tc(item.object, gen_emp()), false, g);
 
       // collect guards for deleting heap alloc size
       when = or2tc(when, item.guard);
diff --git a/src/goto-symex/dynamic_allocation.cpp b/src/goto-symex/dynamic_allocation.cpp
index b3905450..02ea409c 100644
--- a/src/goto-symex/dynamic_allocation.cpp
+++ b/src/goto-symex/dynamic_allocation.cpp
@@ -33,9 +33,15 @@ void goto_symext::default_replace_dynamic_allocation(expr2tc &expr)
       // Checking that the object is valid by heap_alloc_size
       log_status(" --- generate cond for checking heap region --- ");
       const valid_object2t &obj = to_valid_object2t(expr);
-      obj.dump();
-      const heap_region2t &valid_inner = to_heap_region2t(obj.value);
-      const intheap_type2t &_type = to_intheap_type(valid_inner.type);
+      const expr2tc &heap_region = obj.value;
+      if (!is_intheap_type(heap_region->type) ||
+          !to_intheap_type(heap_region->type).is_region)
+      {
+        log_error("Wrong object");
+        abort();
+      }
+
+      const intheap_type2t &_type = to_intheap_type(heap_region->type);
       // get alloc size heap
       expr2tc alloc_size_heap;
       migrate_expr(symbol_expr(*ns.lookup(alloc_size_heap_name)), alloc_size_heap);
@@ -44,7 +50,7 @@ void goto_symext::default_replace_dynamic_allocation(expr2tc &expr)
       expr2tc heap_contain =
         heap_contain2tc(
           alloc_size_heap,
-          points_to2tc(valid_inner.source_location, size)
+          points_to2tc(_type.location, size)
         );
       expr = heap_contain;
       log_status(" --- generate cond for checking heap region --- ");
diff --git a/src/goto-symex/goto_symex.h b/src/goto-symex/goto_symex.h
index eb21851b..71b248ab 100644
--- a/src/goto-symex/goto_symex.h
+++ b/src/goto-symex/goto_symex.h
@@ -969,8 +969,8 @@ class symex_dereference_statet : public dereference_callbackt
   dump_internal_state(const std::list<struct internal_item> &data) override;
   bool is_live_variable(const expr2tc &sym) override;
 
-  void update_heap_type(const expr2tc &flag) override;
-  void update_heap_type_rec(expr2tc &expr, const symbol2t &flag) override;
+  void update_heap_type(const intheap_type2t &type) override;
+  void update_heap_type_rec(expr2tc &expr, const intheap_type2t &type) override;
   std::string get_nondet_id(std::string prefix = "") override;
   irep_idt get_alloc_size_heap_name() override;
 };
diff --git a/src/goto-symex/goto_symex_state.cpp b/src/goto-symex/goto_symex_state.cpp
index 496ec218..92f179f9 100644
--- a/src/goto-symex/goto_symex_state.cpp
+++ b/src/goto-symex/goto_symex_state.cpp
@@ -67,9 +67,7 @@ void goto_symex_statet::initialize(
 bool goto_symex_statet::constant_propagation(const expr2tc &expr) const
 {
   // SLHV propagation
-  if (is_constant_intheap2t(expr) ||
-      is_constant_intloc2t(expr) ||
-      is_heap_region2t(expr))
+  if (is_constant_intheap2t(expr) || is_constant_intloc2t(expr))
     return true;
 
   if (is_locadd2t(expr))
@@ -210,13 +208,6 @@ void goto_symex_statet::assignment(expr2tc &lhs, const expr2tc &rhs)
   expr2tc l1_lhs = lhs;
 
   expr2tc const_value = constant_propagation(rhs) ? rhs : expr2tc();
-
-  // Each heap region has only one unique flag that does not change
-  // during its lifetime. The l1 version of flag is the representation.
-  // For constant_propagation, all heap regions should hold their flag. 
-  if (!is_nil_expr(const_value) && is_heap_region2t(const_value))
-    level2.get_original_name(to_heap_region2t(const_value).flag);
-
   level2.make_assignment(lhs, const_value, rhs);
 
   if (use_value_set)
@@ -230,6 +221,7 @@ void goto_symex_statet::assignment(expr2tc &lhs, const expr2tc &rhs)
     l1_lhs->dump();
     log_status("#####");
     value_set.assign(l1_lhs, l1_rhs);
+    log_status("update value set done!!!!");
   }
 }
 
@@ -263,7 +255,8 @@ void goto_symex_statet::rename_type(expr2tc &expr)
 void goto_symex_statet::rename(expr2tc &expr)
 {
   // rename all the symbols with their last known value
-  if (is_nil_expr(expr))
+  if (is_nil_expr(expr) ||
+      is_heap_region2t(expr))
     return;
 
   rename_type(expr);
@@ -280,15 +273,6 @@ void goto_symex_statet::rename(expr2tc &expr)
     address_of2t &addrof = to_address_of2t(expr);
     rename_address(addrof.ptr_obj);
   }
-  else  if (is_heap_region2t(expr))
-  {
-    heap_region2t &heap_region = to_heap_region2t(expr);
-    rename(heap_region.source_location);
-    // Return to l1 name first
-    level2.get_original_name(heap_region.flag);
-    // Get the newest l2 name
-    level2.get_ident_name(heap_region.flag);
-  }
   else
   {
     // do this recursively
diff --git a/src/goto-symex/slice.cpp b/src/goto-symex/slice.cpp
index 8e7def16..b1d97c6a 100644
--- a/src/goto-symex/slice.cpp
+++ b/src/goto-symex/slice.cpp
@@ -15,19 +15,14 @@ bool symex_slicet::get_symbols(const expr2tc &expr)
   // locationof only has heap_region as oprend
   // the location of heap_region is completely fresh
   // and is not being used in symbolic execution
-  if (is_locationof2t(expr)) return false;
+  if (is_locationof2t(expr) || is_heap_region2t(expr)) return false;
 
-  if (is_heap_region2t(expr))
-    return get_symbols<Add>(to_heap_region2t(expr).flag);
-  else
-  {
-    // Recursively look if any of the operands has a inner symbol
-    expr->foreach_operand([this, &res](const expr2tc &e) {
-      if (!is_nil_expr(e))
-        res |= get_symbols<Add>(e);
-      return res;
-    });
-  }
+  // Recursively look if any of the operands has a inner symbol
+  expr->foreach_operand([this, &res](const expr2tc &e) {
+    if (!is_nil_expr(e))
+      res |= get_symbols<Add>(e);
+    return res;
+  });
 
   if (!is_symbol2t(expr))
     return res;
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index 8076f61a..c734ce2d 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -294,6 +294,7 @@ void goto_symext::symex_assign_rec(
   {
     log_status("symex_assign_symbol");
     symex_assign_symbol(lhs, full_lhs, rhs, full_rhs, guard, hidden);
+    log_status("symex_assign_symbol done!!!");
   } 
   else if (is_index2t(lhs))
   {
@@ -349,10 +350,7 @@ void goto_symext::symex_assign_rec(
   {
     log_status("symex_assign_fieldof");
     symex_assign_fieldof(lhs, full_lhs, rhs, full_rhs, guard, hidden);
-  }
-  else if (is_heap_region2t(lhs))
-  {
-    log_status("symex_assign_heap_region");
+    log_status("symex_assign_fieldof done!!!");
   }
   else
   {
@@ -397,6 +395,8 @@ void goto_symext::symex_assign_symbol(
 
   cur_state->assignment(renamed_lhs, rhs);
 
+  log_status("cur state assignment done!!!");
+
   // Special case when the lhs is an array access, we need to get the
   // right symbol for the index
   expr2tc new_lhs = full_lhs;
@@ -906,18 +906,13 @@ void goto_symext::symex_assign_fieldof(
   assert(is_scalar_type(rhs));
 
   const fieldof2t& fieldof = to_fieldof2t(lhs);
-  const heap_region2t &heap_region = to_heap_region2t(fieldof.source_heap);
+  const expr2tc &heap_region = fieldof.source_heap;
   const expr2tc &field = fieldof.operand;
 
   expr2tc update_heap =
-    heap_update2tc(heap_region.type, fieldof.source_heap, field, rhs);
+    heap_update2tc(heap_region->type, heap_region, field, rhs);
 
-  symex_assign_rec(
-    heap_region.flag,
-    fieldof.source_heap,
-    update_heap,
-    update_heap,
-    guard, hidden);
+  symex_assign_rec(heap_region, full_lhs, update_heap, full_rhs, guard, hidden);
 }
 
 void goto_symext::replace_nondet(expr2tc &expr)
diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp
index 042314a4..8801d3c2 100644
--- a/src/goto-symex/symex_dereference.cpp
+++ b/src/goto-symex/symex_dereference.cpp
@@ -166,82 +166,56 @@ bool symex_dereference_statet::is_live_variable(const expr2tc &symbol)
   return false;
 }
 
-void symex_dereference_statet::update_heap_type(const expr2tc &flag)
+void symex_dereference_statet::update_heap_type(const intheap_type2t &type)
 {
-  if (!is_symbol2t(flag))
+  if (is_nil_expr(to_intheap_type(type).location))
   {
-    log_error("Wrong flag!!!!");
+    log_error("Wrong type!!!!");
     abort();
   }
 
-  log_status("begin update heap type");
-  flag->dump();
-
-  // Each heap region has a unique L0 name
-  expr2tc l0_flag = flag;
-  goto_symex.cur_state->get_original_name(l0_flag);
-  const symbol2t l0_sym = to_symbol2t(l0_flag);
-
-  l0_flag->dump();
-
   // update value set
   value_sett& value_set = goto_symex.cur_state->value_set;
   unsigned int n = value_set.object_numbering.size();
   for(unsigned int i = 0; i < n; i++)
-    update_heap_type_rec(value_set.object_numbering[i], l0_sym);
-  
-
-  log_status("finishing update value set");
+    update_heap_type_rec(value_set.object_numbering[i], type);
 
   // update eq system
   std::shared_ptr<symex_target_equationt> eq =
     std::dynamic_pointer_cast<symex_target_equationt>(goto_symex.target);
   for(auto& ssa_step : eq->SSA_steps)
   {
-    update_heap_type_rec(ssa_step.guard, l0_sym);
-    update_heap_type_rec(ssa_step.rhs, l0_sym);
-    update_heap_type_rec(ssa_step.cond, l0_sym);
+    update_heap_type_rec(ssa_step.guard, type);
+    update_heap_type_rec(ssa_step.rhs, type);
+    update_heap_type_rec(ssa_step.cond, type);
   }
-
-  log_status("finishing replace");
 }
 
 void symex_dereference_statet::update_heap_type_rec(
-  expr2tc &expr, const symbol2t &flag)
+  expr2tc &expr, const intheap_type2t &type)
 {
   if (is_nil_expr(expr)) return;
-  log_status("update type of :");
-  expr->dump();
-  if (is_symbol2t(expr))
+  if (is_intheap_type(expr))
   {
-    // update heap variable
-    expr2tc l0_sym = expr;
-    goto_symex.cur_state->get_original_name(l0_sym);
+    intheap_type2t &_type = to_intheap_type(expr->type);
 
-    if (flag.get_symbol_name() == to_symbol2t(l0_sym).get_symbol_name())
-      expr->type = flag.type;
-  }
-  else if (is_heap_region2t(expr))
-  {
-    heap_region2t &heap_region = to_heap_region2t(expr);
-    
-    expr2tc l0_flag = heap_region.flag;
-    goto_symex.cur_state->get_original_name(l0_flag);
+    if (is_nil_expr(_type.location)) return;
 
-    l0_flag->dump();
-
-    if (flag.get_symbol_name() ==
-        to_symbol2t(l0_flag).get_symbol_name()) 
+    if (to_symbol2t(_type.location).get_symbol_name() ==
+        to_symbol2t(type.location).get_symbol_name())
+      expr->type = intheap_type2tc(type);
+    
+    if (is_heap_region2t(expr))
     {
-      heap_region.type = flag.type;
-      update_heap_type_rec(heap_region.flag, flag);
+      heap_region2t &heap_region = to_heap_region2t(expr);
+      update_heap_type_rec(heap_region.flag, type);
     }
   }
   else
   {
-    expr->Foreach_operand([this, &flag](expr2tc& e){
+    expr->Foreach_operand([this, &type](expr2tc& e){
       if (!is_nil_expr(e))
-        update_heap_type_rec(e, flag);
+        update_heap_type_rec(e, type);
     });
   }
 }
diff --git a/src/goto-symex/symex_main.cpp b/src/goto-symex/symex_main.cpp
index df99dbda..f68233c3 100644
--- a/src/goto-symex/symex_main.cpp
+++ b/src/goto-symex/symex_main.cpp
@@ -1226,8 +1226,7 @@ void goto_symext::add_memory_leak_checks()
     log_status(" ----------- [memleak encoding]----------- ");
     for (auto const &it : dynamic_memory){
       log_status("allocated object {}: ", it.name);
-      expr2tc obj_flag = flagof2tc(it.obj);
-      expr2tc deallocated = equality2tc(obj_flag, gen_emp());
+      expr2tc deallocated = equality2tc(it.obj, gen_emp());
       expr2tc when = it.alloc_guard.as_expr();
       expr2tc cond = implies2tc(when, deallocated);
       cur_state->rename(cond);
diff --git a/src/irep2/irep2.h b/src/irep2/irep2.h
index 601c5774..13a44369 100644
--- a/src/irep2/irep2.h
+++ b/src/irep2/irep2.h
@@ -107,7 +107,6 @@
   BOOST_PP_LIST_CONS(uplus,                                                    \
   BOOST_PP_LIST_CONS(locadd,                                                   \
   BOOST_PP_LIST_CONS(heap_region,                                              \
-  BOOST_PP_LIST_CONS(flagof,                                                   \
   BOOST_PP_LIST_CONS(locationof,                                               \
   BOOST_PP_LIST_CONS(fieldof,                                                  \
   BOOST_PP_LIST_CONS(heap_update,                                              \
@@ -154,7 +153,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,                                                     \
diff --git a/src/irep2/irep2_expr.cpp b/src/irep2/irep2_expr.cpp
index a49356a6..f293ef80 100644
--- a/src/irep2/irep2_expr.cpp
+++ b/src/irep2/irep2_expr.cpp
@@ -78,7 +78,6 @@ static const char *expr_names[] = {
   "uplus",
   "locadd",
   "heap_region",
-  "flagof",
   "locationof",
   "fieldof",
   "heap_update",
diff --git a/src/irep2/irep2_expr.h b/src/irep2/irep2_expr.h
index 4ef14c45..fe39b5e9 100644
--- a/src/irep2/irep2_expr.h
+++ b/src/irep2/irep2_expr.h
@@ -1704,7 +1704,6 @@ irep_typedefs(points_to, points_to_data);
 irep_typedefs(uplus, uplus_data);
 irep_typedefs(locadd, locadd_data);
 irep_typedefs(heap_region, heap_region_data);
-irep_typedefs(flagof, heap_ops);
 irep_typedefs(locationof, heap_ops);
 irep_typedefs(fieldof, heap_1op);
 irep_typedefs(heap_update, heap_2ops);
@@ -3231,18 +3230,6 @@ class heap_region2t : public heap_region_expr_methods
   static std::string field_names[esbmct::num_type_fields];
 };
 
-class flagof2t : public flagof_expr_methods
-{
-public:
-  flagof2t(const expr2tc &source_region)
-    : flagof_expr_methods(get_intheap_type(), flagof_id, source_region)
-  {
-  }
-  flagof2t(const flagof2t &ref) = default;
-
-  static std::string field_names[esbmct::num_type_fields];
-};
-
 class locationof2t : public locationof_expr_methods
 {
 public:
diff --git a/src/irep2/irep2_type.h b/src/irep2/irep2_type.h
index 1b80546c..9332b103 100644
--- a/src/irep2/irep2_type.h
+++ b/src/irep2/irep2_type.h
@@ -208,22 +208,26 @@ class intheap_data : public type2t
 public:
   intheap_data(
     type2t::type_ids id,
-    const std::vector<type2tc> &ft,
+    const expr2tc &loc,
     unsigned int tb,
     bool ir,
     bool ia)
-    : type2t(id), field_types(ft), total_bytes(tb),
+    : type2t(id),
+      location(loc), total_bytes(tb),
       is_region(ir), is_aligned(ia)
   {
   }
   intheap_data(const intheap_data &ref) = default;
 
+  expr2tc location;
   std::vector<type2tc> field_types;
   unsigned int total_bytes;
   bool is_region;
   bool is_aligned;
   
   // Type mangling:
+  typedef esbmct::field_traits<expr2tc, intheap_data, &intheap_data::location>
+    location_field;
   typedef esbmct::field_traits<std::vector<type2tc>, intheap_data, &intheap_data::field_types>
     field_types_field;
   typedef esbmct::field_traits<unsigned int, intheap_data, &intheap_data::total_bytes>
@@ -233,6 +237,7 @@ class intheap_data : public type2t
   typedef esbmct::field_traits<bool, intheap_data, &intheap_data::is_aligned>
     is_aligned_field;
   typedef esbmct::type2t_traits<
+    location_field,
     field_types_field,
     total_bytes_field,
     is_region_field,
@@ -394,11 +399,14 @@ class intheap_type2t : public intheap_type_methods
 {
 public:
   intheap_type2t(
-    const std::vector<type2tc> &field_types,
+    const expr2tc &location,
     unsigned int total_bytes,
     bool is_region,
     bool is_aligned)
-    : intheap_type_methods(intheap_id, field_types, total_bytes, is_region, is_aligned)
+    : intheap_type_methods(
+      intheap_id,
+      location, total_bytes,
+      is_region, is_aligned)
   {
     if (is_region && this->field_types.empty())
       this->field_types.push_back(empty_type2tc());
diff --git a/src/irep2/templates/irep2_templates.cpp b/src/irep2/templates/irep2_templates.cpp
index bbf67151..054df6e0 100644
--- a/src/irep2/templates/irep2_templates.cpp
+++ b/src/irep2/templates/irep2_templates.cpp
@@ -12,7 +12,7 @@ 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] =
-  {"field_types", "total_bytes", "is_region", "is_aligned", ""};
+  {"location", "field_types", "total_bytes", "is_region", "is_aligned", ""};
 std::string symbol_type2t::field_names[esbmct::num_type_fields] =
   {"symbol_name", "", "", "", ""};
 std::string struct_type2t::field_names[esbmct::num_type_fields] =
@@ -170,8 +170,6 @@ std::string locadd2t::field_names[esbmct::num_type_fields] =
   {"location", "offset", "", "", ""};
 std::string heap_region2t::field_names[esbmct::num_type_fields] = 
   {"flag", "source_location", "", "", ""};
-std::string flagof2t::field_names[esbmct::num_type_fields] =
-  {"source_region", "", "", "", ""};
 std::string locationof2t::field_names[esbmct::num_type_fields] =
   {"source_region", "", "", "", ""};
 std::string fieldof2t::field_names[esbmct::num_type_fields] =
diff --git a/src/irep2/templates/irep2_templates_expr_ops.cpp b/src/irep2/templates/irep2_templates_expr_ops.cpp
index 338cf3ef..fd7a2575 100644
--- a/src/irep2/templates/irep2_templates_expr_ops.cpp
+++ b/src/irep2/templates/irep2_templates_expr_ops.cpp
@@ -48,7 +48,6 @@ expr_typedefs1(isnan, bool_1op);
 expr_typedefs1(overflow_neg, overflow_ops);
 
 expr_typedefs1(locationof, heap_ops);
-expr_typedefs1(flagof, heap_ops);
 expr_typedefs3(fieldof, heap_1op);
 expr_typedefs4(heap_update, heap_2ops);
 expr_typedefs2(heap_append, heap_1op);
diff --git a/src/pointer-analysis/dereference.cpp b/src/pointer-analysis/dereference.cpp
index 3ae141e1..a32e2391 100644
--- a/src/pointer-analysis/dereference.cpp
+++ b/src/pointer-analysis/dereference.cpp
@@ -852,31 +852,28 @@ expr2tc dereferencet::build_reference_to(
       lexical_offset->dump();
 
     guardt tmp_guard(guard);
-    if (is_heap_region2t(value))
-    {
-      heap_region2t& heap_region = to_heap_region2t(value);
-
-      if (!is_free(mode) && !is_internal(mode))
-      {
-        int access_sz = type->get_width() / 8;
-        // Do alignment
-        intheap_type2t &_type = to_intheap_type(heap_region.type);
-        bool has_changed = _type.do_alignment(access_sz);
-        if (has_changed)
-        {
-          to_symbol2t(heap_region.flag).type = heap_region.type;
-          dereference_callback.update_heap_type(heap_region.flag);
-        }
-      }
-      pointer_guard = same_object2tc(deref_expr, locationof2tc(value));
-      tmp_guard.add(pointer_guard);
-    }
-    else
+    if (!is_intheap_type(value) ||
+        !to_intheap_type(value->type).is_region)
     {
       log_error("Not heap region");
       abort();
     }
 
+    intheap_type2t &_type = to_intheap_type(value->type);
+
+    if (!is_free(mode) && !is_internal(mode))
+    {
+      int access_sz = type->get_width() / 8;
+      // Do alignment
+      bool has_changed = _type.do_alignment(access_sz);
+      if (has_changed)
+        dereference_callback.update_heap_type(_type);
+    }
+    pointer_guard = same_object2tc(deref_expr, locationof2tc(value));
+    tmp_guard.add(pointer_guard);
+  
+
+
     log_status("generated pointer guard:");
     pointer_guard->dump();
 
@@ -929,8 +926,7 @@ expr2tc dereferencet::build_reference_to(
     }
 
     // other checks may be added later
-    if (is_heap_region2t(value))
-      check_heap_region_access(value, final_offset, type, tmp_guard, mode);
+    check_heap_region_access(value, final_offset, type, tmp_guard, mode);
 
     build_deref_slhv(value, final_offset, type, tmp_guard, mode, alignment);
 
@@ -1268,9 +1264,11 @@ void dereferencet::build_deref_slhv(
     abort();
   }
 
-  heap_region2t& heap_region = to_heap_region2t(value);
+  // value is the flag symbol of a heap region
+  expr2tc &heap_region = value;
+
   unsigned int field = to_constant_int2t(offset).value.to_uint64();
-  intheap_type2t &_type = to_intheap_type(heap_region.type);
+  intheap_type2t &_type = to_intheap_type(heap_region->type);
   unsigned int access_sz = type_byte_size(type, &ns).to_uint64();
 
   if (!_type.is_aligned)
@@ -1297,10 +1295,7 @@ void dereferencet::build_deref_slhv(
 
   // update field type
   if (_type.set_field_type(field, type))
-  {
-    heap_region.flag->type = heap_region.type;
-    dereference_callback.update_heap_type(heap_region.flag);
-  }
+    dereference_callback.update_heap_type(_type);
 
   log_status(" ----------------- build deref slhv ----------------- ");
 }
@@ -2313,6 +2308,22 @@ void dereferencet::valid_check(
     // always "valid", shut up
     return;
   }
+  else if(is_intheap_type(symbol))
+  {
+    log_status("guard : ");
+    guard.dump();
+    expr2tc not_valid_heap_region = not2tc(valid_object2tc(symbol));
+    log_status("not valid print:");
+    not_valid_heap_region->dump();
+    guardt tmp_guard(guard);
+    tmp_guard.add(not_valid_heap_region);
+    std::string foo = is_free(mode) ?  "invalid free pointer"
+                                      : "invalid dereference pointer";
+    // deref failure will replace heap region with heap contains
+    // that indicates the reigon is avaliable.
+    dereference_failure("pointer dereference", foo, tmp_guard);
+    return;
+  }
   else if (is_symbol2t(symbol))
   {
     // Hacks, but as dereferencet object isn't persistent, necessary. Fix by
@@ -2366,22 +2377,6 @@ void dereferencet::valid_check(
       }
     }
   }
-  else if(is_heap_region2t(symbol))
-  {
-    log_status("guard : ");
-    guard.dump();
-    expr2tc not_valid_heap_region = not2tc(valid_object2tc(symbol));
-    log_status("not valid print:");
-    not_valid_heap_region->dump();
-    guardt tmp_guard(guard);
-    tmp_guard.add(not_valid_heap_region);
-    std::string foo = is_free(mode) ?  "invalid free pointer"
-                                      : "invalid dereference pointer";
-    // deref failure will replace heap region with heap contains
-    // that indicates the reigon is avaliable.
-    dereference_failure("pointer dereference", foo, tmp_guard);
-    return;
-  }
 }
 
 void dereferencet::bounds_check(
diff --git a/src/pointer-analysis/dereference.h b/src/pointer-analysis/dereference.h
index 5e1f8857..a5766e54 100644
--- a/src/pointer-analysis/dereference.h
+++ b/src/pointer-analysis/dereference.h
@@ -154,13 +154,13 @@ class dereference_callbackt
   virtual bool is_live_variable(const expr2tc &sym) = 0;
 
 
-  virtual void update_heap_type(const expr2tc &flag)
+  virtual void update_heap_type(const intheap_type2t &type)
   {
     log_error("Do not support");
     abort();
   }
 
-  virtual void update_heap_type_rec(expr2tc &expr, const symbol2t &flag)
+  virtual void update_heap_type_rec(expr2tc &expr, const intheap_type2t &type)
   {
     log_error("Do not support");
     abort();
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
index 34477f95..bbf3e3ab 100644
--- a/src/pointer-analysis/value_set.cpp
+++ b/src/pointer-analysis/value_set.cpp
@@ -566,10 +566,7 @@ void value_sett::get_value_set_rec(
   }
   // SLHV:
   if (is_constant_intloc2t(expr) || is_constant_intheap2t(expr) ||
-      is_heap_append2t(expr) || is_heap_delete2t(expr) ||
-      // heap_region as a constant
-      // deref a heap region use fieldof(region, 0)
-      is_heap_region2t(expr))
+      is_heap_append2t(expr) || is_heap_delete2t(expr))
   {
     expr2tc new_object = expr;
     insert(dest, new_object, BigInt(0));
@@ -609,7 +606,8 @@ void value_sett::get_value_set_rec(
   if (is_fieldof2t(expr))
   {
     const fieldof2t &fieldof = to_fieldof2t(expr);
-    const heap_region2t &heap_region = to_heap_region2t(fieldof.source_heap);
+    const expr2tc &heap_region = fieldof.source_heap;
+    const intheap_type2t &_type = to_intheap_type(heap_region->type);
     expr2tc field = fieldof.operand;
 
     if (!is_constant_int2t(field))
@@ -621,7 +619,7 @@ void value_sett::get_value_set_rec(
     unsigned int _field = to_constant_int2t(field).value.to_uint64();
 
     get_value_set_rec(
-      heap_region.flag,
+      _type.location,
       dest,
       "::field::" + std::to_string(_field) + "::" + suffix,
       original_type
@@ -629,7 +627,8 @@ void value_sett::get_value_set_rec(
     return;
   }
 
-  if (is_heap_update2t(expr) || is_points_to2t(expr))
+  if (is_heap_update2t(expr) || is_points_to2t(expr) ||
+      is_heap_region2t(expr))
   {
     expr->dump();
     log_status("fini get_value_set_rec heap_update");
@@ -870,8 +869,7 @@ void value_sett::get_reference_set_rec(const expr2tc &expr, object_mapt &dest)
 {
   if (
     is_symbol2t(expr) || is_dynamic_object2t(expr) ||
-    is_constant_string2t(expr) || is_constant_array2t(expr)
-    || is_heap_region2t(expr))
+    is_constant_string2t(expr) || is_constant_array2t(expr))
   {
     // Any symbol we refer to, store into the destination object map.
     // Given that this is a simple symbol, we can be sure that the offset to
@@ -1247,6 +1245,17 @@ void value_sett::assign(
 
   if (is_intheap_type(lhs_type))
   {
+    if (is_heap_region2t(rhs))
+    {
+      // heap region is created for encoding
+      // the heap variable lhs contains all information
+      expr2tc new_obj = to_heap_region2t(rhs).flag;
+      object_mapt values_rhs;
+      // flag contains all neccessary information
+      insert(values_rhs, new_obj, BigInt(0));
+      assign_rec(lhs, values_rhs, "", add_to_sets);
+      return;
+    }
     if (to_intheap_type(lhs_type).is_region && is_heap_update2t(rhs))
     {
       const heap_update2t &heap_upd = to_heap_update2t(rhs);
@@ -1422,11 +1431,13 @@ void value_sett::assign_rec(
     }
 
     unsigned int _field = to_constant_int2t(field).value.to_uint64();
+    const expr2tc &heap_region = fieldof.source_heap;
+    const intheap_type2t &_type = to_intheap_type(heap_region->type);
 
-    const heap_region2t &heap_region = to_heap_region2t(fieldof.source_heap);
-
+    // TODO : fix
+    // use location to encoding field
     assign_rec(
-      heap_region.flag,
+      _type.location,
       values_rhs,
       "::field::" + std::to_string(_field) + "::" + suffix,
       add_to_sets);
diff --git a/src/solvers/smt/smt_conv.cpp b/src/solvers/smt/smt_conv.cpp
index efc37b22..39a92714 100644
--- a/src/solvers/smt/smt_conv.cpp
+++ b/src/solvers/smt/smt_conv.cpp
@@ -346,7 +346,6 @@ smt_astt smt_convt::convert_ast(const expr2tc &expr)
   case expr2t::constant_intheap_id:
   case expr2t::constant_intloc_id:
   case expr2t::heap_region_id:
-  case expr2t::flagof_id:
   case expr2t::locationof_id:
   case expr2t::fieldof_id:
   case expr2t::points_to_id:
diff --git a/src/solvers/z3-slhv/z3_slhv_conv.cpp b/src/solvers/z3-slhv/z3_slhv_conv.cpp
index 8df266bc..1c0d97db 100644
--- a/src/solvers/z3-slhv/z3_slhv_conv.cpp
+++ b/src/solvers/z3-slhv/z3_slhv_conv.cpp
@@ -237,36 +237,12 @@ z3_slhv_convt::convert_slhv_opts(
       }
       return pt_vec.size() == 1 ? pt_vec[0] : mk_uplus(pt_vec);
     }
-    case expr2t::flagof_id:
-    {
-      const flagof2t &flagof = to_flagof2t(expr);
-
-      if (is_symbol2t(flagof.source_heap))
-      {
-        if (!is_intheap_type(flagof.source_heap->type))
-        {
-          log_error("Wrong intheap type");
-          abort();
-        }
-        return args[0];
-      }
-
-      if (!is_heap_region2t(flagof.source_heap))
-      {
-        log_error("We can't get a location of a non-region heap");
-        abort();
-      }
-      return convert_ast(to_heap_region2t(flagof.source_heap).flag);
-    }
     case expr2t::locationof_id:
     {
       const locationof2t &locof = to_locationof2t(expr);
-      if (!is_heap_region2t(locof.source_heap))
-      {
-        log_error("We can't get a location of a non-region heap");
-        abort();
-      }
-      return convert_ast(to_heap_region2t(locof.source_heap).source_location);
+      const expr2tc &heap_region = locof.source_heap;
+      const intheap_type2t &_type = to_intheap_type(heap_region->type);
+      return convert_ast(_type.location);
     }
     case expr2t::points_to_id:
     {
@@ -354,24 +330,18 @@ z3_slhv_convt::convert_opt_without_assert(const expr2tc &expr)
           mk_smt_bool(true),
           mk_fresh(convert_sort(fieldof.type), mk_fresh_name("invalid_loc_")));
 
-      if (!is_heap_region2t(fieldof.source_heap))
-      {
-        log_error("We can't get a location of a non-region heap");
-        abort();
-      }
       if (!is_constant_int2t(fieldof.operand))
       {
         log_error("Wrong field");
         abort();
       }
 
-      const heap_region2t &heap_region = to_heap_region2t(fieldof.source_heap);
-      const intheap_type2t &_type = to_intheap_type(heap_region.type);
+      const expr2tc &heap_region = fieldof.source_heap;
+      const intheap_type2t &_type = to_intheap_type(heap_region->type);
       const expr2tc &field = fieldof.operand;
-
       unsigned int _field = to_constant_int2t(field).value.to_uint64();
 
-      smt_astt source_loc = convert_ast(heap_region.source_location);
+      smt_astt source_loc = convert_ast(_type.location);
       smt_astt loc = _field == 0 ?
         source_loc : mk_locadd(source_loc, convert_ast(field));
 
@@ -390,31 +360,27 @@ z3_slhv_convt::convert_opt_without_assert(const expr2tc &expr)
       }
       smt_astt v1 = mk_fresh(s1, name);
 
-      smt_astt assert_expr = mk_subh(mk_pt(loc, v1), convert_ast(heap_region.flag));
+      smt_astt assert_expr = mk_subh(mk_pt(loc, v1), convert_ast(heap_region));
       return std::make_pair(assert_expr, v1);
     }
     case expr2t::heap_update_id:
     {
       const heap_update2t &heap_upd = to_heap_update2t(expr);
-      if (!is_heap_region2t(heap_upd.source_heap))
-      {
-        log_error("Do not support heap update for other heap terms");
-        abort();
-      }
       if (!is_constant_int2t(heap_upd.operand_1))
       {
         log_error("Wrong field");
         abort();
       }
 
-      const heap_region2t &heap_region = to_heap_region2t(heap_upd.source_heap);
+      const expr2tc &heap_region = heap_upd.source_heap;
+      const intheap_type2t &_type = to_intheap_type(heap_region->type);
       const expr2tc &upd_field = heap_upd.operand_1;
       const expr2tc &upd_value = heap_upd.operand_2;
 
       unsigned int _field = to_constant_int2t(upd_field).value.to_uint64();
 
-      smt_astt h = convert_ast(heap_region.flag);
-      smt_astt source_loc = convert_ast(heap_region.source_location);
+      smt_astt h = convert_ast(heap_region);
+      smt_astt source_loc = convert_ast(_type.location);
       smt_astt field = convert_ast(upd_field);
       smt_astt loc = _field == 0 ? source_loc : mk_locadd(source_loc, field);
       smt_astt val = convert_ast(upd_value);
@@ -452,11 +418,14 @@ z3_slhv_convt::smt_ast_pair
 z3_slhv_convt::project(const expr2tc &expr)
 {
   if (is_symbol2t(expr))
+  {
+    if (is_intheap_type(expr))
+    {
+      const intheap_type2t &_type = to_intheap_type(expr->type);
+      return this->project(_type.location);
+    }
     return convert_opt_without_assert(expr);
-  else if (is_heap_region2t(expr))
-    return this->project(to_heap_region2t(expr).source_location);
-  else if (is_flagof2t(expr))
-    return this->project(to_flagof2t(expr).source_heap);
+  }
   else if (is_locationof2t(expr))
     return this->project(to_locationof2t(expr).source_heap);
   else if (is_fieldof2t(expr))
diff --git a/src/util/c_types.cpp b/src/util/c_types.cpp
index 51183b95..adb768c0 100644
--- a/src/util/c_types.cpp
+++ b/src/util/c_types.cpp
@@ -396,8 +396,7 @@ type2tc get_empty_type()
 
 type2tc get_intheap_type(unsigned int sz)
 {
-  std::vector<type2tc> field_types;
-  return intheap_type2tc(field_types, sz, sz != 0, false);
+  return intheap_type2tc(expr2tc(), sz, sz != 0, false);
 }
 
 type2tc get_intloc_type() {
diff --git a/src/util/migrate.cpp b/src/util/migrate.cpp
index 56a54f74..f486183d 100644
--- a/src/util/migrate.cpp
+++ b/src/util/migrate.cpp
@@ -2644,14 +2644,6 @@ exprt migrate_expr_back(const expr2tc &ref)
     region.copy_to_operands(migrate_expr_back(ref2.source_location));
     return region;
   }
-  case expr2t::flagof_id:
-  {
-    const flagof2t &ref2 = to_flagof2t(ref);
-    typet thetype = migrate_type_back(ref->type);
-    exprt flagof("flagof", thetype);
-    flagof.copy_to_operands(migrate_expr_back(ref2.source_heap));
-    return flagof;
-  }
   case expr2t::locationof_id:
   {
     const locationof2t &ref2 = to_locationof2t(ref);
diff --git a/src/util/type_byte_size.cpp b/src/util/type_byte_size.cpp
index 0d5be611..14a7eaa4 100644
--- a/src/util/type_byte_size.cpp
+++ b/src/util/type_byte_size.cpp
@@ -453,9 +453,6 @@ const expr2tc &get_base_object(const expr2tc &expr)
 
   if (is_dereference2t(expr))
     return get_base_object(to_dereference2t(expr).value);
-
-  if (is_flagof2t(expr))
-    return get_base_object(to_flagof2t(expr).source_heap);
   
   if (is_locationof2t(expr))
     return get_base_object(to_locationof2t(expr).source_heap);