From a9db042b2ec6f5d1b2a1c27e21955d1935b996b9 Mon Sep 17 00:00:00 2001
From: thk123 <thomas@diffblue.com>
Date: Thu, 7 Mar 2019 13:46:40 +0000
Subject: [PATCH 1/3] Add variant submodule

---
 .gitmodules | 3 +++
 lib/variant | 1 +
 2 files changed, 4 insertions(+)
 create mode 160000 lib/variant

diff --git a/.gitmodules b/.gitmodules
index 371d9dff8df..e44d67c4a55 100644
--- a/.gitmodules
+++ b/.gitmodules
@@ -1,3 +1,6 @@
 [submodule "jbmc/lib/java-models-library"]
 	path = jbmc/lib/java-models-library
 	url = https://github.com/diffblue/java-models-library.git
+[submodule "lib/variant"]
+	path = lib/variant
+	url = https://github.com/mpark/variant.git
diff --git a/lib/variant b/lib/variant
new file mode 160000
index 00000000000..0b488da9beb
--- /dev/null
+++ b/lib/variant
@@ -0,0 +1 @@
+Subproject commit 0b488da9bebac980e7ba0e158a959c956a449676

From e3edd5c38140190dc7b79adc91d3076ec66c7885 Mon Sep 17 00:00:00 2001
From: thk123 <thomas@diffblue.com>
Date: Thu, 7 Mar 2019 13:53:34 +0000
Subject: [PATCH 2/3] Run existing variant tests on travis

---
 .travis.yml                  |  1 +
 scripts/run_variant_tests.sh | 10 ++++++++++
 2 files changed, 11 insertions(+)
 create mode 100755 scripts/run_variant_tests.sh

diff --git a/.travis.yml b/.travis.yml
index c62ee5db9ed..8700e554233 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -326,6 +326,7 @@ install:
   - make -C src/cpp library_check
   - make -C src "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j3
   - make -C jbmc/src "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j3
+  - ./scripts/run_variant_tests.sh -j3
 
 script:
   - if [ -e bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
diff --git a/scripts/run_variant_tests.sh b/scripts/run_variant_tests.sh
new file mode 100755
index 00000000000..5b98ae09dd4
--- /dev/null
+++ b/scripts/run_variant_tests.sh
@@ -0,0 +1,10 @@
+#!/bin/bash
+
+set -euo pipefail
+
+cd lib/variant
+mkdir -p build
+cd build
+cmake -DMPARK_VARIANT_INCLUDE_TESTS="mpark" -DCMAKE_CXX_FLAGS="-std=c++11" ..
+cmake --build . -- $@
+ctest --output-on-failure

From 8437b25c524495380cf2e12ee04504ccfe76f2cd Mon Sep 17 00:00:00 2001
From: thk123 <thomas@diffblue.com>
Date: Thu, 7 Mar 2019 14:03:48 +0000
Subject: [PATCH 3/3] Add basic unit test

Full tests are provided in the submodule - this checks that it compiles
and links correctly.
---
 CMakeLists.txt                   |  2 ++
 src/util/CMakeLists.txt          |  2 +-
 src/util/module_dependencies.txt |  2 ++
 src/util/variant.h               | 18 ++++++++++++++++++
 unit/Makefile                    |  1 +
 unit/util/variant.cpp            | 12 ++++++++++++
 6 files changed, 36 insertions(+), 1 deletion(-)
 create mode 100644 src/util/variant.h
 create mode 100644 unit/util/variant.cpp

diff --git a/CMakeLists.txt b/CMakeLists.txt
index 583d3a577b9..922cc70b062 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -113,6 +113,8 @@ if("${CMAKE_CXX_COMPILER_ID}" STREQUAL "Clang" OR
     endif()
 endif()
 
+add_subdirectory(lib/variant)
+
 add_subdirectory(src)
 add_subdirectory(regression)
 add_subdirectory(unit)
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt
index 4ae6f1ff10f..1eaa821ec2e 100644
--- a/src/util/CMakeLists.txt
+++ b/src/util/CMakeLists.txt
@@ -47,4 +47,4 @@ add_dependencies(util generate_version_cpp)
 
 generic_includes(util)
 
-target_link_libraries(util big-int langapi)
+target_link_libraries(util big-int langapi mpark_variant)
diff --git a/src/util/module_dependencies.txt b/src/util/module_dependencies.txt
index a0f86e99c8f..5d32e66b4b5 100644
--- a/src/util/module_dependencies.txt
+++ b/src/util/module_dependencies.txt
@@ -1,6 +1,8 @@
 big-int
 mach # system
 malloc # system
+mpark
 nonstd
 sys # system
 util
+
diff --git a/src/util/variant.h b/src/util/variant.h
new file mode 100644
index 00000000000..3d314e02869
--- /dev/null
+++ b/src/util/variant.h
@@ -0,0 +1,18 @@
+/*******************************************************************\
+
+Module: typedef for variant class template. To be replaced with
+        std::variant once C++17 support is enabled
+
+Author: Diffblue Ltd.
+
+\*******************************************************************/
+
+#ifndef CPROVER_UTIL_VARIANT_H
+#define CPROVER_UTIL_VARIANT_H
+
+#include <mpark/variant.hpp>
+
+template <typename... Ts>
+using variantt = mpark::variant<Ts...>;
+
+#endif // CPROVER_UTIL_VARIANT_H
diff --git a/unit/Makefile b/unit/Makefile
index d9eb73606ed..fe8c061f151 100644
--- a/unit/Makefile
+++ b/unit/Makefile
@@ -78,6 +78,7 @@ SRC += analyses/ai/ai.cpp \
        util/symbol_table.cpp \
        util/symbol.cpp \
        util/unicode.cpp \
+       util/variant.cpp \
        # Empty last line
 
 INCLUDES= -I ../src/ -I.
diff --git a/unit/util/variant.cpp b/unit/util/variant.cpp
new file mode 100644
index 00000000000..2b5d1f2411b
--- /dev/null
+++ b/unit/util/variant.cpp
@@ -0,0 +1,12 @@
+// Copyright 2016-2019 Diffblue Limited. All Rights Reserved.
+
+#include <testing-utils/use_catch.h>
+#include <util/variant.h>
+
+TEST_CASE("Ensure variant has been included", "[core][util][variant]")
+{
+  variantt<int, float> some_type = 1;
+  REQUIRE(some_type.index() == 0);
+  some_type = 1.0f;
+  REQUIRE(some_type.index() == 1);
+}