From 9152aaa7d6db1bf1b300d89e2d75f301e37fd264 Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Mon, 5 Mar 2018 16:49:04 +0000
Subject: [PATCH] fix(bit_tricks): make sure no one calls math.h's log2() this
 fixes the bit_trick test with MSVC

---
 src/tests/util/bit_tricks.cpp | 28 ++++++++++++++--------------
 src/util/bit_tricks.cpp       |  8 ++++++++
 src/util/bit_tricks.h         |  1 +
 3 files changed, 23 insertions(+), 14 deletions(-)

diff --git a/src/tests/util/bit_tricks.cpp b/src/tests/util/bit_tricks.cpp
index c31c586e38..ca283669e7 100644
--- a/src/tests/util/bit_tricks.cpp
+++ b/src/tests/util/bit_tricks.cpp
@@ -9,20 +9,20 @@ Author: Leonardo de Moura
 using namespace lean;
 
 static void tst1() {
-    lean_assert(log2(255) == 7);
-    lean_assert(log2(256) == 8);
-    lean_assert(log2(257) == 8);
-    lean_assert(log2(321) == 8);
-    lean_assert(log2(520) == 9);
-    lean_assert(log2(65535) == 15);
-    lean_assert(log2(65536) == 16);
-    lean_assert(log2(65537) == 16);
-    lean_assert(log2(5203939) == 22);
-    lean_assert(log2(10309482) == 23);
-    lean_assert(log2(41039392) == 25);
-    lean_assert(log2(213469392) == 27);
-    lean_assert(log2(1293828727) == 30);
-    lean_assert(log2(1073741824) == 30);
+    lean_assert(log2(255u) == 7);
+    lean_assert(log2(256u) == 8);
+    lean_assert(log2(257u) == 8);
+    lean_assert(log2(321u) == 8);
+    lean_assert(log2(520u) == 9);
+    lean_assert(log2(65535u) == 15);
+    lean_assert(log2(65536u) == 16);
+    lean_assert(log2(65537u) == 16);
+    lean_assert(log2(5203939u) == 22);
+    lean_assert(log2(10309482u) == 23);
+    lean_assert(log2(41039392u) == 25);
+    lean_assert(log2(213469392u) == 27);
+    lean_assert(log2(1293828727u) == 30);
+    lean_assert(log2(1073741824u) == 30);
     lean_assert(log2(2147483648u) == 31);
     lean_assert(log2(4294967295u) == 31);
 }
diff --git a/src/util/bit_tricks.cpp b/src/util/bit_tricks.cpp
index 00b01cbe69..5519d83c9b 100644
--- a/src/util/bit_tricks.cpp
+++ b/src/util/bit_tricks.cpp
@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "util/debug.h"
+
 namespace lean {
 unsigned log2(unsigned v) {
     unsigned r = 0;
@@ -29,4 +31,10 @@ unsigned log2(unsigned v) {
     }
     return r;
 }
+
+// make sure no one calls the math.h log2 accidentally
+double log2(int v) {
+  (void)v;
+  lean_unreachable();
+}
 }
diff --git a/src/util/bit_tricks.h b/src/util/bit_tricks.h
index 0bffaff41e..c3a5a03f21 100644
--- a/src/util/bit_tricks.h
+++ b/src/util/bit_tricks.h
@@ -9,4 +9,5 @@ Author: Leonardo de Moura
 namespace lean {
 inline bool is_power_of_two(unsigned v) { return !(v & (v - 1)) && v; }
 unsigned log2(unsigned v);
+double log2(int v);
 }