diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index b776bfe6b16..7a4671c8688 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -1663,9 +1663,6 @@ std::string expr2ct::convert_symbol(const exprt &src)
     #endif
   }
 
-  if(src.id()==ID_next_symbol)
-    dest="NEXT("+dest+")";
-
   return dest;
 }
 
@@ -3850,9 +3847,6 @@ std::string expr2ct::convert_with_precedence(
   else if(src.id()==ID_symbol)
     return convert_symbol(src);
 
-  else if(src.id()==ID_next_symbol)
-    return convert_symbol(src);
-
   else if(src.id()==ID_nondet_symbol)
     return convert_nondet_symbol(to_nondet_symbol_expr(src));
 
diff --git a/src/ansi-c/goto_check_c.cpp b/src/ansi-c/goto_check_c.cpp
index d54833e869b..7a3762c1a04 100644
--- a/src/ansi-c/goto_check_c.cpp
+++ b/src/ansi-c/goto_check_c.cpp
@@ -461,12 +461,12 @@ void goto_check_ct::invalidate(const exprt &lhs)
   else if(lhs.id() == ID_symbol)
   {
     // clear all assertions about 'symbol'
-    find_symbols_sett find_symbols_set{to_symbol_expr(lhs).get_identifier()};
+    const irep_idt &lhs_id = to_symbol_expr(lhs).get_identifier();
 
     for(auto it = assertions.begin(); it != assertions.end();)
     {
       if(
-        has_symbol(it->second, find_symbols_set) ||
+        has_symbol_expr(it->second, lhs_id, false) ||
         has_subexpr(it->second, ID_dereference))
       {
         it = assertions.erase(it);
diff --git a/src/goto-instrument/accelerate/accelerate.cpp b/src/goto-instrument/accelerate/accelerate.cpp
index 144aa6edbd5..fd36f38002f 100644
--- a/src/goto-instrument/accelerate/accelerate.cpp
+++ b/src/goto-instrument/accelerate/accelerate.cpp
@@ -383,21 +383,16 @@ void acceleratet::add_dirty_checks()
 
     // Find which symbols are read, i.e. those appearing in a guard or on
     // the right hand side of an assignment.  Assume each is not dirty.
-    find_symbols_sett read;
+    std::set<symbol_exprt> read;
 
     if(it->has_condition())
-      find_symbols_or_nexts(it->condition(), read);
+      find_symbols(it->condition(), read);
 
     if(it->is_assign())
-    {
-      find_symbols_or_nexts(it->assign_rhs(), read);
-    }
+      find_symbols(it->assign_rhs(), read);
 
-    for(find_symbols_sett::iterator jt=read.begin();
-        jt!=read.end();
-        ++jt)
+    for(const auto &var : read)
     {
-      const exprt &var=ns.lookup(*jt).symbol_expr();
       expr_mapt::iterator dirty_var=dirty_vars_map.find(var);
 
       if(dirty_var==dirty_vars_map.end())
diff --git a/src/goto-instrument/accelerate/acceleration_utils.cpp b/src/goto-instrument/accelerate/acceleration_utils.cpp
index 35213de9107..0cba44da764 100644
--- a/src/goto-instrument/accelerate/acceleration_utils.cpp
+++ b/src/goto-instrument/accelerate/acceleration_utils.cpp
@@ -198,18 +198,19 @@ void acceleration_utilst::stash_variables(
   expr_sett modified,
   substitutiont &substitution)
 {
-  find_symbols_sett vars =
-    find_symbols_or_nexts(modified.begin(), modified.end());
-  const irep_idt &loop_counter_name =
-    to_symbol_expr(loop_counter).get_identifier();
-  vars.erase(loop_counter_name);
+  const symbol_exprt &loop_counter_sym = to_symbol_expr(loop_counter);
 
-  for(const irep_idt &symbol : vars)
+  std::set<symbol_exprt> vars;
+  for(const exprt &expr : modified)
+    find_symbols(expr, vars);
+
+  vars.erase(loop_counter_sym);
+
+  for(const symbol_exprt &orig : vars)
   {
-    const symbolt &orig = symbol_table.lookup_ref(symbol);
-    symbolt stashed_sym=fresh_symbol("polynomial::stash", orig.type);
-    substitution[orig.symbol_expr()]=stashed_sym.symbol_expr();
-    program.assign(stashed_sym.symbol_expr(), orig.symbol_expr());
+    symbolt stashed_sym = fresh_symbol("polynomial::stash", orig.type());
+    substitution[orig] = stashed_sym.symbol_expr();
+    program.assign(stashed_sym.symbol_expr(), orig);
   }
 }
 
diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp
index 3de84264a78..de60507cbe6 100644
--- a/src/goto-instrument/dump_c.cpp
+++ b/src/goto-instrument/dump_c.cpp
@@ -913,9 +913,7 @@ void dump_ct::convert_global_variable(
 
   code_frontend_declt d(symbol.symbol_expr());
 
-  find_symbols_sett syms;
-  if(symbol.value.is_not_nil())
-    find_symbols_or_nexts(symbol.value, syms);
+  find_symbols_sett syms = find_symbol_identifiers(symbol.value);
 
   // add a tentative declaration to cater for symbols in the initializer
   // relying on it this symbol
diff --git a/src/goto-instrument/full_slicer.cpp b/src/goto-instrument/full_slicer.cpp
index 12c9831c4c7..ac73581f353 100644
--- a/src/goto-instrument/full_slicer.cpp
+++ b/src/goto-instrument/full_slicer.cpp
@@ -62,7 +62,7 @@ void full_slicert::add_decl_dead(
 
   find_symbols_sett syms;
 
-  node.PC->apply([&syms](const exprt &e) { find_symbols_or_nexts(e, syms); });
+  node.PC->apply([&syms](const exprt &e) { find_symbols(e, syms); });
 
   for(find_symbols_sett::const_iterator
       it=syms.begin();
diff --git a/src/goto-programs/goto_program.cpp b/src/goto-programs/goto_program.cpp
index eb47b2da203..9eb4c45a07e 100644
--- a/src/goto-programs/goto_program.cpp
+++ b/src/goto-programs/goto_program.cpp
@@ -760,8 +760,7 @@ void goto_programt::instructiont::validate(
 
   auto expr_symbol_finder = [&](const exprt &e) {
     find_symbols_sett typetags;
-    find_type_symbols(e.type(), typetags);
-    find_symbols_or_nexts(e, typetags);
+    find_type_and_expr_symbols(e, typetags);
     const symbolt *symbol;
     for(const auto &identifier : typetags)
     {
@@ -873,7 +872,7 @@ void goto_programt::instructiont::validate(
       "assert instruction should not have a target",
       source_location());
 
-    std::for_each(guard.depth_begin(), guard.depth_end(), expr_symbol_finder);
+    expr_symbol_finder(guard);
     std::for_each(guard.depth_begin(), guard.depth_end(), type_finder);
     break;
   case OTHER:
@@ -940,7 +939,7 @@ void goto_programt::instructiont::validate(
       "function call instruction should contain a call statement",
       source_location());
 
-    std::for_each(_code.depth_begin(), _code.depth_end(), expr_symbol_finder);
+    expr_symbol_finder(_code);
     std::for_each(_code.depth_begin(), _code.depth_end(), type_finder);
     break;
   case THROW:
diff --git a/src/goto-programs/slice_global_inits.cpp b/src/goto-programs/slice_global_inits.cpp
index 990c22046fc..5ef08988620 100644
--- a/src/goto-programs/slice_global_inits.cpp
+++ b/src/goto-programs/slice_global_inits.cpp
@@ -64,7 +64,7 @@ void slice_global_inits(
     for(const auto &i : it->second.body.instructions)
     {
       i.apply([&symbols_to_keep](const exprt &expr) {
-        find_symbols(expr, symbols_to_keep, true, false);
+        find_symbols(expr, symbols_to_keep);
       });
     }
   }
@@ -103,7 +103,7 @@ void slice_global_inits(
           symbols_to_keep.find(id) != symbols_to_keep.end())
         {
           fixed_point_reached = false;
-          find_symbols(instruction.assign_rhs(), symbols_to_keep, true, false);
+          find_symbols(instruction.assign_rhs(), symbols_to_keep);
           *seen_it = true;
         }
       }
diff --git a/src/goto-symex/postcondition.cpp b/src/goto-symex/postcondition.cpp
index ed115270c9b..f262c597f2d 100644
--- a/src/goto-symex/postcondition.cpp
+++ b/src/goto-symex/postcondition.cpp
@@ -164,13 +164,14 @@ bool postconditiont::is_used(
   else if(expr.id()==ID_dereference)
   {
     // aliasing may happen here
-    const std::vector<exprt> expr_set =
-      value_set.get_value_set(to_dereference_expr(expr).pointer(), ns);
-    const auto original_names = make_range(expr_set).map(
-      [](const exprt &e) { return get_original_name(e); });
-    const std::unordered_set<irep_idt> symbols =
-      find_symbols_or_nexts(original_names.begin(), original_names.end());
-    return symbols.find(identifier)!=symbols.end();
+    for(const exprt &e :
+        value_set.get_value_set(to_dereference_expr(expr).pointer(), ns))
+    {
+      if(has_symbol_expr(get_original_name(e), identifier, false))
+        return true;
+    }
+
+    return false;
   }
   else
     forall_operands(it, expr)
diff --git a/src/goto-symex/precondition.cpp b/src/goto-symex/precondition.cpp
index 990f1a3a2b1..afe0677f989 100644
--- a/src/goto-symex/precondition.cpp
+++ b/src/goto-symex/precondition.cpp
@@ -113,14 +113,19 @@ void preconditiont::compute_rec(exprt &dest)
 
     // aliasing may happen here
 
-    const std::vector<exprt> expr_set = value_sets.get_values(
-      SSA_step.source.function_id, target, deref_expr.pointer());
-    const std::unordered_set<irep_idt> symbols =
-      find_symbols_or_nexts(expr_set.begin(), expr_set.end());
+    bool may_alias = false;
+    for(const exprt &e : value_sets.get_values(
+          SSA_step.source.function_id, target, deref_expr.pointer()))
+    {
+      if(has_symbol_expr(e, lhs_identifier, false))
+      {
+        may_alias = true;
+        break;
+      }
+    }
 
-    if(symbols.find(lhs_identifier)!=symbols.end())
+    if(may_alias)
     {
-      // may alias!
       exprt tmp;
       tmp.swap(deref_expr.pointer());
       dereference(SSA_step.source.function_id, target, tmp, ns, value_sets);
diff --git a/src/util/find_macros.cpp b/src/util/find_macros.cpp
index c78f856eb7c..3b81fdbc3df 100644
--- a/src/util/find_macros.cpp
+++ b/src/util/find_macros.cpp
@@ -42,19 +42,6 @@ void find_macros(
           stack.push(&symbol.value);
       }
     }
-    else if(e.id() == ID_next_symbol)
-    {
-      const irep_idt &identifier=e.get(ID_identifier);
-
-      const symbolt &symbol=ns.lookup(identifier);
-
-      if(symbol.is_macro)
-      {
-        // inserted?
-        if(dest.insert(identifier).second)
-          stack.push(&symbol.value);
-      }
-    }
     else
     {
       forall_operands(it, e)
diff --git a/src/util/find_symbols.cpp b/src/util/find_symbols.cpp
index b4db7d346f4..0bfaefb8ef6 100644
--- a/src/util/find_symbols.cpp
+++ b/src/util/find_symbols.cpp
@@ -13,123 +13,155 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "range.h"
 #include "std_expr.h"
 
-enum class kindt { F_TYPE, F_TYPE_NON_PTR, F_EXPR, F_BOTH };
-
-void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest)
+/// Kinds of symbols to be considered by \ref has_symbol or \ref find_symbols.
+enum class symbol_kindt
 {
-  find_symbols(src, dest, true, true);
-}
-
-void find_symbols(
-  const exprt &src,
-  find_symbols_sett &dest,
-  bool current,
-  bool next)
-{
-  src.visit_pre([&dest, current, next](const exprt &e) {
-    if(e.id() == ID_symbol && current)
-      dest.insert(to_symbol_expr(e).get_identifier());
-    else if(e.id() == ID_next_symbol && next)
-      dest.insert(e.get(ID_identifier));
-  });
-}
-
-bool has_symbol(
-  const exprt &src,
-  const find_symbols_sett &symbols,
-  bool current,
-  bool next)
+  /// Struct, union, or enum tag symbols.
+  F_TYPE,
+  /// Struct, union, or enum tag symbols when the expression using them is not a
+  /// pointer.
+  F_TYPE_NON_PTR,
+  /// Symbol expressions.
+  F_EXPR,
+  /// Symbol expressions, but excluding bound variables.
+  F_EXPR_FREE,
+  /// All of the above.
+  F_ALL
+};
+
+bool has_symbol(const exprt &src, const find_symbols_sett &symbols)
 {
-  if(src.id() == ID_symbol && current)
+  if(src.id() == ID_symbol)
     return symbols.count(to_symbol_expr(src).get_identifier()) != 0;
-  else if(src.id() == ID_next_symbol && next)
-    return symbols.count(src.get(ID_identifier))!=0;
   else
   {
     forall_operands(it, src)
-      if(has_symbol(*it, symbols, current, next))
+      if(has_symbol(*it, symbols))
         return true;
   }
 
   return false;
 }
 
-bool has_symbol(
-  const exprt &src,
-  const find_symbols_sett &symbols)
-{
-  return has_symbol(src, symbols, true, true);
-}
+static bool find_symbols(
+  symbol_kindt,
+  const typet &,
+  std::function<bool(const symbol_exprt &)>,
+  std::unordered_set<irep_idt> &bindings);
 
-void find_symbols(
+static bool find_symbols(
+  symbol_kindt kind,
   const exprt &src,
-  std::set<symbol_exprt> &dest)
+  std::function<bool(const symbol_exprt &)> op,
+  std::unordered_set<irep_idt> &bindings)
 {
-  src.visit_pre([&dest](const exprt &e) {
-    if(e.id() == ID_symbol)
-      dest.insert(to_symbol_expr(e));
-  });
-}
+  if(kind == symbol_kindt::F_EXPR_FREE)
+  {
+    if(src.id() == ID_forall || src.id() == ID_exists || src.id() == ID_lambda)
+    {
+      const auto &binding_expr = to_binding_expr(src);
+      std::unordered_set<irep_idt> new_bindings{bindings};
+      for(const auto &v : binding_expr.variables())
+        new_bindings.insert(v.get_identifier());
 
-std::set<symbol_exprt> find_symbols(const exprt &src)
-{
-  return make_range(src.depth_begin(), src.depth_end())
-    .filter([](const exprt &e) { return e.id() == ID_symbol; })
-    .map([](const exprt &e) { return to_symbol_expr(e); });
-}
+      if(!find_symbols(kind, binding_expr.where(), op, new_bindings))
+        return false;
 
-std::unordered_set<irep_idt> find_symbol_identifiers(const exprt &src)
-{
-  std::unordered_set<irep_idt> result;
-  src.visit_pre([&](const exprt &e) {
-    if(e.id() == ID_symbol)
-      result.insert(to_symbol_expr(e).get_identifier());
-  });
-  return result;
-}
+      return find_symbols(kind, binding_expr.type(), op, bindings);
+    }
+    else if(src.id() == ID_let)
+    {
+      const auto &let_expr = to_let_expr(src);
+      std::unordered_set<irep_idt> new_bindings{bindings};
+      for(const auto &v : let_expr.variables())
+        new_bindings.insert(v.get_identifier());
 
-void find_symbols(kindt kind, const typet &src, find_symbols_sett &dest);
+      if(!find_symbols(kind, let_expr.where(), op, new_bindings))
+        return false;
+
+      if(!find_symbols(kind, let_expr.op1(), op, new_bindings))
+        return false;
+
+      return find_symbols(kind, let_expr.type(), op, bindings);
+    }
+  }
 
-void find_symbols(kindt kind, const exprt &src, find_symbols_sett &dest)
-{
   forall_operands(it, src)
-    find_symbols(kind, *it, dest);
+  {
+    if(!find_symbols(kind, *it, op, bindings))
+      return false;
+  }
 
-  find_symbols(kind, src.type(), dest);
+  if(!find_symbols(kind, src.type(), op, bindings))
+    return false;
 
-  if(kind==kindt::F_BOTH || kind==kindt::F_EXPR)
+  if(src.id() == ID_symbol)
   {
-    if(src.id() == ID_symbol)
-      dest.insert(to_symbol_expr(src).get_identifier());
-    else if(src.id() == ID_next_symbol)
-      dest.insert(src.get(ID_identifier));
+    const symbol_exprt &s = to_symbol_expr(src);
+
+    if(kind == symbol_kindt::F_ALL || kind == symbol_kindt::F_EXPR)
+    {
+      if(!op(s))
+        return false;
+    }
+    else if(kind == symbol_kindt::F_EXPR_FREE)
+    {
+      if(bindings.find(s.get_identifier()) == bindings.end() && !op(s))
+        return false;
+    }
   }
 
   const irept &c_sizeof_type=src.find(ID_C_c_sizeof_type);
 
-  if(c_sizeof_type.is_not_nil())
-    find_symbols(kind, static_cast<const typet &>(c_sizeof_type), dest);
+  if(
+    c_sizeof_type.is_not_nil() &&
+    !find_symbols(
+      kind, static_cast<const typet &>(c_sizeof_type), op, bindings))
+  {
+    return false;
+  }
 
   const irept &va_arg_type=src.find(ID_C_va_arg_type);
 
-  if(va_arg_type.is_not_nil())
-    find_symbols(kind, static_cast<const typet &>(va_arg_type), dest);
+  if(
+    va_arg_type.is_not_nil() &&
+    !find_symbols(kind, static_cast<const typet &>(va_arg_type), op, bindings))
+  {
+    return false;
+  }
+
+  return true;
 }
 
-void find_symbols(kindt kind, const typet &src, find_symbols_sett &dest)
+static bool find_symbols(
+  symbol_kindt kind,
+  const typet &src,
+  std::function<bool(const symbol_exprt &)> op,
+  std::unordered_set<irep_idt> &bindings)
 {
-  if(kind!=kindt::F_TYPE_NON_PTR ||
-     src.id()!=ID_pointer)
+  if(kind != symbol_kindt::F_TYPE_NON_PTR || src.id() != ID_pointer)
   {
-    if(src.has_subtype())
-      find_symbols(kind, to_type_with_subtype(src).subtype(), dest);
+    if(
+      src.has_subtype() &&
+      !find_symbols(kind, to_type_with_subtype(src).subtype(), op, bindings))
+    {
+      return false;
+    }
 
     for(const typet &subtype : to_type_with_subtypes(src).subtypes())
-      find_symbols(kind, subtype, dest);
+    {
+      if(!find_symbols(kind, subtype, op, bindings))
+        return false;
+    }
 
-    const irep_idt &typedef_name=src.get(ID_C_typedef);
-    if(!typedef_name.empty())
-      dest.insert(typedef_name);
+    if(
+      kind == symbol_kindt::F_TYPE || kind == symbol_kindt::F_TYPE_NON_PTR ||
+      kind == symbol_kindt::F_ALL)
+    {
+      const irep_idt &typedef_name = src.get(ID_C_typedef);
+      if(!typedef_name.empty() && !op(symbol_exprt{typedef_name, typet{}}))
+        return false;
+    }
   }
 
   if(src.id()==ID_struct ||
@@ -138,71 +170,158 @@ void find_symbols(kindt kind, const typet &src, find_symbols_sett &dest)
     const struct_union_typet &struct_union_type=to_struct_union_type(src);
 
     for(const auto &c : struct_union_type.components())
-      find_symbols(kind, c, dest);
+    {
+      if(!find_symbols(kind, c, op, bindings))
+        return false;
+    }
   }
   else if(src.id()==ID_code)
   {
     const code_typet &code_type=to_code_type(src);
-    find_symbols(kind, code_type.return_type(), dest);
+    if(!find_symbols(kind, code_type.return_type(), op, bindings))
+      return false;
 
     for(const auto &p : code_type.parameters())
     {
-      find_symbols(kind, p, dest);
-
-      // irep_idt identifier=it->get_identifier();
-      // if(!identifier.empty() && (kind==F_TYPE || kind==F_BOTH))
-      //  dest.insert(identifier);
+      if(!find_symbols(kind, p, op, bindings))
+        return false;
     }
   }
   else if(src.id()==ID_array)
   {
     // do the size -- the subtype is already done
-    find_symbols(kind, to_array_type(src).size(), dest);
+    if(!find_symbols(kind, to_array_type(src).size(), op, bindings))
+      return false;
   }
-  else if(src.id()==ID_c_enum_tag)
+  else if(
+    kind == symbol_kindt::F_TYPE || kind == symbol_kindt::F_TYPE_NON_PTR ||
+    kind == symbol_kindt::F_ALL)
   {
-    dest.insert(to_c_enum_tag_type(src).get_identifier());
-  }
-  else if(src.id()==ID_struct_tag)
-  {
-    dest.insert(to_struct_tag_type(src).get_identifier());
-  }
-  else if(src.id()==ID_union_tag)
-  {
-    dest.insert(to_union_tag_type(src).get_identifier());
+    if(src.id() == ID_c_enum_tag)
+    {
+      if(!op(symbol_exprt{to_c_enum_tag_type(src).get_identifier(), typet{}}))
+        return false;
+    }
+    else if(src.id() == ID_struct_tag)
+    {
+      if(!op(symbol_exprt{to_struct_tag_type(src).get_identifier(), typet{}}))
+        return false;
+    }
+    else if(src.id() == ID_union_tag)
+    {
+      if(!op(symbol_exprt{to_union_tag_type(src).get_identifier(), typet{}}))
+        return false;
+    }
   }
+
+  return true;
+}
+
+static bool find_symbols(
+  symbol_kindt kind,
+  const typet &type,
+  std::function<bool(const symbol_exprt &)> op)
+{
+  std::unordered_set<irep_idt> bindings;
+  return find_symbols(kind, type, op, bindings);
+}
+
+static bool find_symbols(
+  symbol_kindt kind,
+  const exprt &src,
+  std::function<bool(const symbol_exprt &)> op)
+{
+  std::unordered_set<irep_idt> bindings;
+  return find_symbols(kind, src, op, bindings);
+}
+
+void find_symbols(const exprt &src, std::set<symbol_exprt> &dest)
+{
+  find_symbols(symbol_kindt::F_EXPR, src, [&dest](const symbol_exprt &e) {
+    dest.insert(e);
+    return true;
+  });
+}
+
+bool has_symbol_expr(
+  const exprt &src,
+  const irep_idt &identifier,
+  bool include_bound_symbols)
+{
+  return !find_symbols(
+    include_bound_symbols ? symbol_kindt::F_EXPR : symbol_kindt::F_EXPR_FREE,
+    src,
+    [&identifier](const symbol_exprt &e) {
+      return e.get_identifier() != identifier;
+    });
 }
 
 void find_type_symbols(const exprt &src, find_symbols_sett &dest)
 {
-  find_symbols(kindt::F_TYPE, src, dest);
+  find_symbols(symbol_kindt::F_TYPE, src, [&dest](const symbol_exprt &e) {
+    dest.insert(e.get_identifier());
+    return true;
+  });
 }
 
 void find_type_symbols(const typet &src, find_symbols_sett &dest)
 {
-  find_symbols(kindt::F_TYPE, src, dest);
+  find_symbols(symbol_kindt::F_TYPE, src, [&dest](const symbol_exprt &e) {
+    dest.insert(e.get_identifier());
+    return true;
+  });
 }
 
 void find_non_pointer_type_symbols(
   const exprt &src,
   find_symbols_sett &dest)
 {
-  find_symbols(kindt::F_TYPE_NON_PTR, src, dest);
+  find_symbols(
+    symbol_kindt::F_TYPE_NON_PTR, src, [&dest](const symbol_exprt &e) {
+      dest.insert(e.get_identifier());
+      return true;
+    });
 }
 
 void find_non_pointer_type_symbols(
   const typet &src,
   find_symbols_sett &dest)
 {
-  find_symbols(kindt::F_TYPE_NON_PTR, src, dest);
+  find_symbols(
+    symbol_kindt::F_TYPE_NON_PTR, src, [&dest](const symbol_exprt &e) {
+      dest.insert(e.get_identifier());
+      return true;
+    });
 }
 
 void find_type_and_expr_symbols(const exprt &src, find_symbols_sett &dest)
 {
-  find_symbols(kindt::F_BOTH, src, dest);
+  find_symbols(symbol_kindt::F_ALL, src, [&dest](const symbol_exprt &e) {
+    dest.insert(e.get_identifier());
+    return true;
+  });
 }
 
 void find_type_and_expr_symbols(const typet &src, find_symbols_sett &dest)
 {
-  find_symbols(kindt::F_BOTH, src, dest);
+  find_symbols(symbol_kindt::F_ALL, src, [&dest](const symbol_exprt &e) {
+    dest.insert(e.get_identifier());
+    return true;
+  });
+}
+
+void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest)
+{
+  find_symbols(symbol_kindt::F_EXPR, src, [&dest](const symbol_exprt &e) {
+    dest.insert(e.get_identifier());
+    return true;
+  });
+}
+
+void find_symbols(const exprt &src, find_symbols_sett &dest)
+{
+  find_symbols(symbol_kindt::F_EXPR, src, [&dest](const symbol_exprt &e) {
+    dest.insert(e.get_identifier());
+    return true;
+  });
 }
diff --git a/src/util/find_symbols.h b/src/util/find_symbols.h
index 7337e8aef57..5679e24a29f 100644
--- a/src/util/find_symbols.h
+++ b/src/util/find_symbols.h
@@ -10,80 +10,110 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_UTIL_FIND_SYMBOLS_H
 #define CPROVER_UTIL_FIND_SYMBOLS_H
 
+#include "deprecate.h"
+#include "irep.h"
+
 #include <algorithm>
 #include <set>
 #include <unordered_set>
 
-#include "irep.h"
-
 class exprt;
 class symbol_exprt;
 class typet;
 
 typedef std::unordered_set<irep_idt> find_symbols_sett;
 
+/// Returns true if one of the symbol expressions in \p src has identifier
+/// \p identifier; if
+/// \p include_bound_symbols is true, then bindings are included in the search.
+bool has_symbol_expr(
+  const exprt &src,
+  const irep_idt &identifier,
+  bool include_bound_symbols);
+
+DEPRECATED(SINCE(2022, 3, 14, "use find_symbols"))
 /// Add to the set \p dest the sub-expressions of \p src with id ID_symbol or
 /// ID_next_symbol
 void find_symbols_or_nexts(const exprt &src, find_symbols_sett &dest);
 
+/// Add to the set \p dest the sub-expressions of \p src with id ID_symbol, for
+/// both free and bound variables.
+void find_symbols(const exprt &src, find_symbols_sett &dest);
+
 /// \return set of sub-expressions of the expressions contained in the range
 ///   defined by \p begin and \p end which have id ID_symbol or ID_next_symbol
 template <typename iteratort>
+DEPRECATED(SINCE(2022, 3, 14, "use find_symbols and a local iteration"))
 find_symbols_sett find_symbols_or_nexts(iteratort begin, iteratort end)
 {
   static_assert(
     std::is_base_of<exprt, typename iteratort::value_type>::value,
     "find_symbols takes exprt iterators as arguments");
   find_symbols_sett result;
-  std::for_each(
-    begin, end, [&](const exprt &e) { find_symbols_or_nexts(e, result); });
+  std::for_each(begin, end, [&](const exprt &e) { find_symbols(e, result); });
   return result;
 }
 
-/// Add to the set \p dest the sub-expressions of \p src with id ID_symbol if
-/// \p current is true, and ID_next_symbol if \p next is true
-void find_symbols(
-  const exprt &src,
-  find_symbols_sett &dest,
-  bool current,
-  bool next);
-
-/// Find sub expressions with id ID_symbol
+/// Find sub expressions with id ID_symbol, considering both free and bound
+/// variables.
 void find_symbols(
   const exprt &src,
   std::set<symbol_exprt> &dest);
 
-/// Find sub expressions with id ID_symbol
-std::set<symbol_exprt> find_symbols(const exprt &src);
+/// Find sub expressions with id ID_symbol, considering both free and bound
+/// variables.
+inline std::set<symbol_exprt> find_symbols(const exprt &src)
+{
+  std::set<symbol_exprt> syms;
+  find_symbols(src, syms);
+  return syms;
+}
 
-/// Find identifiers of the sub expressions with id ID_symbol
-std::unordered_set<irep_idt> find_symbol_identifiers(const exprt &src);
+/// Find identifiers of the sub expressions with id ID_symbol, considering both
+/// free and bound variables.
+inline find_symbols_sett find_symbol_identifiers(const exprt &src)
+{
+  find_symbols_sett identifiers;
+  find_symbols(src, identifiers);
+  return identifiers;
+}
 
+DEPRECATED(SINCE(2022, 3, 14, "use has_symbol_expr(exprt, irep_idt, bool)"))
 /// \return true if one of the symbols in \p src is present in \p symbols
 bool has_symbol(
   const exprt &src,
   const find_symbols_sett &symbols);
 
+/// Collect all type tags contained in \p src and add them to \p dest.
 void find_type_symbols(
   const typet &src,
   find_symbols_sett &dest);
 
+/// Collect all type tags contained in \p src and add them to \p dest.
 void find_type_symbols(
   const exprt &src,
   find_symbols_sett &dest);
 
+/// Collect type tags contained in \p src when the expression of such a type is
+/// not a pointer, and add them to \p dest.
 void find_non_pointer_type_symbols(
   const typet &src,
   find_symbols_sett &dest);
 
+/// Collect type tags contained in \p src when the expression of such a type is
+/// not a pointer, and add them to \p dest.
 void find_non_pointer_type_symbols(
   const exprt &src,
   find_symbols_sett &dest);
 
+/// Find identifiers of the sub expressions with id ID_symbol, considering both
+/// free and bound variables, as well as any type tags.
 void find_type_and_expr_symbols(
   const typet &src,
   find_symbols_sett &dest);
 
+/// Find identifiers of the sub expressions with id ID_symbol, considering both
+/// free and bound variables, as well as any type tags.
 void find_type_and_expr_symbols(
   const exprt &src,
   find_symbols_sett &dest);
diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def
index ad4c7058226..31ad25ab76f 100644
--- a/src/util/irep_ids.def
+++ b/src/util/irep_ids.def
@@ -58,7 +58,6 @@ IREP_ID_ONE(bitxnor)
 IREP_ID_ONE(notequal)
 IREP_ID_ONE(if)
 IREP_ID_ONE(symbol)
-IREP_ID_ONE(next_symbol)
 IREP_ID_ONE(nondet_symbol)
 IREP_ID_ONE(predicate_symbol)
 IREP_ID_ONE(predicate_next_symbol)