diff --git a/src/analyses/invariant_set.cpp b/src/analyses/invariant_set.cpp
index 0ade67e810c..59bf88ca8e1 100644
--- a/src/analyses/invariant_set.cpp
+++ b/src/analyses/invariant_set.cpp
@@ -1104,10 +1104,6 @@ void invariant_sett::apply_code(const codet &code)
   {
     // does nothing
   }
-  else if(statement==ID_free)
-  {
-    // does nothing
-  }
   else if(statement==ID_printf)
   {
     // does nothing
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index 96090faf7f2..c5afebfb5db 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -2996,9 +2996,6 @@ std::string expr2ct::convert_code(
   if(statement==ID_switch_case)
     return convert_code_switch_case(to_code_switch_case(src), indent);
 
-  if(statement==ID_free)
-    return convert_code_free(src, indent);
-
   if(statement==ID_array_set)
     return convert_code_array_set(src, indent);
 
@@ -3028,19 +3025,6 @@ std::string expr2ct::convert_code_assign(
   return dest;
 }
 
-std::string expr2ct::convert_code_free(
-  const codet &src,
-  unsigned indent)
-{
-  if(src.operands().size()!=1)
-  {
-    unsigned precedence;
-    return convert_norep(src, precedence);
-  }
-
-  return indent_str(indent)+"FREE("+convert(src.op0())+");";
-}
-
 std::string expr2ct::convert_code_lock(
   const codet &src,
   unsigned indent)
diff --git a/src/ansi-c/expr2c_class.h b/src/ansi-c/expr2c_class.h
index eb01413eff4..97ff70f1298 100644
--- a/src/ansi-c/expr2c_class.h
+++ b/src/ansi-c/expr2c_class.h
@@ -187,7 +187,6 @@ class expr2ct
   std::string convert_code_switch_case(const code_switch_caset &src, unsigned indent);
   std::string convert_code_asm(const code_asmt &src, unsigned indent);
   std::string convert_code_assign(const code_assignt &src, unsigned indent);
-  std::string convert_code_free(const codet &src, unsigned indent);
   // NOLINTNEXTLINE(whitespace/line_length)
   std::string convert_code_ifthenelse(const code_ifthenelset &src, unsigned indent);
   std::string convert_code_for(const code_fort &src, unsigned indent);
diff --git a/src/goto-programs/wp.cpp b/src/goto-programs/wp.cpp
index 8c44985bbf8..e3babd9ba62 100644
--- a/src/goto-programs/wp.cpp
+++ b/src/goto-programs/wp.cpp
@@ -259,8 +259,6 @@ exprt wp(
     return post;
   else if(statement==ID_printf)
     return post; // ignored
-  else if(statement==ID_free)
-    return post; // ignored
   else if(statement==ID_asm)
     return post; // ignored
   else if(statement==ID_fence)
diff --git a/src/goto-symex/symex_other.cpp b/src/goto-symex/symex_other.cpp
index 47a5603a88d..fdc56c43fa1 100644
--- a/src/goto-symex/symex_other.cpp
+++ b/src/goto-symex/symex_other.cpp
@@ -94,10 +94,6 @@ void goto_symext::symex_other(
     clean_expr(clean_code, state, false);
     symex_cpp_delete(state, clean_code);
   }
-  else if(statement==ID_free)
-  {
-    // ignore
-  }
   else if(statement==ID_printf)
   {
     codet clean_code=code;
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
index ea91de3e959..9c9ffc9ac40 100644
--- a/src/pointer-analysis/value_set.cpp
+++ b/src/pointer-analysis/value_set.cpp
@@ -1269,86 +1269,6 @@ void value_sett::assign(
   }
 }
 
-void value_sett::do_free(
-  const exprt &op,
-  const namespacet &ns)
-{
-  // op must be a pointer
-  if(op.type().id()!=ID_pointer)
-    throw "free expected to have pointer-type operand";
-
-  // find out what it points to
-  object_mapt value_set;
-  get_value_set(op, value_set, ns, false);
-
-  const object_map_dt &object_map=value_set.read();
-
-  // find out which *instances* interest us
-  dynamic_object_id_sett to_mark;
-
-  for(object_map_dt::const_iterator
-      it=object_map.begin();
-      it!=object_map.end();
-      it++)
-  {
-    const exprt &object=object_numbering[it->first];
-
-    if(object.id()==ID_dynamic_object)
-    {
-      const dynamic_object_exprt &dynamic_object=
-        to_dynamic_object_expr(object);
-
-      if(dynamic_object.valid().is_true())
-        to_mark.insert(dynamic_object.get_instance());
-    }
-  }
-
-  // mark these as 'may be invalid'
-  // this, unfortunately, destroys the sharing
-  for(valuest::iterator v_it=values.begin();
-      v_it!=values.end();
-      v_it++)
-  {
-    object_mapt new_object_map;
-
-    const object_map_dt &old_object_map=
-      v_it->second.object_map.read();
-
-    bool changed=false;
-
-    for(object_map_dt::const_iterator
-        o_it=old_object_map.begin();
-        o_it!=old_object_map.end();
-        o_it++)
-    {
-      const exprt &object=object_numbering[o_it->first];
-
-      if(object.id()==ID_dynamic_object)
-      {
-        const dynamic_object_exprt &dynamic_object=
-          to_dynamic_object_expr(object);
-
-        if(to_mark.count(dynamic_object.get_instance())==0)
-          set(new_object_map, *o_it);
-        else
-        {
-          // adjust
-          offsett o = o_it->second;
-          exprt tmp(object);
-          to_dynamic_object_expr(tmp).valid()=exprt(ID_unknown);
-          insert(new_object_map, tmp, o);
-          changed=true;
-        }
-      }
-      else
-        set(new_object_map, *o_it);
-    }
-
-    if(changed)
-      v_it->second.object_map=new_object_map;
-  }
-}
-
 void value_sett::assign_rec(
   const exprt &lhs,
   const object_mapt &values_rhs,
@@ -1605,15 +1525,6 @@ void value_sett::apply_code_rec(
   {
     // does nothing
   }
-  else if(statement==ID_free)
-  {
-    // this may kill a valid bit
-
-    if(code.operands().size()!=1)
-      throw "free expected to have one operand";
-
-    do_free(code.op0(), ns);
-  }
   else if(statement=="lock" || statement=="unlock")
   {
     // ignore for now
diff --git a/src/pointer-analysis/value_set.h b/src/pointer-analysis/value_set.h
index c12d33bfa79..635c6b1345c 100644
--- a/src/pointer-analysis/value_set.h
+++ b/src/pointer-analysis/value_set.h
@@ -484,13 +484,6 @@ class value_sett
     const exprt &src,
     exprt &dest) const;
 
-  /// Marks objects that may be pointed to by `op` as maybe-invalid
-  /// \param op: pointer to invalidate
-  /// \param ns: global namespace
-  void do_free(
-    const exprt &op,
-    const namespacet &ns);
-
   /// Extracts a member from a struct- or union-typed expression.
   /// Usually that means making a `member_exprt`, but this can shortcut
   /// extracting members from constants or with-expressions.
diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp
index bcb92739829..b00a4e937c4 100644
--- a/src/pointer-analysis/value_set_fi.cpp
+++ b/src/pointer-analysis/value_set_fi.cpp
@@ -1115,83 +1115,6 @@ void value_set_fit::assign(
   }
 }
 
-void value_set_fit::do_free(
-  const exprt &op,
-  const namespacet &ns)
-{
-  // op must be a pointer
-  if(op.type().id()!=ID_pointer)
-    throw "free expected to have pointer-type operand";
-
-  // find out what it points to
-  object_mapt value_set;
-  get_value_set(op, value_set, ns);
-  entryt e; e.identifier="VP:TEMP";
-  e.object_map = value_set;
-  flatten(e, value_set);
-
-  const object_map_dt &object_map=value_set.read();
-
-  // find out which *instances* interest us
-  dynamic_object_id_sett to_mark;
-
-  forall_objects(it, object_map)
-  {
-    const exprt &object=object_numbering[it->first];
-
-    if(object.id()==ID_dynamic_object)
-    {
-      const dynamic_object_exprt &dynamic_object=
-        to_dynamic_object_expr(object);
-
-      if(dynamic_object.valid().is_true())
-        to_mark.insert(dynamic_object.get_instance());
-    }
-  }
-
-  // mark these as 'may be invalid'
-  // this, unfortunately, destroys the sharing
-  for(valuest::iterator v_it=values.begin();
-      v_it!=values.end();
-      v_it++)
-  {
-    object_mapt new_object_map;
-
-    const object_map_dt &old_object_map=
-      v_it->second.object_map.read();
-
-    bool changed=false;
-
-    forall_objects(o_it, old_object_map)
-    {
-      const exprt &object=object_numbering[o_it->first];
-
-      if(object.id()==ID_dynamic_object)
-      {
-        const dynamic_object_exprt &dynamic_object=
-          to_dynamic_object_expr(object);
-
-        if(to_mark.count(dynamic_object.get_instance())==0)
-          set(new_object_map, *o_it);
-        else
-        {
-          // adjust
-          offsett o = o_it->second;
-          exprt tmp(object);
-          to_dynamic_object_expr(tmp).valid()=exprt(ID_unknown);
-          insert(new_object_map, tmp, o);
-          changed=true;
-        }
-      }
-      else
-        set(new_object_map, *o_it);
-    }
-
-    if(changed)
-      v_it->second.object_map=new_object_map;
-  }
-}
-
 void value_set_fit::assign_rec(
   const exprt &lhs,
   const object_mapt &values_rhs,
@@ -1450,15 +1373,6 @@ void value_set_fit::apply_code(
   {
     // does nothing
   }
-  else if(statement==ID_free)
-  {
-    // this may kill a valid bit
-
-    if(code.operands().size()!=1)
-      throw "free expected to have one operand";
-
-    do_free(code.op0(), ns);
-  }
   else if(statement=="lock" || statement=="unlock")
   {
     // ignore for now
diff --git a/src/pointer-analysis/value_set_fi.h b/src/pointer-analysis/value_set_fi.h
index ea9bf8cf441..d26da2feef8 100644
--- a/src/pointer-analysis/value_set_fi.h
+++ b/src/pointer-analysis/value_set_fi.h
@@ -344,10 +344,6 @@ class value_set_fit
     const namespacet &ns,
     assign_recursion_sett &recursion_set);
 
-  void do_free(
-    const exprt &op,
-    const namespacet &ns);
-
   void flatten(const entryt &e, object_mapt &dest) const;
 
   void flatten_rec(
diff --git a/src/pointer-analysis/value_set_fivr.cpp b/src/pointer-analysis/value_set_fivr.cpp
index 1bbbd54fb08..23c0028d3ab 100644
--- a/src/pointer-analysis/value_set_fivr.cpp
+++ b/src/pointer-analysis/value_set_fivr.cpp
@@ -1224,87 +1224,6 @@ void value_set_fivrt::assign(
   }
 }
 
-void value_set_fivrt::do_free(
-  const exprt &op,
-  const namespacet &ns)
-{
-  // op must be a pointer
-  if(op.type().id()!=ID_pointer)
-    throw "free expected to have pointer-type operand";
-
-  // find out what it points to
-  object_mapt value_set;
-  get_value_set(op, value_set, ns);
-  entryt e; e.identifier="VP:TEMP";
-  e.object_map=value_set;
-  flatten(e, value_set);
-
-  const object_map_dt &object_map=value_set.read();
-
-  // find out which *instances* interest us
-  dynamic_object_id_sett to_mark;
-
-  forall_objects(it, object_map)
-  {
-    const exprt &object=object_numbering[it->first];
-
-    if(object.id()==ID_dynamic_object)
-    {
-      const dynamic_object_exprt &dynamic_object=
-        to_dynamic_object_expr(object);
-
-      if(dynamic_object.valid().is_true())
-        to_mark.insert(dynamic_object.get_instance());
-    }
-  }
-
-  // mark these as 'may be invalid'
-  // this, unfortunately, destroys the sharing
-  for(valuest::iterator v_it=values.begin();
-      v_it!=values.end();
-      v_it++)
-  {
-    object_mapt new_object_map;
-
-    const object_map_dt &old_object_map=
-      v_it->second.object_map.read();
-
-    bool changed=false;
-
-    forall_objects(o_it, old_object_map)
-    {
-      const exprt &object=object_numbering[o_it->first];
-
-      if(object.id()==ID_dynamic_object)
-      {
-        const dynamic_object_exprt &dynamic_object=
-          to_dynamic_object_expr(object);
-
-        if(to_mark.count(dynamic_object.get_instance())==0)
-          set(new_object_map, o_it);
-        else
-        {
-          // adjust
-          offsett o = o_it->second;
-          exprt tmp(object);
-          to_dynamic_object_expr(tmp).valid()=exprt(ID_unknown);
-          insert_to(new_object_map, tmp, o);
-          changed=true;
-        }
-      }
-      else
-        set(new_object_map, o_it);
-    }
-
-    if(changed)
-    {
-      entryt &temp_entry=get_temporary_entry(v_it->second.identifier,
-                                               v_it->second.suffix);
-      temp_entry.object_map=new_object_map;
-    }
-  }
-}
-
 void value_set_fivrt::assign_rec(
   const exprt &lhs,
   const object_mapt &values_rhs,
@@ -1604,15 +1523,6 @@ void value_set_fivrt::apply_code(
   {
     // does nothing
   }
-  else if(statement==ID_free)
-  {
-    // this may kill a valid bit
-
-    if(code.operands().size()!=1)
-      throw "free expected to have one operand";
-
-    do_free(code.op0(), ns);
-  }
   else if(statement=="lock" || statement=="unlock")
   {
     // ignore for now
diff --git a/src/pointer-analysis/value_set_fivr.h b/src/pointer-analysis/value_set_fivr.h
index 6c5c07ee543..49460a87805 100644
--- a/src/pointer-analysis/value_set_fivr.h
+++ b/src/pointer-analysis/value_set_fivr.h
@@ -383,10 +383,6 @@ class value_set_fivrt
     assign_recursion_sett &recursion_set,
     bool add_to_sets);
 
-  void do_free(
-    const exprt &op,
-    const namespacet &ns);
-
   void flatten(
     const entryt &e,
     object_mapt &dest) const;
diff --git a/src/pointer-analysis/value_set_fivrns.cpp b/src/pointer-analysis/value_set_fivrns.cpp
index 01382a1d0da..aed31f6ee02 100644
--- a/src/pointer-analysis/value_set_fivrns.cpp
+++ b/src/pointer-analysis/value_set_fivrns.cpp
@@ -916,84 +916,6 @@ void value_set_fivrnst::assign(
   }
 }
 
-void value_set_fivrnst::do_free(
-  const exprt &op,
-  const namespacet &ns)
-{
-  // op must be a pointer
-  if(op.type().id()!=ID_pointer)
-    throw "free expected to have pointer-type operand";
-
-  // find out what it points to
-  object_mapt value_set;
-  get_value_set(op, value_set, ns);
-
-  const object_map_dt &object_map=value_set.read();
-
-  // find out which *instances* interest us
-  dynamic_object_id_sett to_mark;
-
-  forall_objects(it, object_map)
-  {
-    const exprt &object=object_numbering[it->first];
-
-    if(object.id()==ID_dynamic_object)
-    {
-      const dynamic_object_exprt &dynamic_object=
-        to_dynamic_object_expr(object);
-
-      if(dynamic_object.valid().is_true())
-        to_mark.insert(dynamic_object.get_instance());
-    }
-  }
-
-  // mark these as 'may be invalid'
-  // this, unfortunately, destroys the sharing
-  for(valuest::iterator v_it=values.begin();
-      v_it!=values.end();
-      v_it++)
-  {
-    object_mapt new_object_map;
-
-    const object_map_dt &old_object_map=
-      v_it->second.object_map.read();
-
-    bool changed=false;
-
-    forall_valid_objects(o_it, old_object_map)
-    {
-      const exprt &object=object_numbering[o_it->first];
-
-      if(object.id()==ID_dynamic_object)
-      {
-        const dynamic_object_exprt &dynamic_object=
-          to_dynamic_object_expr(object);
-
-        if(to_mark.count(dynamic_object.get_instance())==0)
-          set(new_object_map, o_it);
-        else
-        {
-          // adjust
-          offsett o = o_it->second;
-          exprt tmp(object);
-          to_dynamic_object_expr(tmp).valid()=exprt(ID_unknown);
-          insert_to(new_object_map, tmp, o);
-          changed=true;
-        }
-      }
-      else
-        set(new_object_map, o_it);
-    }
-
-    if(changed)
-    {
-      entryt &temp_entry = get_temporary_entry(v_it->second.identifier,
-                                               v_it->second.suffix);
-      temp_entry.object_map=new_object_map;
-    }
-  }
-}
-
 void value_set_fivrnst::assign_rec(
   const exprt &lhs,
   const object_mapt &values_rhs,
@@ -1263,15 +1185,6 @@ void value_set_fivrnst::apply_code(
   {
     // does nothing
   }
-  else if(statement==ID_free)
-  {
-    // this may kill a valid bit
-
-    if(code.operands().size()!=1)
-      throw "free expected to have one operand";
-
-    do_free(code.op0(), ns);
-  }
   else if(statement=="lock" || statement=="unlock")
   {
     // ignore for now
diff --git a/src/pointer-analysis/value_set_fivrns.h b/src/pointer-analysis/value_set_fivrns.h
index c2f183c3ea3..5cfb4690e88 100644
--- a/src/pointer-analysis/value_set_fivrns.h
+++ b/src/pointer-analysis/value_set_fivrns.h
@@ -372,10 +372,6 @@ class value_set_fivrnst
     const std::string &suffix,
     const namespacet &ns,
     bool add_to_sets);
-
-  void do_free(
-    const exprt &op,
-    const namespacet &ns);
 };
 
 #endif // CPROVER_POINTER_ANALYSIS_VALUE_SET_FIVRNS_H
diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def
index 628883fa928..595096bec87 100644
--- a/src/util/irep_ids.def
+++ b/src/util/irep_ids.def
@@ -194,7 +194,6 @@ IREP_ID_TWO(C_base, #base)
 IREP_ID_ONE(destination)
 IREP_ID_ONE(main)
 IREP_ID_ONE(expression)
-IREP_ID_ONE(free)
 IREP_ID_ONE(allocate)
 IREP_ID_TWO(C_cxx_alloc_type, #cxx_alloc_type)
 IREP_ID_ONE(cpp_new)