From 1179b6b52b654500b086021f4e7bb15293e7d581 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 29 Sep 2013 17:03:48 -0700
Subject: [PATCH] test(hash): add missing tests

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

diff --git a/src/tests/util/CMakeLists.txt b/src/tests/util/CMakeLists.txt
index 3c3991e8ca..30b960428b 100644
--- a/src/tests/util/CMakeLists.txt
+++ b/src/tests/util/CMakeLists.txt
@@ -52,3 +52,6 @@ add_test(bit_tricks ${CMAKE_CURRENT_BINARY_DIR}/bit_tricks)
 add_executable(lazy_list lazy_list.cpp)
 target_link_libraries(lazy_list ${EXTRA_LIBS})
 add_test(lazy_list ${CMAKE_CURRENT_BINARY_DIR}/lazy_list)
+add_executable(hash hash.cpp)
+target_link_libraries(hash ${EXTRA_LIBS})
+add_test(hash ${CMAKE_CURRENT_BINARY_DIR}/hash)
diff --git a/src/tests/util/hash.cpp b/src/tests/util/hash.cpp
new file mode 100644
index 0000000000..2113fcfd97
--- /dev/null
+++ b/src/tests/util/hash.cpp
@@ -0,0 +1,23 @@
+/*
+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/hash.h"
+using namespace lean;
+
+static void tst1() {
+    int a[] = {0, 1, 2};
+    unsigned h3 = hash(3, [&](unsigned i) { return a[i]; });
+    lean_assert(h3 == hash(3, [&](unsigned i) { return a[i]; }));
+    unsigned h1 = hash(1, [&](unsigned i) { return a[i]; });
+    lean_assert(h1 != h3);
+}
+
+int main() {
+    tst1();
+    return has_violations() ? 1 : 0;
+}