diff --git a/src/tests/util/optional.cpp b/src/tests/util/optional.cpp
new file mode 100644
index 000000000..b859c4b45
--- /dev/null
+++ b/src/tests/util/optional.cpp
@@ -0,0 +1,48 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <iostream>
+#include "util/test.h"
+#include "util/optional.h"
+using namespace lean;
+
+struct point {
+    std::string m_msg;
+    int m_x;
+    int m_y;
+    point(char const * msg, int x, int y):m_msg(msg), m_x(x), m_y(y) {}
+    point(point const & p):m_msg(p.m_msg), m_x(p.m_x), m_y(p.m_y) {}
+    point(point && p):m_msg(std::move(p.m_msg)), m_x(p.m_x), m_y(p.m_y) {}
+    ~point() { std::cout << "destructed... " << m_msg << " " << m_x << " " << m_y << "\n"; }
+};
+
+static void tst1() {
+    optional<int> i;
+    lean_assert(!i);
+    i = 10;
+    lean_assert(i);
+    lean_assert(*i == 10);
+}
+
+static void tst2() {
+    optional<point> p1;
+    lean_assert(!p1);
+    optional<point> p2("p2", 10, 20);
+    lean_assert(p2->m_x == 10);
+    p2 = point("p3", 20, 30);
+    lean_assert(p2->m_y == 30);
+    lean_assert((*p2).m_x == 20);
+    p1 = p2;
+    lean_assert(p1);
+    lean_assert(p1.value().m_x == 20);
+    p1.emplace("p4", 2, 3);
+}
+
+int main() {
+    tst1();
+    tst2();
+    return has_violations() ? 1 : 0;
+}
diff --git a/src/util/optional.h b/src/util/optional.h
new file mode 100644
index 000000000..d2e2fabc5
--- /dev/null
+++ b/src/util/optional.h
@@ -0,0 +1,99 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "util/debug.h"
+
+namespace lean {
+/**
+   \brief Simple optional template. This is a naive replacement for C++14 optional.
+   We will delete it as soon optional is supported in g++ and clang++.
+*/
+template<typename T>
+class optional {
+    bool m_some;
+    union {
+        T m_value;
+    };
+public:
+    optional():m_some(false) {}
+    optional(T const & v):m_some(true) {
+        new (&m_value) T(v);
+    }
+    template<typename... Args>
+    optional(Args&&... args):m_some(true) {
+        new (&m_value) T(args...);
+    }
+    optional(optional const & other):m_some(other.m_some) {
+        if (m_some)
+            new (&m_value) T(other.m_value);
+    }
+    optional(optional && other):m_some(other.m_some) {
+        if (m_some)
+            m_value = std::move(other.m_value);
+    }
+    ~optional() {
+        if (m_some)
+            m_value.~T();
+    }
+
+    operator bool() const { return m_some; }
+    T const * operator->() const { lean_assert(m_some); return &m_value; }
+    T * operator->() { lean_assert(m_some); return &m_value; }
+    T const & operator*() const { lean_assert(m_some); return m_value; }
+    T & operator*() { lean_assert(m_some); return m_value; }
+    T const & value() const { lean_assert(m_some); return m_value; }
+    T & value() { lean_assert(m_some); return m_value; }
+
+    template<typename... Args>
+    void emplace(Args&&... args) {
+        if (m_some)
+            m_value.~T();
+        new (&m_value) T(args...);
+    }
+
+    optional& operator=(optional const & other) {
+        if (this == &other)
+            return *this;
+        if (m_some)
+            m_value.~T();
+        m_some = other.m_some;
+        if (m_some)
+            new (&m_value) T(other.m_value);
+        return *this;
+    }
+    optional& operator=(optional && other) {
+        lean_assert(this != &other);
+        if (m_some)
+            m_value.~T();
+        m_some = other.m_some;
+        if (m_some)
+            new (&m_value) T(std::forward<T>(other.m_value));
+        return *this;
+    }
+    optional& operator=(T const & other) {
+        if (m_some)
+            m_value.~T();
+        m_some = true;
+        new (&m_value) T(other.m_value);
+        return *this;
+    }
+    optional& operator=(T && other) {
+        if (m_some)
+            m_value.~T();
+        m_some = true;
+        new (&m_value) T(std::forward<T>(other));
+        return *this;
+    }
+
+    friend bool operator==(optional const & o1, optional const & o2) {
+        if (o1.m_some != o2.m_some)
+            return false;
+        else
+            return !o1.m_some || o1.m_value == o2.m_value;
+    }
+};
+}