diff --git a/src/util/irep.cpp b/src/util/irep.cpp
index b5fb653ae3f..e9778239ef6 100644
--- a/src/util/irep.cpp
+++ b/src/util/irep.cpp
@@ -17,7 +17,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "string_hash.h"
 #include "irep_hash.h"
 
-#ifdef SUB_IS_LIST
+#ifdef NAMED_SUB_IS_FORWARD_LIST
 #include <algorithm>
 #endif
 
@@ -31,7 +31,7 @@ irept nil_rep_storage;
 irept::dt irept::empty_d;
 #endif
 
-#ifdef SUB_IS_LIST
+#ifdef NAMED_SUB_IS_FORWARD_LIST
 static inline bool named_subt_order(
   const std::pair<irep_namet, irept> &a,
   const irep_namet &b)
@@ -152,9 +152,9 @@ void irept::nonrecursive_destructor(dt *old_data)
 
     if(d->ref_count==0)
     {
-      stack.reserve(stack.size()+
-                    d->named_sub.size()+
-                    d->sub.size());
+      stack.reserve(
+        stack.size() + std::distance(d->named_sub.begin(), d->named_sub.end()) +
+        d->sub.size());
 
       for(named_subt::iterator
           it=d->named_sub.begin();
@@ -203,7 +203,7 @@ const irep_idt &irept::get(const irep_namet &name) const
 {
   const named_subt &s = get_named_sub();
 
-#ifdef SUB_IS_LIST
+#ifdef NAMED_SUB_IS_FORWARD_LIST
   named_subt::const_iterator it=named_subt_lower_bound(s, name);
 
   if(it==s.end() ||
@@ -259,11 +259,16 @@ void irept::remove(const irep_namet &name)
 {
   named_subt &s = get_named_sub();
 
-#ifdef SUB_IS_LIST
+#ifdef NAMED_SUB_IS_FORWARD_LIST
   named_subt::iterator it=named_subt_lower_bound(s, name);
 
   if(it!=s.end() && it->first==name)
-    s.erase(it);
+  {
+    named_subt::iterator before = s.before_begin();
+    while(std::next(before) != it)
+      ++before;
+    s.erase_after(before);
+  }
 #else
   s.erase(name);
 #endif
@@ -273,7 +278,7 @@ const irept &irept::find(const irep_namet &name) const
 {
   const named_subt &s = get_named_sub();
 
-#ifdef SUB_IS_LIST
+#ifdef NAMED_SUB_IS_FORWARD_LIST
   named_subt::const_iterator it=named_subt_lower_bound(s, name);
 
   if(it==s.end() ||
@@ -293,12 +298,17 @@ irept &irept::add(const irep_namet &name)
 {
   named_subt &s = get_named_sub();
 
-#ifdef SUB_IS_LIST
+#ifdef NAMED_SUB_IS_FORWARD_LIST
   named_subt::iterator it=named_subt_lower_bound(s, name);
 
   if(it==s.end() ||
      it->first!=name)
-    it=s.insert(it, std::make_pair(name, irept()));
+  {
+    named_subt::iterator before = s.before_begin();
+    while(std::next(before) != it)
+      ++before;
+    it = s.emplace_after(before, name, irept());
+  }
 
   return it->second;
 #else
@@ -310,12 +320,17 @@ irept &irept::add(const irep_namet &name, const irept &irep)
 {
   named_subt &s = get_named_sub();
 
-#ifdef SUB_IS_LIST
+#ifdef NAMED_SUB_IS_FORWARD_LIST
   named_subt::iterator it=named_subt_lower_bound(s, name);
 
   if(it==s.end() ||
      it->first!=name)
-    it=s.insert(it, std::make_pair(name, irep));
+  {
+    named_subt::iterator before = s.before_begin();
+    while(std::next(before) != it)
+      ++before;
+    it = s.emplace_after(before, name, irep);
+  }
   else
     it->second=irep;
 
@@ -407,13 +422,24 @@ bool irept::full_eq(const irept &other) const
 
   const irept::subt &i1_sub=get_sub();
   const irept::subt &i2_sub=other.get_sub();
+
+  if(i1_sub.size() != i2_sub.size())
+    return false;
+
   const irept::named_subt &i1_named_sub=get_named_sub();
   const irept::named_subt &i2_named_sub=other.get_named_sub();
 
+#ifdef NAMED_SUB_IS_FORWARD_LIST
   if(
-    i1_sub.size() != i2_sub.size() ||
-    i1_named_sub.size() != i2_named_sub.size())
+    std::distance(i1_named_sub.begin(), i1_named_sub.end()) !=
+    std::distance(i2_named_sub.begin(), i2_named_sub.end()))
+  {
+    return false;
+  }
+#else
+  if(i1_named_sub.size() != i2_named_sub.size())
     return false;
+#endif
 
   for(std::size_t i=0; i<i1_sub.size(); i++)
     if(!i1_sub[i].full_eq(i2_sub[i]))
@@ -667,7 +693,13 @@ std::size_t irept::full_hash() const
     result=hash_combine(result, it->second.full_hash());
   }
 
-  result = hash_finalize(result, named_sub.size() + sub.size());
+#ifdef NAMED_SUB_IS_FORWARD_LIST
+  const std::size_t named_sub_size =
+    std::distance(named_sub.begin(), named_sub.end());
+#else
+  const std::size_t named_sub_size = named_sub.size();
+#endif
+  result = hash_finalize(result, named_sub_size + sub.size());
 
   return result;
 }
diff --git a/src/util/irep.h b/src/util/irep.h
index 91c94b4cf6b..6e96af7ba9f 100644
--- a/src/util/irep.h
+++ b/src/util/irep.h
@@ -20,10 +20,10 @@ Author: Daniel Kroening, kroening@kroening.com
 #define SHARING
 // #define HASH_CODE
 #define USE_MOVE
-// #define SUB_IS_LIST
+// #define NAMED_SUB_IS_FORWARD_LIST
 
-#ifdef SUB_IS_LIST
-#include <list>
+#ifdef NAMED_SUB_IS_FORWARD_LIST
+#include <forward_list>
 #else
 #include <map>
 #endif
@@ -160,11 +160,11 @@ class irept
   // use std::forward_list or std::vector< unique_ptr<T> > to save
   // memory and increase efficiency.
 
-  #ifdef SUB_IS_LIST
-  typedef std::list<std::pair<irep_namet, irept> > named_subt;
-  #else
+#ifdef NAMED_SUB_IS_FORWARD_LIST
+  typedef std::forward_list<std::pair<irep_namet, irept>> named_subt;
+#else
   typedef std::map<irep_namet, irept> named_subt;
-  #endif
+#endif
 
   bool is_nil() const { return id()==ID_nil; }
   bool is_not_nil() const { return id()!=ID_nil; }
diff --git a/src/util/irep_hash_container.cpp b/src/util/irep_hash_container.cpp
index bb88e0ae001..7ef373be684 100644
--- a/src/util/irep_hash_container.cpp
+++ b/src/util/irep_hash_container.cpp
@@ -54,7 +54,13 @@ void irep_hash_container_baset::pack(
   {
     // we pack: the irep id, the sub size, the subs, the named-sub size, and
     // each of the named subs with their ids
-    packed.reserve(1 + 1 + sub.size() + 1 + named_sub.size() * 2);
+#ifdef NAMED_SUB_IS_FORWARD_LIST
+    const std::size_t named_sub_size =
+      std::distance(named_sub.begin(), named_sub.end());
+#else
+    const std::size_t named_sub_size = named_sub.size();
+#endif
+    packed.reserve(1 + 1 + sub.size() + 1 + named_sub_size * 2);
 
     packed.push_back(irep_id_hash()(irep.id()));
 
@@ -62,7 +68,7 @@ void irep_hash_container_baset::pack(
     forall_irep(it, sub)
       packed.push_back(number(*it));
 
-    packed.push_back(named_sub.size());
+    packed.push_back(named_sub_size);
     for(const auto &sub_irep : named_sub)
     {
       packed.push_back(irep_id_hash()(sub_irep.first)); // id
diff --git a/src/util/lispirep.cpp b/src/util/lispirep.cpp
index 9ba1a3ceae7..ec42c2dbf58 100644
--- a/src/util/lispirep.cpp
+++ b/src/util/lispirep.cpp
@@ -46,7 +46,13 @@ void irep2lisp(const irept &src, lispexprt &dest)
   dest.value="";
   dest.type=lispexprt::List;
 
-  dest.reserve(2 + 2 * src.get_sub().size() + 2 * src.get_named_sub().size());
+#ifdef NAMED_SUB_IS_FORWARD_LIST
+  const std::size_t named_sub_size =
+    std::distance(src.get_named_sub().begin(), src.get_named_sub().end());
+#else
+  const std::size_t named_sub_size = src.get_named_sub().size();
+#endif
+  dest.reserve(2 + 2 * src.get_sub().size() + 2 * named_sub_size);
 
   lispexprt id;
   id.type=lispexprt::String;
diff --git a/src/util/merge_irep.cpp b/src/util/merge_irep.cpp
index 7937adb29cf..eeb0d45c733 100644
--- a/src/util/merge_irep.cpp
+++ b/src/util/merge_irep.cpp
@@ -28,7 +28,13 @@ std::size_t to_be_merged_irept::hash() const
         result, static_cast<const merged_irept &>(it->second).hash());
   }
 
-  result=hash_finalize(result, named_sub.size()+sub.size());
+#ifdef NAMED_SUB_IS_FORWARD_LIST
+  const std::size_t named_sub_size =
+    std::distance(named_sub.begin(), named_sub.end());
+#else
+  const std::size_t named_sub_size = named_sub.size();
+#endif
+  result = hash_finalize(result, named_sub_size + sub.size());
 
   return result;
 }
@@ -45,8 +51,17 @@ bool to_be_merged_irept::operator == (const to_be_merged_irept &other) const
 
   if(sub.size()!=o_sub.size())
     return false;
+#ifdef NAMED_SUB_IS_FORWARD_LIST
+  if(
+    std::distance(named_sub.begin(), named_sub.end()) !=
+    std::distance(o_named_sub.begin(), o_named_sub.end()))
+  {
+    return false;
+  }
+#else
   if(named_sub.size()!=o_named_sub.size())
     return false;
+#endif
 
   {
     irept::subt::const_iterator s_it=sub.begin();
@@ -95,13 +110,19 @@ const merged_irept &merged_irepst::merged(const irept &irep)
   const irept::named_subt &src_named_sub=irep.get_named_sub();
   irept::named_subt &dest_named_sub=new_irep.get_named_sub();
 
+#ifdef NAMED_SUB_IS_FORWARD_LIST
+  irept::named_subt::iterator before = dest_named_sub.before_begin();
+#endif
   forall_named_irep(it, src_named_sub)
-    #ifdef SUB_IS_LIST
-    dest_named_sub.push_back(
-      std::make_pair(it->first, merged(it->second))); // recursive call
-    #else
+  {
+#ifdef NAMED_SUB_IS_FORWARD_LIST
+    dest_named_sub.emplace_after(
+      before, it->first, merged(it->second)); // recursive call
+    ++before;
+#else
     dest_named_sub[it->first]=merged(it->second); // recursive call
-    #endif
+#endif
+  }
 
   std::pair<to_be_merged_irep_storet::const_iterator, bool> result=
     to_be_merged_irep_store.insert(to_be_merged_irept(new_irep));
@@ -140,13 +161,19 @@ const irept &merge_irept::merged(const irept &irep)
   const irept::named_subt &src_named_sub=irep.get_named_sub();
   irept::named_subt &dest_named_sub=new_irep.get_named_sub();
 
+#ifdef NAMED_SUB_IS_FORWARD_LIST
+  irept::named_subt::iterator before = dest_named_sub.before_begin();
+#endif
   forall_named_irep(it, src_named_sub)
-    #ifdef SUB_IS_LIST
-    dest_named_sub.push_back(
-      std::make_pair(it->first, merged(it->second))); // recursive call
-    #else
+  {
+#ifdef NAMED_SUB_IS_FORWARD_LIST
+    dest_named_sub.emplace_after(
+      before, it->first, merged(it->second)); // recursive call
+    ++before;
+#else
     dest_named_sub[it->first]=merged(it->second); // recursive call
-    #endif
+#endif
+  }
 
   return *irep_store.insert(std::move(new_irep)).first;
 }
@@ -177,13 +204,19 @@ const irept &merge_full_irept::merged(const irept &irep)
   const irept::named_subt &src_named_sub=irep.get_named_sub();
   irept::named_subt &dest_named_sub=new_irep.get_named_sub();
 
+#ifdef NAMED_SUB_IS_FORWARD_LIST
+  irept::named_subt::iterator before = dest_named_sub.before_begin();
+#endif
   forall_named_irep(it, src_named_sub)
-    #ifdef SUB_IS_LIST
-    dest_named_sub.push_back(
-      std::make_pair(it->first, merged(it->second))); // recursive call
-    #else
+  {
+#ifdef NAMED_SUB_IS_FORWARD_LIST
+    dest_named_sub.emplace_after(
+      before, it->first, merged(it->second)); // recursive call
+    ++before;
+#else
     dest_named_sub[it->first]=merged(it->second); // recursive call
-    #endif
+#endif
+  }
 
   return *irep_store.insert(std::move(new_irep)).first;
 }
diff --git a/unit/util/irep.cpp b/unit/util/irep.cpp
index f22bbfd35e9..e5ac9c61b30 100644
--- a/unit/util/irep.cpp
+++ b/unit/util/irep.cpp
@@ -35,7 +35,7 @@ SCENARIO("irept_memory", "[core][utils][irept]")
       REQUIRE(sizeof(std::vector<int>) == 3 * sizeof(void *));
 #endif
 
-#ifndef SUB_IS_LIST
+#ifndef NAMED_SUB_IS_FORWARD_LIST
       const std::size_t named_size = sizeof(std::map<int, int>);
 #  ifndef _GLIBCXX_DEBUG
 #    ifdef __APPLE__
@@ -47,9 +47,9 @@ SCENARIO("irept_memory", "[core][utils][irept]")
 #    endif
 #  endif
 #else
-      const std::size_t named_size = sizeof(std::list<int>);
+      const std::size_t named_size = sizeof(std::forward_list<int>);
 #  ifndef _GLIBCXX_DEBUG
-      REQUIRE(sizeof(std::list<int>) == 3 * sizeof(void *));
+      REQUIRE(sizeof(std::forward_list<int>) == sizeof(void *));
 #  endif
 #endif
 
@@ -140,12 +140,16 @@ SCENARIO("irept_memory", "[core][utils][irept]")
       irep.add("a_new_element", irep2);
       REQUIRE(!irept::is_comment("a_new_element"));
       REQUIRE(irep.find("a_new_element").id() == "second_irep");
-      REQUIRE(irep.get_named_sub().size() == 1);
+      std::size_t named_sub_size =
+        std::distance(irep.get_named_sub().begin(), irep.get_named_sub().end());
+      REQUIRE(named_sub_size == 1);
 
       irep.add("#a_comment", irep2);
       REQUIRE(irept::is_comment("#a_comment"));
       REQUIRE(irep.find("#a_comment").id() == "second_irep");
-      REQUIRE(irep.get_named_sub().size() == 2);
+      named_sub_size =
+        std::distance(irep.get_named_sub().begin(), irep.get_named_sub().end());
+      REQUIRE(named_sub_size == 2);
       REQUIRE(irept::number_of_non_comments(irep.get_named_sub()) == 1);
 
       irept bak(irep);
@@ -160,17 +164,23 @@ SCENARIO("irept_memory", "[core][utils][irept]")
 
       irep.move_to_named_sub("another_entry", irep2);
       REQUIRE(irep.get_sub().size() == 1);
-      REQUIRE(irep.get_named_sub().size() == 2);
+      named_sub_size =
+        std::distance(irep.get_named_sub().begin(), irep.get_named_sub().end());
+      REQUIRE(named_sub_size == 2);
 
       irept irep3;
       irep.move_to_named_sub("#a_comment", irep3);
       REQUIRE(irep.find("#a_comment").id().empty());
       REQUIRE(irep.get_sub().size() == 1);
-      REQUIRE(irep.get_named_sub().size() == 2);
+      named_sub_size =
+        std::distance(irep.get_named_sub().begin(), irep.get_named_sub().end());
+      REQUIRE(named_sub_size == 2);
 
       irept irep4;
       irep.move_to_named_sub("#another_comment", irep4);
-      REQUIRE(irep.get_named_sub().size() == 3);
+      named_sub_size =
+        std::distance(irep.get_named_sub().begin(), irep.get_named_sub().end());
+      REQUIRE(named_sub_size == 3);
     }
 
     THEN("Setting and getting works")