diff --git a/regression/cbmc/gcc_clz1/main.c b/regression/cbmc-library/__builtin_clz-01/main.c
similarity index 84%
rename from regression/cbmc/gcc_clz1/main.c
rename to regression/cbmc-library/__builtin_clz-01/main.c
index d5cc0260efc..fbae81294d8 100644
--- a/regression/cbmc/gcc_clz1/main.c
+++ b/regression/cbmc-library/__builtin_clz-01/main.c
@@ -1,9 +1,8 @@
 #include <assert.h>
 
-#ifndef __GNUC__
-int __builtin_clz(unsigned int);
-int __builtin_clzl(unsigned long);
-int __builtin_clzll(unsigned long long);
+#ifdef _MSC_VER
+#  define __builtin_clz(x) __lzcnt(x)
+#  define __builtin_clzll(x) __lzcnt64(x)
 #endif
 
 unsigned int __VERIFIER_nondet_unsigned();
@@ -39,10 +38,16 @@ int nlz2a(unsigned x)
 
 int main()
 {
+#ifdef _MSC_VER
+  unsigned short f = 42;
+  assert(__lzcnt16(f) == 10);
+#endif
   assert(nlz2a(42) == 26);
   assert(__builtin_clz(42) == 26);
+#ifndef _MSC_VER
   assert(
     __builtin_clzl(42) == 26 + (sizeof(unsigned long) - sizeof(unsigned)) * 8);
+#endif
   assert(
     __builtin_clzll(42) ==
     26 + (sizeof(unsigned long long) - sizeof(unsigned)) * 8);
diff --git a/regression/cbmc/gcc_clz1/test.desc b/regression/cbmc/gcc_clz1/test.desc
deleted file mode 100644
index 9efefbc7362..00000000000
--- a/regression/cbmc/gcc_clz1/test.desc
+++ /dev/null
@@ -1,8 +0,0 @@
-CORE
-main.c
-
-^EXIT=0$
-^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
---
-^warning: ignoring
diff --git a/src/ansi-c/library/windows.c b/src/ansi-c/library/windows.c
index 1c6b5e758bf..aa9ed115b62 100644
--- a/src/ansi-c/library/windows.c
+++ b/src/ansi-c/library/windows.c
@@ -51,3 +51,46 @@ inline HANDLE CreateThread(
   return handle;
 }
 #endif
+
+/* FUNCTION: __lzcnt16 */
+
+#ifdef _MSC_VER
+int __builtin_clz(unsigned int x);
+
+unsigned short __lzcnt16(unsigned short value)
+{
+  if(value == 0)
+    return 16;
+
+  return __builtin_clz(value) -
+         (sizeof(unsigned int) - sizeof(unsigned short)) * 8;
+}
+#endif
+
+/* FUNCTION: __lzcnt */
+
+#ifdef _MSC_VER
+int __builtin_clz(unsigned int x);
+
+unsigned int __lzcnt(unsigned int value)
+{
+  if(value == 0)
+    return 32;
+
+  return __builtin_clz(value);
+}
+#endif
+
+/* FUNCTION: __lzcnt64 */
+
+#ifdef _MSC_VER
+int __builtin_clzll(unsigned long long x);
+
+unsigned __int64 __lzcnt64(unsigned __int64 value)
+{
+  if(value == 0)
+    return 64;
+
+  return __builtin_clzll(value);
+}
+#endif