diff --git a/src/analyses/invariant_propagation.cpp b/src/analyses/invariant_propagation.cpp
index 97211760f52..02d3ec36b17 100644
--- a/src/analyses/invariant_propagation.cpp
+++ b/src/analyses/invariant_propagation.cpp
@@ -178,10 +178,13 @@ void invariant_propagationt::get_globals(
   object_listt &dest)
 {
   // static ones
-  forall_symbols(it, ns.get_symbol_table().symbols)
-    if(it->second.is_lvalue &&
-       it->second.is_static_lifetime)
-      get_objects(it->second, dest);
+  for(const auto &symbol_pair : ns.get_symbol_table().symbols)
+  {
+    if(symbol_pair.second.is_lvalue && symbol_pair.second.is_static_lifetime)
+    {
+      get_objects(symbol_pair.second, dest);
+    }
+  }
 }
 
 bool invariant_propagationt::check_type(const typet &type) const
diff --git a/src/goto-instrument/alignment_checks.cpp b/src/goto-instrument/alignment_checks.cpp
index 3a177bdcd28..68c173bda7a 100644
--- a/src/goto-instrument/alignment_checks.cpp
+++ b/src/goto-instrument/alignment_checks.cpp
@@ -19,21 +19,21 @@ void print_struct_alignment_problems(
   const symbol_tablet &symbol_table,
   std::ostream &out)
 {
-  forall_symbols(it, symbol_table.symbols)
-    if(it->second.is_type && it->second.type.id()==ID_struct)
+  for(const auto &symbol_pair : symbol_table.symbols)
+  {
+    if(symbol_pair.second.is_type && symbol_pair.second.type.id() == ID_struct)
     {
-      const struct_typet &str=to_struct_type(it->second.type);
-      const struct_typet::componentst &components=str.components();
+      const struct_typet &str = to_struct_type(symbol_pair.second.type);
+      const struct_typet::componentst &components = str.components();
 
-      bool first_time_seen_in_struct=true;
+      bool first_time_seen_in_struct = true;
 
-      for(struct_typet::componentst::const_iterator
-          it_mem=components.begin();
-          it_mem!=components.end();
+      for(struct_typet::componentst::const_iterator it_mem = components.begin();
+          it_mem != components.end();
           it_mem++)
       {
-        mp_integer cumulated_length=0;
-        bool first_time_seen_from=true;
+        mp_integer cumulated_length = 0;
+        bool first_time_seen_from = true;
 
         // if the instruction cannot be aligned to the address,
         // try the next one
@@ -42,40 +42,39 @@ void print_struct_alignment_problems(
           // || alignment(it_mem->type())%config.ansi_c.alignment!=0)
           continue;
 
-        for(struct_typet::componentst::const_iterator
-            it_next=it_mem;
-            it_next!=components.end();
+        for(struct_typet::componentst::const_iterator it_next = it_mem;
+            it_next != components.end();
             it_next++)
         {
-          const typet &it_type=it_next->type();
+          const typet &it_type = it_next->type();
           const namespacet ns(symbol_table);
-          mp_integer size=pointer_offset_size(it_type, ns);
+          mp_integer size = pointer_offset_size(it_type, ns);
 
-          if(size<0)
-            throw "type of unknown size:\n"+it_type.pretty();
+          if(size < 0)
+            throw "type of unknown size:\n" + it_type.pretty();
 
-          cumulated_length+=size;
+          cumulated_length += size;
           // [it_mem;it_next] cannot be covered by an instruction
-          if(cumulated_length>config.ansi_c.memory_operand_size)
+          if(cumulated_length > config.ansi_c.memory_operand_size)
           {
             // if interferences have been found, no need to check with
             // starting from an already covered member
             if(!first_time_seen_from)
-              it_mem=it_next-1;
+              it_mem = it_next - 1;
             break;
           }
 
-          if(it_mem!=it_next && !it_next->get_is_padding())
+          if(it_mem != it_next && !it_next->get_is_padding())
           {
             if(first_time_seen_in_struct)
             {
-              first_time_seen_in_struct=false;
-              first_time_seen_from=false;
+              first_time_seen_in_struct = false;
+              first_time_seen_from = false;
 
               out << "\nWARNING: "
                   << "declaration of structure "
-                  << str.find_type(ID_tag).pretty()
-                  << " at " << it->second.location << '\n';
+                  << str.find_type(ID_tag).pretty() << " at "
+                  << symbol_pair.second.location << '\n';
             }
 
             out << "members " << it_mem->get_pretty_name() << " and "
@@ -84,12 +83,12 @@ void print_struct_alignment_problems(
         }
       }
     }
-    else if(it->second.type.id()==ID_array)
+    else if(symbol_pair.second.type.id() == ID_array)
     {
       // is this structure likely to introduce data races?
       #if 0
       const namespacet ns(symbol_table);
-      const array_typet array=to_array_type(it->second.type);
+      const array_typet array=to_array_type(symbol_pair.second.type);
       const mp_integer size=
         pointer_offset_size(array.subtype(), ns);
 
@@ -100,9 +99,10 @@ void print_struct_alignment_problems(
       {
         out << "\nWARNING: "
             << "declaration of an array at "
-            << it->second.location <<
+            << symbol_pair.second.location <<
             << "\nmight be concurrently accessed\n";
       }
       #endif
     }
+  }
 }
diff --git a/src/goto-instrument/dump_c.cpp b/src/goto-instrument/dump_c.cpp
index c32fb2cc11a..557a8a4e99d 100644
--- a/src/goto-instrument/dump_c.cpp
+++ b/src/goto-instrument/dump_c.cpp
@@ -82,8 +82,10 @@ void dump_ct::operator()(std::ostream &os)
       }
     }
   }
-  forall_symbols(it, symbols_transparent.symbols)
-    copied_symbol_table.add(it->second);
+  for(const auto &symbol_pair : symbols_transparent.symbols)
+  {
+    copied_symbol_table.add(symbol_pair.second);
+  }
 
   typedef std::unordered_map<irep_idt, unsigned, irep_id_hash> unique_tagst;
   unique_tagst unique_tags;
diff --git a/src/goto-instrument/model_argc_argv.cpp b/src/goto-instrument/model_argc_argv.cpp
index 779bf1bfcc1..b47071a2c42 100644
--- a/src/goto-instrument/model_argc_argv.cpp
+++ b/src/goto-instrument/model_argc_argv.cpp
@@ -114,25 +114,27 @@ bool model_argc_argv(
   // locate the body of the newly built start function as well as any
   // additional declarations we might need; the body will then be
   // converted and inserted into the start function
-  forall_symbols(it, tmp_symbol_table.symbols)
+  for(const auto &symbol_pair : tmp_symbol_table.symbols)
   {
     // add __CPROVER_assume if necessary (it might exist already)
-    if(it->first==CPROVER_PREFIX "assume" ||
-       it->first==CPROVER_PREFIX "input")
-      goto_model.symbol_table.add(it->second);
-    else if(it->first==goto_model.goto_functions.entry_point())
+    if(
+      symbol_pair.first == CPROVER_PREFIX "assume" ||
+      symbol_pair.first == CPROVER_PREFIX "input")
+      goto_model.symbol_table.add(symbol_pair.second);
+    else if(symbol_pair.first == goto_model.goto_functions.entry_point())
     {
-      value=it->second.value;
+      value = symbol_pair.second.value;
 
       replace_symbolt replace;
       replace.insert("ARGC", ns.lookup("argc'").symbol_expr());
       replace.insert("ARGV", ns.lookup("argv'").symbol_expr());
       replace(value);
     }
-    else if(has_prefix(
-        id2string(it->first),
-        id2string(goto_model.goto_functions.entry_point())+"::") &&
-      goto_model.symbol_table.add(it->second))
+    else if(
+      has_prefix(
+        id2string(symbol_pair.first),
+        id2string(goto_model.goto_functions.entry_point()) + "::") &&
+      goto_model.symbol_table.add(symbol_pair.second))
       UNREACHABLE;
   }
   POSTCONDITION(value.is_not_nil());
diff --git a/src/goto-programs/class_hierarchy.cpp b/src/goto-programs/class_hierarchy.cpp
index c8ef2a1a3f3..7f0e7fe558b 100644
--- a/src/goto-programs/class_hierarchy.cpp
+++ b/src/goto-programs/class_hierarchy.cpp
@@ -24,12 +24,11 @@ Date: April 2016
 /// \param symbol_table: The symbol table to analyze
 void class_hierarchyt::operator()(const symbol_tablet &symbol_table)
 {
-  forall_symbols(it, symbol_table.symbols)
+  for(const auto &symbol_pair : symbol_table.symbols)
   {
-    if(it->second.is_type && it->second.type.id()==ID_struct)
+    if(symbol_pair.second.is_type && symbol_pair.second.type.id() == ID_struct)
     {
-      const struct_typet &struct_type=
-        to_struct_type(it->second.type);
+      const struct_typet &struct_type = to_struct_type(symbol_pair.second.type);
 
       const irept::subt &bases=
         struct_type.find(ID_bases).get_sub();
@@ -40,8 +39,8 @@ void class_hierarchyt::operator()(const symbol_tablet &symbol_table)
         if(parent.empty())
           continue;
 
-        class_map[parent].children.push_back(it->first);
-        class_map[it->first].parents.push_back(parent);
+        class_map[parent].children.push_back(symbol_pair.first);
+        class_map[symbol_pair.first].parents.push_back(parent);
       }
     }
   }
@@ -55,28 +54,31 @@ void class_hierarchyt::operator()(const symbol_tablet &symbol_table)
 void class_hierarchy_grapht::populate(const symbol_tablet &symbol_table)
 {
   // Add nodes for all classes:
-  forall_symbols(it, symbol_table.symbols)
+  for(const auto &symbol_pair : symbol_table.symbols)
   {
-    if(it->second.is_type && it->second.type.id() == ID_struct)
+    if(symbol_pair.second.is_type && symbol_pair.second.type.id() == ID_struct)
     {
       node_indext new_node_index = add_node();
-      nodes_by_name[it->first] = new_node_index;
-      (*this)[new_node_index].class_identifier = it->first;
+      nodes_by_name[symbol_pair.first] = new_node_index;
+      (*this)[new_node_index].class_identifier = symbol_pair.first;
     }
   }
 
   // Add parent -> child edges:
-  forall_symbols(it, symbol_table.symbols)
+  for(const auto &symbol_pair : symbol_table.symbols)
   {
-    if(it->second.is_type && it->second.type.id() == ID_struct)
+    if(symbol_pair.second.is_type && symbol_pair.second.type.id() == ID_struct)
     {
-      const class_typet &class_type = to_class_type(it->second.type);
+      const class_typet &class_type = to_class_type(symbol_pair.second.type);
 
       for(const auto &base : class_type.bases())
       {
         const irep_idt &parent = to_symbol_type(base.type()).get_identifier();
         if(!parent.empty())
-          add_edge(nodes_by_name.at(parent), nodes_by_name.at(it->first));
+        {
+          add_edge(
+            nodes_by_name.at(parent), nodes_by_name.at(symbol_pair.first));
+        }
       }
     }
   }
diff --git a/src/goto-programs/goto_convert_functions.cpp b/src/goto-programs/goto_convert_functions.cpp
index 1f9f49867f1..f4edab30c47 100644
--- a/src/goto-programs/goto_convert_functions.cpp
+++ b/src/goto-programs/goto_convert_functions.cpp
@@ -38,16 +38,16 @@ void goto_convert_functionst::goto_convert(goto_functionst &functions)
   typedef std::list<irep_idt> symbol_listt;
   symbol_listt symbol_list;
 
-  forall_symbols(it, symbol_table.symbols)
+  for(const auto &symbol_pair : symbol_table.symbols)
   {
-    if(!it->second.is_type &&
-       !it->second.is_macro &&
-       it->second.type.id()==ID_code &&
-       (it->second.mode==ID_C ||
-        it->second.mode==ID_cpp ||
-        it->second.mode==ID_java ||
-        it->second.mode=="jsil"))
-      symbol_list.push_back(it->first);
+    if(
+      !symbol_pair.second.is_type && !symbol_pair.second.is_macro &&
+      symbol_pair.second.type.id() == ID_code &&
+      (symbol_pair.second.mode == ID_C || symbol_pair.second.mode == ID_cpp ||
+       symbol_pair.second.mode == ID_java || symbol_pair.second.mode == "jsil"))
+    {
+      symbol_list.push_back(symbol_pair.first);
+    }
   }
 
   for(const auto &id : symbol_list)
@@ -59,12 +59,14 @@ void goto_convert_functionst::goto_convert(goto_functionst &functions)
 
   // this removes the parse tree of the bodies from memory
   #if 0
-  Forall_symbols(it, symbol_table.symbols)
+  for(const auto &symbol_pair, symbol_table.symbols)
   {
-    if(!it->second.is_type &&
-       it->second.type.id()==ID_code &&
-       it->second.value.is_not_nil())
-      it->second.value=codet();
+    if(!symbol_pair.second.is_type &&
+       symbol_pair.second.type.id()==ID_code &&
+       symbol_pair.second.value.is_not_nil())
+    {
+      symbol_pair.second.value=codet();
+    }
   }
   #endif
 }
diff --git a/src/goto-programs/link_goto_model.cpp b/src/goto-programs/link_goto_model.cpp
index 029a1665a25..6fd9702cf0e 100644
--- a/src/goto-programs/link_goto_model.cpp
+++ b/src/goto-programs/link_goto_model.cpp
@@ -110,13 +110,14 @@ static bool link_functions(
   // apply macros
   rename_symbolt macro_application;
 
-  forall_symbols(it, dest_symbol_table.symbols)
-    if(it->second.is_macro && !it->second.is_type)
+  for(const auto &symbol_pair : dest_symbol_table.symbols)
+  {
+    if(symbol_pair.second.is_macro && !symbol_pair.second.is_type)
     {
-      const symbolt &symbol=it->second;
+      const symbolt &symbol = symbol_pair.second;
 
-      INVARIANT(symbol.value.id()==ID_symbol, "must have symbol");
-      const irep_idt &id=to_symbol_expr(symbol.value).get_identifier();
+      INVARIANT(symbol.value.id() == ID_symbol, "must have symbol");
+      const irep_idt &id = to_symbol_expr(symbol.value).get_identifier();
 
       #if 0
       if(!base_type_eq(symbol.type, ns.lookup(id).type, ns))
@@ -130,6 +131,7 @@ static bool link_functions(
 
       macro_application.insert_expr(symbol.name, id);
     }
+  }
 
   if(!macro_application.expr_map.empty())
     Forall_goto_functions(dest_it, dest_functions)
@@ -159,9 +161,11 @@ void link_goto_model(
   typedef std::unordered_set<irep_idt, irep_id_hash> id_sett;
   id_sett weak_symbols;
 
-  forall_symbols(it, dest.symbol_table.symbols)
-    if(it->second.is_weak)
-      weak_symbols.insert(it->first);
+  for(const auto &symbol_pair : dest.symbol_table.symbols)
+  {
+    if(symbol_pair.second.is_weak)
+      weak_symbols.insert(symbol_pair.first);
+  }
 
   linkingt linking(dest.symbol_table,
                    src.symbol_table,
diff --git a/src/goto-programs/show_symbol_table.cpp b/src/goto-programs/show_symbol_table.cpp
index f65728df11b..771bc88da00 100644
--- a/src/goto-programs/show_symbol_table.cpp
+++ b/src/goto-programs/show_symbol_table.cpp
@@ -30,8 +30,10 @@ void show_symbol_table_brief_plain(
   // we want to sort alphabetically
   std::set<std::string> symbols;
 
-  forall_symbols(it, symbol_table.symbols)
-    symbols.insert(id2string(it->first));
+  for(const auto &symbol_pair : symbol_table.symbols)
+  {
+    symbols.insert(id2string(symbol_pair.first));
+  }
 
   const namespacet ns(symbol_table);
 
@@ -68,8 +70,10 @@ void show_symbol_table_plain(
   // we want to sort alphabetically
   std::set<std::string> symbols;
 
-  forall_symbols(it, symbol_table.symbols)
-    symbols.insert(id2string(it->first));
+  for(const auto &symbol_pair : symbol_table.symbols)
+  {
+    symbols.insert(id2string(symbol_pair.first));
+  }
 
   const namespacet ns(symbol_table);
 
diff --git a/src/goto-programs/write_goto_binary.cpp b/src/goto-programs/write_goto_binary.cpp
index bdc353ad122..a6d0f144cb2 100644
--- a/src/goto-programs/write_goto_binary.cpp
+++ b/src/goto-programs/write_goto_binary.cpp
@@ -30,12 +30,12 @@ bool write_goto_binary_v3(
 
   write_gb_word(out, symbol_table.symbols.size());
 
-  forall_symbols(it, symbol_table.symbols)
+  for(const auto &symbol_pair : symbol_table.symbols)
   {
     // Since version 2, symbols are not converted to ireps,
     // instead they are saved in a custom binary format
 
-    const symbolt &sym = it->second;
+    const symbolt &sym = symbol_pair.second;
 
     irepconverter.reference_convert(sym.type, out);
     irepconverter.reference_convert(sym.value, out);
diff --git a/src/goto-symex/symex_start_thread.cpp b/src/goto-symex/symex_start_thread.cpp
index a7e3101d84d..4b672574aab 100644
--- a/src/goto-symex/symex_start_thread.cpp
+++ b/src/goto-symex/symex_start_thread.cpp
@@ -97,9 +97,9 @@ void goto_symext::symex_start_thread(statet &state)
   // initialize all variables marked thread-local
   const symbol_tablet &symbol_table=ns.get_symbol_table();
 
-  forall_symbols(it, symbol_table.symbols)
+  for(const auto &symbol_pair : symbol_table.symbols)
   {
-    const symbolt &symbol=it->second;
+    const symbolt &symbol = symbol_pair.second;
 
     if(!symbol.is_thread_local ||
        !symbol.is_static_lifetime ||
diff --git a/src/java_bytecode/java_bytecode_convert_method.cpp b/src/java_bytecode/java_bytecode_convert_method.cpp
index 5df719e5172..62fd222fe2a 100644
--- a/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -1019,7 +1019,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
        i_it->statement=="jsr" ||
        i_it->statement=="jsr_w")
     {
-      assert(!i_it->args.empty());
+      PRECONDITION(!i_it->args.empty());
 
       unsigned target;
       bool ret=to_unsigned_integer(to_constant_expr(i_it->args[0]), target);
@@ -1104,7 +1104,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
   {
     std::set<unsigned>::iterator cur=working_set.begin();
     address_mapt::iterator a_it=address_map.find(*cur);
-    assert(a_it!=address_map.end());
+    CHECK_RETURN(a_it != address_map.end());
     unsigned cur_pc=*cur;
     working_set.erase(cur);
 
@@ -1196,7 +1196,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     }
     else if(statement=="athrow")
     {
-      assert(op.size()==1 && results.size()==1);
+      PRECONDITION(op.size() == 1 && results.size() == 1);
 
       side_effect_expr_throwt throw_expr;
       throw_expr.add_source_location()=i_it->source_location;
@@ -1209,7 +1209,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
       // checkcast throws an exception in case a cast of object
       // on stack to given type fails.
       // The stack isn't modified.
-      assert(op.size()==1 && results.size()==1);
+      PRECONDITION(op.size() == 1 && results.size() == 1);
       binary_predicate_exprt check(op[0], ID_java_instanceof, arg0);
       code_assertt assert_class(check);
       assert_class.add_source_location().set_comment("Dynamic cast check");
@@ -1431,14 +1431,14 @@ codet java_bytecode_convert_methodt::convert_instructions(
     }
     else if(statement=="return")
     {
-      assert(op.empty() && results.empty());
+      PRECONDITION(op.empty() && results.empty());
       c=code_returnt();
     }
     else if(statement==patternt("?return"))
     {
       // Return types are promoted in java, so this might need
       // conversion.
-      assert(op.size()==1 && results.empty());
+      PRECONDITION(op.size() == 1 && results.empty());
       exprt r=op[0];
       if(r.type()!=method_return_type)
         r=typecast_exprt(r, method_return_type);
@@ -1485,7 +1485,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     else if(statement==patternt("?store"))
     {
       // store value into some local variable
-      assert(op.size()==1 && results.empty());
+      PRECONDITION(op.size() == 1 && results.empty());
 
       exprt var=
         variable(arg0, statement[0], i_it->address, NO_CAST);
@@ -1510,7 +1510,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     }
     else if(statement==patternt("?aload"))
     {
-      assert(op.size()==2 && results.size()==1);
+      PRECONDITION(op.size() == 2 && results.size() == 1);
 
       char type_char=statement[0];
 
@@ -1541,7 +1541,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     else if(statement=="ldc" || statement=="ldc_w" ||
             statement=="ldc2" || statement=="ldc2_w")
     {
-      assert(op.empty() && results.size()==1);
+      PRECONDITION(op.empty() && results.size() == 1);
 
       INVARIANT(
         arg0.id() != ID_java_string_literal && arg0.id() != ID_type,
@@ -1552,7 +1552,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     }
     else if(statement=="goto" || statement=="goto_w")
     {
-      assert(op.empty() && results.empty());
+      PRECONDITION(op.empty() && results.empty());
       mp_integer number;
       bool ret=to_integer(to_constant_expr(arg0), number);
       INVARIANT(!ret, "goto argument should be an integer");
@@ -1562,7 +1562,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     else if(statement=="jsr" || statement=="jsr_w")
     {
       // As 'goto', except we must also push the subroutine return address:
-      assert(op.empty() && results.size()==1);
+      PRECONDITION(op.empty() && results.size() == 1);
       mp_integer number;
       bool ret=to_integer(to_constant_expr(arg0), number);
       INVARIANT(!ret, "jsr argument should be an integer");
@@ -1579,7 +1579,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
       // Since we have a bounded target set, make life easier on our analyses
       // and write something like:
       // if(retaddr==5) goto 5; else if(retaddr==10) goto 10; ...
-      assert(op.empty() && results.empty());
+      PRECONDITION(op.empty() && results.empty());
       c=code_blockt();
       auto retvar=variable(arg0, 'a', i_it->address, NO_CAST);
       assert(!jsr_ret_targets.empty());
@@ -1659,7 +1659,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     }
     else if(statement==patternt("if_?cmp??"))
     {
-      assert(op.size()==2 && results.empty());
+      PRECONDITION(op.size() == 2 && results.empty());
       mp_integer number;
       bool ret=to_integer(to_constant_expr(arg0), number);
       INVARIANT(!ret, "if_?cmp?? argument should be an integer");
@@ -1697,7 +1697,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
 
       INVARIANT(!id.empty(), "unexpected bytecode-if");
 
-      assert(op.size()==1 && results.empty());
+      PRECONDITION(op.size() == 1 && results.empty());
       mp_integer number;
       bool ret=to_integer(to_constant_expr(arg0), number);
       INVARIANT(!ret, "if?? argument should be an integer");
@@ -1718,7 +1718,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     }
     else if(statement==patternt("ifnonnull"))
     {
-      assert(op.size()==1 && results.empty());
+      PRECONDITION(op.size() == 1 && results.empty());
       mp_integer number;
       bool ret=to_integer(to_constant_expr(arg0), number);
       INVARIANT(!ret, "ifnonnull argument should be an integer");
@@ -1735,7 +1735,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     }
     else if(statement==patternt("ifnull"))
     {
-      assert(op.size()==1 && results.empty());
+      PRECONDITION(op.size() == 1 && results.empty());
       mp_integer number;
       bool ret=to_integer(to_constant_expr(arg0), number);
       INVARIANT(!ret, "ifnull argument should be an integer");
@@ -1777,32 +1777,32 @@ codet java_bytecode_convert_methodt::convert_instructions(
     }
     else if(statement==patternt("?xor"))
     {
-      assert(op.size()==2 && results.size()==1);
+      PRECONDITION(op.size() == 2 && results.size() == 1);
       results[0]=bitxor_exprt(op[0], op[1]);
     }
     else if(statement==patternt("?or"))
     {
-      assert(op.size()==2 && results.size()==1);
+      PRECONDITION(op.size() == 2 && results.size() == 1);
       results[0]=bitor_exprt(op[0], op[1]);
     }
     else if(statement==patternt("?and"))
     {
-      assert(op.size()==2 && results.size()==1);
+      PRECONDITION(op.size() == 2 && results.size() == 1);
       results[0]=bitand_exprt(op[0], op[1]);
     }
     else if(statement==patternt("?shl"))
     {
-      assert(op.size()==2 && results.size()==1);
+      PRECONDITION(op.size() == 2 && results.size() == 1);
       results[0]=shl_exprt(op[0], op[1]);
     }
     else if(statement==patternt("?shr"))
     {
-      assert(op.size()==2 && results.size()==1);
+      PRECONDITION(op.size() == 2 && results.size() == 1);
       results[0]=ashr_exprt(op[0], op[1]);
     }
     else if(statement==patternt("?ushr"))
     {
-      assert(op.size()==2 && results.size()==1);
+      PRECONDITION(op.size() == 2 && results.size() == 1);
       const typet type=java_type_from_char(statement[0]);
 
       const std::size_t width=type.get_size_t(ID_width);
@@ -1821,32 +1821,32 @@ codet java_bytecode_convert_methodt::convert_instructions(
     }
     else if(statement==patternt("?add"))
     {
-      assert(op.size()==2 && results.size()==1);
+      PRECONDITION(op.size() == 2 && results.size() == 1);
       results[0]=plus_exprt(op[0], op[1]);
     }
     else if(statement==patternt("?sub"))
     {
-      assert(op.size()==2 && results.size()==1);
+      PRECONDITION(op.size() == 2 && results.size() == 1);
       results[0]=minus_exprt(op[0], op[1]);
     }
     else if(statement==patternt("?div"))
     {
-      assert(op.size()==2 && results.size()==1);
+      PRECONDITION(op.size() == 2 && results.size() == 1);
       results[0]=div_exprt(op[0], op[1]);
     }
     else if(statement==patternt("?mul"))
     {
-      assert(op.size()==2 && results.size()==1);
+      PRECONDITION(op.size() == 2 && results.size() == 1);
       results[0]=mult_exprt(op[0], op[1]);
     }
     else if(statement==patternt("?neg"))
     {
-      assert(op.size()==1 && results.size()==1);
+      PRECONDITION(op.size() == 1 && results.size() == 1);
       results[0]=unary_minus_exprt(op[0], op[0].type());
     }
     else if(statement==patternt("?rem"))
     {
-      assert(op.size()==2 && results.size()==1);
+      PRECONDITION(op.size() == 2 && results.size() == 1);
       if(statement=="frem" || statement=="drem")
         results[0]=rem_exprt(op[0], op[1]);
       else
@@ -1854,7 +1854,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     }
     else if(statement==patternt("?cmp"))
     {
-      assert(op.size()==2 && results.size()==1);
+      PRECONDITION(op.size() == 2 && results.size() == 1);
 
       // The integer result on the stack is:
       //  0 if op[0] equals op[1]
@@ -1878,7 +1878,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     }
     else if(statement==patternt("?cmp?"))
     {
-      assert(op.size()==2 && results.size()==1);
+      PRECONDITION(op.size() == 2 && results.size() == 1);
       const int nan_value(statement[4]=='l' ? -1 : 1);
       const typet result_type(java_int_type());
       const exprt nan_result(from_integer(nan_value, result_type));
@@ -1906,24 +1906,24 @@ codet java_bytecode_convert_methodt::convert_instructions(
     }
     else if(statement==patternt("?cmpl"))
     {
-      assert(op.size()==2 && results.size()==1);
+      PRECONDITION(op.size() == 2 && results.size() == 1);
       results[0]=binary_relation_exprt(op[0], ID_lt, op[1]);
     }
     else if(statement=="dup")
     {
-      assert(op.size()==1 && results.size()==2);
+      PRECONDITION(op.size() == 1 && results.size() == 2);
       results[0]=results[1]=op[0];
     }
     else if(statement=="dup_x1")
     {
-      assert(op.size()==2 && results.size()==3);
+      PRECONDITION(op.size() == 2 && results.size() == 3);
       results[0]=op[1];
       results[1]=op[0];
       results[2]=op[1];
     }
     else if(statement=="dup_x2")
     {
-      assert(op.size()==3 && results.size()==4);
+      PRECONDITION(op.size() == 3 && results.size() == 4);
       results[0]=op[2];
       results[1]=op[0];
       results[2]=op[1];
@@ -1933,7 +1933,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     // stack
     else if(statement=="dup2")
     {
-      assert(!stack.empty() && results.empty());
+      PRECONDITION(!stack.empty() && results.empty());
 
       if(get_bytecode_type_width(stack.back().type())==32)
         op=pop(2);
@@ -1945,7 +1945,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     }
     else if(statement=="dup2_x1")
     {
-      assert(!stack.empty() && results.empty());
+      PRECONDITION(!stack.empty() && results.empty());
 
       if(get_bytecode_type_width(stack.back().type())==32)
         op=pop(3);
@@ -1957,7 +1957,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     }
     else if(statement=="dup2_x2")
     {
-      assert(!stack.empty() && results.empty());
+      PRECONDITION(!stack.empty() && results.empty());
 
       if(get_bytecode_type_width(stack.back().type())==32)
         op=pop(2);
@@ -1978,20 +1978,20 @@ codet java_bytecode_convert_methodt::convert_instructions(
     }
     else if(statement=="dconst")
     {
-      assert(op.empty() && results.size()==1);
+      PRECONDITION(op.empty() && results.size() == 1);
     }
     else if(statement=="fconst")
     {
-      assert(op.empty() && results.size()==1);
+      PRECONDITION(op.empty() && results.size() == 1);
     }
     else if(statement=="getfield")
     {
-      assert(op.size()==1 && results.size()==1);
+      PRECONDITION(op.size() == 1 && results.size() == 1);
       results[0]=java_bytecode_promotion(to_member(op[0], arg0));
     }
     else if(statement=="getstatic")
     {
-      assert(op.empty() && results.size()==1);
+      PRECONDITION(op.empty() && results.size() == 1);
       symbol_exprt symbol_expr(arg0.type());
       const auto &field_name=arg0.get_string(ID_component_name);
       const bool is_assertions_disabled_field=
@@ -2041,7 +2041,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     }
     else if(statement=="putfield")
     {
-      assert(op.size()==2 && results.empty());
+      PRECONDITION(op.size() == 2 && results.empty());
       code_blockt block;
       save_stack_entries(
         "stack_field",
@@ -2054,7 +2054,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     }
     else if(statement=="putstatic")
     {
-      assert(op.size()==1 && results.empty());
+      PRECONDITION(op.size() == 1 && results.empty());
       symbol_exprt symbol_expr(arg0.type());
       const auto &field_name=arg0.get_string(ID_component_name);
       symbol_expr.set_identifier(
@@ -2091,7 +2091,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     }
     else if(statement==patternt("?2?")) // i2c etc.
     {
-      assert(op.size()==1 && results.size()==1);
+      PRECONDITION(op.size() == 1 && results.size() == 1);
       typet type=java_type_from_char(statement[2]);
       results[0]=op[0];
       if(results[0].type()!=type)
@@ -2100,7 +2100,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     else if(statement=="new")
     {
       // use temporary since the stack symbol might get duplicated
-      assert(op.empty() && results.size()==1);
+      PRECONDITION(op.empty() && results.size() == 1);
       const reference_typet ref_type=java_reference_type(arg0.type());
       exprt java_new_expr=side_effect_exprt(ID_java_new, ref_type);
 
@@ -2125,7 +2125,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
             statement=="anewarray")
     {
       // the op is the array size
-      assert(op.size()==1 && results.size()==1);
+      PRECONDITION(op.size() == 1 && results.size() == 1);
 
       char element_type;
 
@@ -2217,7 +2217,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     }
     else if(statement=="arraylength")
     {
-      assert(op.size()==1 && results.size()==1);
+      PRECONDITION(op.size() == 1 && results.size() == 1);
 
       exprt pointer=
         typecast_exprt(op[0], java_array_type(statement[0]));
@@ -2233,7 +2233,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     else if(statement=="tableswitch" ||
             statement=="lookupswitch")
     {
-      assert(op.size()==1 && results.empty());
+      PRECONDITION(op.size() == 1 && results.empty());
 
       // we turn into switch-case
       code_switcht code_switch;
@@ -2294,7 +2294,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     }
     else if(statement=="instanceof")
     {
-      assert(op.size()==1 && results.size()==1);
+      PRECONDITION(op.size() == 1 && results.size() == 1);
 
       results[0]=
         binary_predicate_exprt(op[0], ID_java_instanceof, arg0);
@@ -2329,7 +2329,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     }
     else if(statement=="swap")
     {
-      assert(op.size()==2 && results.size()==2);
+      PRECONDITION(op.size() == 2 && results.size() == 2);
       results[1]=op[0];
       results[0]=op[1];
     }
@@ -2465,7 +2465,7 @@ codet java_bytecode_convert_methodt::convert_instructions(
     for(const unsigned address : a_it->second.successors)
     {
       address_mapt::iterator a_it2=address_map.find(address);
-      assert(a_it2!=address_map.end());
+      CHECK_RETURN(a_it2 != address_map.end());
 
       // clear the stack if this is an exception handler
       for(const auto &exception_row : method.exception_table)
@@ -2499,7 +2499,9 @@ codet java_bytecode_convert_methodt::convert_instructions(
         }
         else
         {
-          assert(a_it2->second.stack.size()==stack.size());
+          INVARIANT(
+            a_it2->second.stack.size() == stack.size(),
+            "Stack sizes should be the same.");
           stackt::const_iterator os_it=a_it2->second.stack.begin();
           for(auto &expr : stack)
           {
diff --git a/src/java_bytecode/java_bytecode_instrument.cpp b/src/java_bytecode/java_bytecode_instrument.cpp
index ef302e1c9c5..7c09b07b2fe 100644
--- a/src/java_bytecode/java_bytecode_instrument.cpp
+++ b/src/java_bytecode/java_bytecode_instrument.cpp
@@ -614,14 +614,18 @@ void java_bytecode_instrument(
     message_handler);
 
   std::vector<irep_idt> symbols_to_instrument;
-  forall_symbols(s_it, symbol_table.symbols)
+  for(const auto &symbol_pair : symbol_table.symbols)
   {
-    if(s_it->second.value.id()==ID_code)
-      symbols_to_instrument.push_back(s_it->first);
+    if(symbol_pair.second.value.id() == ID_code)
+    {
+      symbols_to_instrument.push_back(symbol_pair.first);
+    }
   }
 
   // instrument(...) can add symbols to the table, so it's
   // not safe to hold a reference to a symbol across a call.
   for(const auto &symbol : symbols_to_instrument)
+  {
     instrument(to_code(symbol_table.get_writeable_ref(symbol).value));
+  }
 }
diff --git a/src/java_bytecode/java_bytecode_typecheck.cpp b/src/java_bytecode/java_bytecode_typecheck.cpp
index 36d9e170068..78a56171060 100644
--- a/src/java_bytecode/java_bytecode_typecheck.cpp
+++ b/src/java_bytecode/java_bytecode_typecheck.cpp
@@ -40,8 +40,8 @@ void java_bytecode_typecheckt::typecheck()
   // and we might add new symbols.
   journalling_symbol_tablet::changesett identifiers;
   identifiers.reserve(symbol_table.symbols.size());
-  forall_symbols(s_it, symbol_table.symbols)
-    identifiers.insert(s_it->first);
+  for(const auto &symbol_pair : symbol_table.symbols)
+    identifiers.insert(symbol_pair.first);
   typecheck(identifiers);
 }
 
diff --git a/src/jsil/jsil_typecheck.cpp b/src/jsil/jsil_typecheck.cpp
index a91eaf36f6f..36393c73af6 100644
--- a/src/jsil/jsil_typecheck.cpp
+++ b/src/jsil/jsil_typecheck.cpp
@@ -888,8 +888,10 @@ void jsil_typecheckt::typecheck()
 
   std::vector<irep_idt> identifiers;
   identifiers.reserve(symbol_table.symbols.size());
-  forall_symbols(s_it, symbol_table.symbols)
-    identifiers.push_back(s_it->first);
+  for(const auto &symbol_pair : symbol_table.symbols)
+  {
+    identifiers.push_back(symbol_pair.first);
+  }
 
   // We first check all type symbols,
   // recursively doing base classes first.
diff --git a/src/langapi/language_ui.cpp b/src/langapi/language_ui.cpp
index a157cc68359..4f3f3ec479e 100644
--- a/src/langapi/language_ui.cpp
+++ b/src/langapi/language_ui.cpp
@@ -155,8 +155,10 @@ void language_uit::show_symbol_table_plain(
   // we want to sort alphabetically
   std::set<std::string> symbols;
 
-  forall_symbols(it, symbol_table.symbols)
-    symbols.insert(id2string(it->first));
+  for(const auto &symbol_pair : symbol_table.symbols)
+  {
+    symbols.insert(id2string(symbol_pair.first));
+  }
 
   const namespacet ns(symbol_table);
 
diff --git a/src/linking/linking.cpp b/src/linking/linking.cpp
index 7b2289256bf..61511a54f73 100644
--- a/src/linking/linking.cpp
+++ b/src/linking/linking.cpp
@@ -1156,20 +1156,17 @@ void linkingt::do_type_dependencies(id_sett &needs_to_be_renamed)
 
   used_byt used_by;
 
-  forall_symbols(s_it, src_symbol_table.symbols)
+  for(const auto &symbol_pair : src_symbol_table.symbols)
   {
-    if(s_it->second.is_type)
+    if(symbol_pair.second.is_type)
     {
       // find type and array-size symbols
       find_symbols_sett symbols_used;
-      find_type_and_expr_symbols(s_it->second.type, symbols_used);
+      find_type_and_expr_symbols(symbol_pair.second.type, symbols_used);
 
-      for(find_symbols_sett::const_iterator
-          it=symbols_used.begin();
-          it!=symbols_used.end();
-          it++)
+      for(const auto &symbol_used : symbols_used)
       {
-        used_by[*it].insert(s_it->first);
+        used_by[symbol_used].insert(symbol_pair.first);
       }
     }
   }
@@ -1305,18 +1302,18 @@ void linkingt::typecheck()
 
   id_sett needs_to_be_renamed;
 
-  forall_symbols(s_it, src_symbol_table.symbols)
+  for(const auto &symbol_pair : src_symbol_table.symbols)
   {
-    symbol_tablet::symbolst::const_iterator
-      m_it=main_symbol_table.symbols.find(s_it->first);
+    symbol_tablet::symbolst::const_iterator m_it =
+      main_symbol_table.symbols.find(symbol_pair.first);
 
-    if(m_it!=main_symbol_table.symbols.end() && // duplicate
-       needs_renaming(m_it->second, s_it->second))
+    if(
+      m_it != main_symbol_table.symbols.end() && // duplicate
+      needs_renaming(m_it->second, symbol_pair.second))
     {
-      needs_to_be_renamed.insert(s_it->first);
+      needs_to_be_renamed.insert(symbol_pair.first);
       #ifdef DEBUG
-      debug() << "LINKING: needs to be renamed: "
-              << s_it->first << eom;
+      debug() << "LINKING: needs to be renamed: " << symbol_pair.first << eom;
       #endif
     }
   }
diff --git a/src/linking/static_lifetime_init.cpp b/src/linking/static_lifetime_init.cpp
index 1b085098e8d..8178f839ea1 100644
--- a/src/linking/static_lifetime_init.cpp
+++ b/src/linking/static_lifetime_init.cpp
@@ -49,8 +49,10 @@ bool static_lifetime_init(
   // sort alphabetically for reproducible results
   std::set<std::string> symbols;
 
-  forall_symbols(it, symbol_table.symbols)
-    symbols.insert(id2string(it->first));
+  for(const auto &symbol_pair : symbol_table.symbols)
+  {
+    symbols.insert(id2string(symbol_pair.first));
+  }
 
   for(const std::string &id : symbols)
   {
diff --git a/src/pointer-analysis/value_set_analysis_fi.cpp b/src/pointer-analysis/value_set_analysis_fi.cpp
index dee9db9ad94..b45addff751 100644
--- a/src/pointer-analysis/value_set_analysis_fi.cpp
+++ b/src/pointer-analysis/value_set_analysis_fi.cpp
@@ -156,10 +156,13 @@ void value_set_analysis_fit::get_globals(
   std::list<value_set_fit::entryt> &dest)
 {
   // static ones
-  forall_symbols(it, ns.get_symbol_table().symbols)
-    if(it->second.is_lvalue &&
-       it->second.is_static_lifetime)
-      get_entries(it->second, dest);
+  for(const auto &symbol_pair : ns.get_symbol_table().symbols)
+  {
+    if(symbol_pair.second.is_lvalue && symbol_pair.second.is_static_lifetime)
+    {
+      get_entries(symbol_pair.second, dest);
+    }
+  }
 }
 
 bool value_set_analysis_fit::check_type(const typet &type)
diff --git a/src/pointer-analysis/value_set_analysis_fivr.cpp b/src/pointer-analysis/value_set_analysis_fivr.cpp
index 9b46f458896..c343b0c200a 100644
--- a/src/pointer-analysis/value_set_analysis_fivr.cpp
+++ b/src/pointer-analysis/value_set_analysis_fivr.cpp
@@ -146,10 +146,13 @@ void value_set_analysis_fivrt::get_globals(
   std::list<value_set_fivrt::entryt> &dest)
 {
   // static ones
-  forall_symbols(it, ns.get_symbol_table().symbols)
-    if(it->second.is_lvalue &&
-       it->second.is_static_lifetime)
-      get_entries(it->second, dest);
+  for(const auto &it : ns.get_symbol_table().symbols)
+  {
+    if(it.second.is_lvalue && it.second.is_static_lifetime)
+    {
+      get_entries(it.second, dest);
+    }
+  }
 }
 
 bool value_set_analysis_fivrt::check_type(const typet &type)
diff --git a/src/pointer-analysis/value_set_analysis_fivrns.cpp b/src/pointer-analysis/value_set_analysis_fivrns.cpp
index 63870eb7432..e6ed4f8ecd1 100644
--- a/src/pointer-analysis/value_set_analysis_fivrns.cpp
+++ b/src/pointer-analysis/value_set_analysis_fivrns.cpp
@@ -146,10 +146,13 @@ void value_set_analysis_fivrnst::get_globals(
   std::list<value_set_fivrnst::entryt> &dest)
 {
   // static ones
-  forall_symbols(it, ns.get_symbol_table().symbols)
-    if(it->second.is_lvalue &&
-       it->second.is_static_lifetime)
-      get_entries(it->second, dest);
+  for(const auto &it : ns.get_symbol_table().symbols)
+  {
+    if(it.second.is_lvalue && it.second.is_static_lifetime)
+    {
+      get_entries(it.second, dest);
+    }
+  }
 }
 
 bool value_set_analysis_fivrnst::check_type(const typet &type)
diff --git a/src/util/get_module.cpp b/src/util/get_module.cpp
index 3af2c46b49c..b53196c1391 100644
--- a/src/util/get_module.cpp
+++ b/src/util/get_module.cpp
@@ -83,9 +83,9 @@ const symbolt &get_module(
   symbolptr_listt symbolptr_list, main_symbolptr_list;
   messaget message(message_handler);
 
-  forall_symbols(it, symbol_table.symbols)
+  for(const auto &symbol_pair : symbol_table.symbols)
   {
-    const symbolt &s=it->second;
+    const symbolt &s = symbol_pair.second;
 
     if(s.type.id()!=ID_module)
       continue;
diff --git a/src/util/namespace.cpp b/src/util/namespace.cpp
index 218e73d2850..5329755d0cc 100644
--- a/src/util/namespace.cpp
+++ b/src/util/namespace.cpp
@@ -26,12 +26,16 @@ unsigned get_max(
 {
   unsigned max_nr=0;
 
-  forall_symbols(it, symbols)
-    if(has_prefix(id2string(it->first), prefix))
-      max_nr=
-        std::max(unsafe_string2unsigned(
-                  id2string(it->first).substr(prefix.size())),
-                 max_nr);
+  for(const auto &symbol_pair : symbols)
+  {
+    if(has_prefix(id2string(symbol_pair.first), prefix))
+    {
+      max_nr = std::max(
+        unsafe_string2unsigned(
+          id2string(symbol_pair.first).substr(prefix.size())),
+        max_nr);
+    }
+  }
 
   return max_nr;
 }
diff --git a/src/util/symbol_table.h b/src/util/symbol_table.h
index 8bd7cf7d797..deb83f237cd 100644
--- a/src/util/symbol_table.h
+++ b/src/util/symbol_table.h
@@ -8,20 +8,11 @@
 
 #include "symbol_table_base.h"
 
-#define forall_symbols(it, expr) \
-  for(symbol_tablet::symbolst::const_iterator it=(expr).begin(); \
-      it!=(expr).end(); ++it)
-
 #define forall_symbol_base_map(it, expr, base_name) \
   for(symbol_base_mapt::const_iterator it=(expr).lower_bound(base_name), \
                                        it_end=(expr).upper_bound(base_name); \
       it!=it_end; ++it)
 
-#define forall_symbol_module_map(it, expr, module) \
-  for(symbol_module_mapt::const_iterator it=(expr).lower_bound(module), \
-                                         it_end=(expr).upper_bound(module); \
-      it!=it_end; ++it)
-
 
 /// \brief The symbol table
 /// \ingroup gr_symbol_table