From 42edc4a72d8d50f008c8c2907ae9a7ca2686831c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 14 Oct 2013 11:27:47 -0700
Subject: [PATCH] test(set): add set of pointers test

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/tests/util/CMakeLists.txt |  3 +++
 src/tests/util/set.cpp        | 34 ++++++++++++++++++++++++++++++++++
 2 files changed, 37 insertions(+)
 create mode 100644 src/tests/util/set.cpp

diff --git a/src/tests/util/CMakeLists.txt b/src/tests/util/CMakeLists.txt
index 460117c73..b1f1697a1 100644
--- a/src/tests/util/CMakeLists.txt
+++ b/src/tests/util/CMakeLists.txt
@@ -58,3 +58,6 @@ add_test(hash ${CMAKE_CURRENT_BINARY_DIR}/hash)
 add_executable(safe_arith safe_arith.cpp)
 target_link_libraries(safe_arith ${EXTRA_LIBS})
 add_test(safe_arith ${CMAKE_CURRENT_BINARY_DIR}/safe_arith)
+add_executable(set set.cpp)
+target_link_libraries(set ${EXTRA_LIBS})
+add_test(set ${CMAKE_CURRENT_BINARY_DIR}/set)
diff --git a/src/tests/util/set.cpp b/src/tests/util/set.cpp
new file mode 100644
index 000000000..9394bbcb9
--- /dev/null
+++ b/src/tests/util/set.cpp
@@ -0,0 +1,34 @@
+/*
+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 <set>
+#include "util/test.h"
+using namespace lean;
+
+static void tst1() {
+    std::set<int*> s;
+    int a;
+    int b;
+    int c;
+    a = 10;
+    b = 20;
+    c = 5;
+    s.insert(&a);
+    s.insert(&b);
+    lean_assert(s.size() == 2);
+    s.insert(&a);
+    lean_assert(s.size() == 2);
+    s.insert(&c);
+    lean_assert(s.size() == 3);
+    for (int * v : s) {
+        std::cout << *v << "\n";
+    }
+}
+
+int main() {
+    tst1();
+    return has_violations() ? 1 : 0;
+}