From e3bbd580c33002793ab3437c730071c1ec7119f0 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <kroening@cs.ox.ac.uk>
Date: Sun, 14 Oct 2018 13:40:42 +0100
Subject: [PATCH] type_with_subtypest now has constructors that take the
 subtypes

---
 src/util/type.h | 13 ++++++++++++-
 1 file changed, 12 insertions(+), 1 deletion(-)

diff --git a/src/util/type.h b/src/util/type.h
index 5a7deacbe00..8074fbbb2f1 100644
--- a/src/util/type.h
+++ b/src/util/type.h
@@ -114,11 +114,22 @@ inline type_with_subtypet &to_type_with_subtype(typet &type)
 class type_with_subtypest:public typet
 {
 public:
+  typedef std::vector<typet> subtypest;
+
   type_with_subtypest() { }
 
   explicit type_with_subtypest(const irep_idt &_id):typet(_id) { }
 
-  typedef std::vector<typet> subtypest;
+  type_with_subtypest(const irep_idt &_id, const subtypest &_subtypes)
+    : typet(_id)
+  {
+    subtypes() = _subtypes;
+  }
+
+  type_with_subtypest(const irep_idt &_id, subtypest &&_subtypes) : typet(_id)
+  {
+    subtypes() = std::move(_subtypes);
+  }
 
   subtypest &subtypes()
   {