diff --git a/CMakeLists.txt b/CMakeLists.txt
index e5619ddc5..64efaf72d 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -1,17 +1,8 @@
 # Enforce some CMake policies
-cmake_minimum_required(VERSION 2.8.12)
+cmake_minimum_required(VERSION 3.4)
+
 if (POLICY CMP0054)
-  # FIXME: This is horrible. With the old behaviour,
-  # quoted strings like "MSVC" in if() conditionals
-  # get implicitly dereferenced. The NEW behaviour
-  # doesn't do this but CMP0054 was only introduced
-  # in CMake 3.1 and we support lower versions as the
-  # minimum. We could set NEW here but it would be very
-  # confusing to use NEW for some builds and OLD for others
-  # which could lead to some subtle bugs. Instead when the
-  # minimum version is 3.1 change this policy to NEW and remove
-  # the hacks in place to work around it.
-  cmake_policy(SET CMP0054 OLD)
+  cmake_policy(SET CMP0054 NEW)
 endif()
 
 if (POLICY CMP0042)
@@ -22,13 +13,6 @@ endif()
 set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake")
 project(Z3 CXX)
 
-if ("${CMAKE_VERSION}" VERSION_LESS "3.4")
-  # FIXME: Drop this when we upgrade to newer CMake versions.
-  # HACK: Although we don't need C language support if it is not
-  # enabled CMake's `FindThreads` module fails in old CMake versions.
-  enable_language(C)
-endif()
-
 ################################################################################
 # Project version
 ################################################################################
@@ -352,12 +336,11 @@ if (("${TARGET_ARCHITECTURE}" STREQUAL "x86_64") OR ("${TARGET_ARCHITECTURE}" ST
       list(APPEND Z3_DEPENDENT_LIBS "iomp5")
     endif()
     set(SSE_FLAGS "-mfpmath=sse" "-msse" "-msse2")
-    # FIXME: Remove "x.." when CMP0054 is set to NEW
   elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Intel")
     set(SSE_FLAGS "-mfpmath=sse" "-msse" "-msse2")
     # Intel's compiler requires linking with libiomp5 
     list(APPEND Z3_DEPENDENT_LIBS "iomp5") 
-  elseif ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC")
+  elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
     set(SSE_FLAGS "/arch:SSE2")
   else()
     message(FATAL_ERROR "Unknown compiler ${CMAKE_CXX_COMPILER_ID}")
@@ -369,17 +352,6 @@ if (("${TARGET_ARCHITECTURE}" STREQUAL "x86_64") OR ("${TARGET_ARCHITECTURE}" ST
   unset(SSE_FLAGS)
 endif()
 
-
-
-# FIXME: Remove "x.." when CMP0054 is set to NEW
-if ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC")
-  # This is the default for MSVC already but to replicate the
-  # python/Makefile build system behaviour this flag is set
-  # explicitly.
-  z3_add_cxx_flag("/fp:precise" REQUIRED)
-endif()
-# There doesn't seem to be an equivalent for clang/gcc
-
 ################################################################################
 # Threading support
 ################################################################################
@@ -493,8 +465,7 @@ endif()
 ################################################################################
 # MSVC specific flags inherited from old build system
 ################################################################################
-# FIXME: Remove "x.." when CMP0054 is set to NEW
-if ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC")
+if ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
   include(${CMAKE_SOURCE_DIR}/cmake/msvc_legacy_quirks.cmake)
 endif()
 
diff --git a/cmake/compiler_lto.cmake b/cmake/compiler_lto.cmake
index b90890f59..b4eb83e18 100644
--- a/cmake/compiler_lto.cmake
+++ b/cmake/compiler_lto.cmake
@@ -22,8 +22,7 @@ if (LINK_TIME_OPTIMIZATION)
       ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU"))
       set(_lto_compiler_flag "-flto")
       set(_lto_linker_flag "-flto")
-  # FIXME: Remove "x.." when CMP0054 is set to NEW
-  elseif ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC")
+  elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
     set(_lto_compiler_flag "/GL")
     set(_lto_linker_flag "/LTCG")
   else()
diff --git a/cmake/compiler_warnings.cmake b/cmake/compiler_warnings.cmake
index 183f490dd..983325796 100644
--- a/cmake/compiler_warnings.cmake
+++ b/cmake/compiler_warnings.cmake
@@ -56,8 +56,7 @@ elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang")
   list(APPEND WARNING_FLAGS_TO_CHECK ${CLANG_ONLY_WARNINGS})
   list(APPEND WARNING_AS_ERROR_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS_AS_ERRORS})
   list(APPEND WARNING_AS_ERROR_FLAGS_TO_CHECK ${CLANG_WARNINGS_AS_ERRORS})
-  # FIXME: Remove "x.." when CMP0054 is set to NEW
-elseif ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC")
+elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
   list(APPEND WARNING_FLAGS_TO_CHECK ${MSVC_WARNINGS})
 
   # CMake's default flags include /W3 already so remove them if
@@ -111,8 +110,7 @@ if ("${WARNINGS_AS_ERRORS}" STREQUAL "ON")
   message(STATUS "Treating compiler warnings as errors")
   if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU"))
     list(APPEND Z3_COMPONENT_CXX_FLAGS "-Werror")
-    # FIXME: Remove "x.." when CMP0054 is set to NEW
-  elseif ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC")
+  elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
     list(APPEND Z3_COMPONENT_CXX_FLAGS "/WX")
   else()
     message(AUTHOR_WARNING "Unknown compiler")
@@ -126,8 +124,7 @@ elseif ("${WARNINGS_AS_ERRORS}" STREQUAL "SERIOUS_ONLY")
   endforeach()
 elseif ("${WARNINGS_AS_ERRORS}" STREQUAL "OFF")
   message(STATUS "Not treating compiler warnings as errors")
-  # FIXME: Remove "x.." when CMP0054 is set to NEW
-  if ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC")
+  if ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
     # Warnings as errors is off by default for MSVC so setting this
     # is not necessary but this duplicates the behaviour of the old
     # build system.
diff --git a/cmake/msvc_legacy_quirks.cmake b/cmake/msvc_legacy_quirks.cmake
index a8006e2d3..d34351c1d 100644
--- a/cmake/msvc_legacy_quirks.cmake
+++ b/cmake/msvc_legacy_quirks.cmake
@@ -69,14 +69,6 @@ list(APPEND Z3_COMPONENT_CXX_DEFINES ${Z3_MSVC_LEGACY_DEFINES})
 ################################################################################
 # Compiler flags
 ################################################################################
-# By default in MSVC this is on but the old build system set this explicitly so
-# for completeness set it too.
-# See https://msdn.microsoft.com/en-us/library/dh8che7s.aspx
-z3_add_cxx_flag("/Zc:wchar_t" REQUIRED)
-# By default in MSVC this on but the old build system set this explicitly so
-# for completeness set it too.
-z3_add_cxx_flag("/Zc:forScope" REQUIRED)
-
 # FIXME: We might want to move this out somewhere else if we decide
 # we want to set `-fno-omit-frame-pointer` for gcc/clang.
 # No omit frame pointer
@@ -106,11 +98,6 @@ if (("${TARGET_ARCHITECTURE}" STREQUAL "x86_64") OR ("${TARGET_ARCHITECTURE}" ST
   z3_add_cxx_flag("/Gd" REQUIRED)
 endif()
 
-# FIXME: The old build system explicitly disables code analysis.
-# I don't know why. Duplicate this behaviour for now.
-# See https://msdn.microsoft.com/en-us/library/ms173498.aspx
-z3_add_cxx_flag("/analyze-" REQUIRED)
-
 ################################################################################
 # Linker flags
 ################################################################################
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index ffbf13010..5397bd80f 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -2725,7 +2725,7 @@ def mk_config():
                 'SLINK_FLAGS=/nologo /LDd\n' % static_opt)
             if VS_X64:
                 config.write(
-                    'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- %s %s\n' % (extra_opt, static_opt))
+                    'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /GS /Gd %s %s\n' % (extra_opt, static_opt))
                 config.write(
                     'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n'
                     'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (link_extra_opt, maybe_disable_dynamic_base, link_extra_opt))
@@ -2734,7 +2734,7 @@ def mk_config():
                 exit(1)
             else:
                 config.write(
-                    'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2 %s %s\n' % (extra_opt, static_opt))
+                    'CXXFLAGS=/c /Zi /nologo /W3 /WX- /Od /Oy- /D WIN32 /D _DEBUG /D Z3DEBUG /D _CONSOLE /D _TRACE /D _WINDOWS /Gm- /EHsc /RTC1 /GS /Gd /arch:SSE2 %s %s\n' % (extra_opt, static_opt))
                 config.write(
                     'LINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n'
                     'SLINK_EXTRA_FLAGS=/link /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (link_extra_opt, maybe_disable_dynamic_base, link_extra_opt))
@@ -2750,7 +2750,7 @@ def mk_config():
                 extra_opt = '%s /D _TRACE ' % extra_opt
             if VS_X64:
                 config.write(
-                    'CXXFLAGS=/c%s /Zi /nologo /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG /D _LIB /D _WINDOWS /D _UNICODE /D UNICODE /Gm- /EHsc /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /TP %s %s\n' % (GL, extra_opt, static_opt))
+                    'CXXFLAGS=/c%s /Zi /nologo /W3 /WX- /O2 /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG /D _LIB /D _WINDOWS /D _UNICODE /D UNICODE /Gm- /EHsc /GS /Gd /TP %s %s\n' % (GL, extra_opt, static_opt))
                 config.write(
                     'LINK_EXTRA_FLAGS=/link%s /MACHINE:X64 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 %s\n'
                     'SLINK_EXTRA_FLAGS=/link%s /MACHINE:X64 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 %s\n' % (LTCG, link_extra_opt, LTCG, link_extra_opt))
@@ -2759,7 +2759,7 @@ def mk_config():
                 exit(1)
             else:
                 config.write(
-                    'CXXFLAGS=/nologo /c%s /Zi /W3 /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG /D _CONSOLE /D _WINDOWS /D ASYNC_COMMANDS /Gm- /EHsc /GS /fp:precise /Zc:wchar_t /Zc:forScope /Gd /analyze- /arch:SSE2 %s %s\n' % (GL, extra_opt, static_opt))
+                    'CXXFLAGS=/nologo /c%s /Zi /W3 /WX- /O2 /Oy- /D _EXTERNAL_RELEASE /D WIN32 /D NDEBUG /D _CONSOLE /D _WINDOWS /D ASYNC_COMMANDS /Gm- /EHsc /GS /Gd /arch:SSE2 %s %s\n' % (GL, extra_opt, static_opt))
                 config.write(
                     'LINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:CONSOLE /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 /DYNAMICBASE /NXCOMPAT %s\n'
                     'SLINK_EXTRA_FLAGS=/link%s /DEBUG /MACHINE:X86 /SUBSYSTEM:WINDOWS /INCREMENTAL:NO /STACK:8388608 /OPT:REF /OPT:ICF /TLBID:1 %s %s\n' % (LTCG, link_extra_opt, LTCG, maybe_disable_dynamic_base, link_extra_opt))