diff --git a/CMakeLists.txt b/CMakeLists.txt
index 87596c60a..561da3595 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -1,15 +1,6 @@
 # Enforce some CMake policies
 cmake_minimum_required(VERSION 3.4)
 
-if (POLICY CMP0054)
-  cmake_policy(SET CMP0054 NEW)
-endif()
-
-if (POLICY CMP0042)
-  # Enable `MACOSX_RPATH` by default.
-  cmake_policy(SET CMP0042 NEW)
-endif()
-
 set(CMAKE_USER_MAKE_RULES_OVERRIDE_CXX "${CMAKE_CURRENT_SOURCE_DIR}/cmake/cxx_compiler_flags_overrides.cmake")
 project(Z3 VERSION 4.8.11.0 LANGUAGES CXX)
 
@@ -42,7 +33,7 @@ set(z3_polluted_tree_msg
 ################################################################################
 # Sanity check - Disallow building in source
 ################################################################################
-if ("${PROJECT_SOURCE_DIR}" STREQUAL "${PROJECT_BINARY_DIR}")
+if (PROJECT_SOURCE_DIR STREQUAL PROJECT_BINARY_DIR)
   message(FATAL_ERROR "In source builds are not allowed. You should invoke "
           "CMake from a different directory.")
 endif()
@@ -194,28 +185,28 @@ set(CMAKE_CXX_STANDARD_REQUIRED ON)
 ################################################################################
 # Platform detection
 ################################################################################
-if ("${CMAKE_SYSTEM_NAME}" STREQUAL "Linux")
+if (CMAKE_SYSTEM_NAME STREQUAL "Linux")
   message(STATUS "Platform: Linux")
   list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_LINUX_")
-  if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64")
+  if (TARGET_ARCHITECTURE STREQUAL "x86_64")
     list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_USE_THREAD_LOCAL")
   endif()
-elseif ("${CMAKE_SYSTEM_NAME}" STREQUAL "Android")
+elseif (CMAKE_SYSTEM_NAME STREQUAL "Android")
   message(STATUS "Platform: Android")
   list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_ANDROID_")
-elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "GNU")
+elseif (CMAKE_SYSTEM_NAME MATCHES "GNU")
   message(STATUS "Platform: GNU/Hurd")
   list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_HURD_")
-elseif ("${CMAKE_SYSTEM_NAME}" STREQUAL "Darwin")
+elseif (CMAKE_SYSTEM_NAME STREQUAL "Darwin")
   # Does macOS really not need any special flags?
   message(STATUS "Platform: Darwin")
-elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "FreeBSD")
+elseif (CMAKE_SYSTEM_NAME MATCHES "FreeBSD")
   message(STATUS "Platform: FreeBSD")
   list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_FREEBSD_")
-elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "NetBSD")
+elseif (CMAKE_SYSTEM_NAME MATCHES "NetBSD")
   message(STATUS "Platform: NetBSD")
   list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_NetBSD_")
-elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "OpenBSD")
+elseif (CMAKE_SYSTEM_NAME MATCHES "OpenBSD")
   message(STATUS "Platform: OpenBSD")
   list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_OPENBSD_")
 elseif (CYGWIN)
@@ -251,8 +242,7 @@ if (Z3_USE_LIB_GMP)
   # can't be found
   find_package(GMP REQUIRED)
   message(STATUS "Using libgmp")
-  list(APPEND Z3_DEPENDENT_LIBS ${GMP_C_LIBRARIES})
-  list(APPEND Z3_COMPONENT_EXTRA_INCLUDE_DIRS ${GMP_INCLUDE_DIRS})
+  list(APPEND Z3_DEPENDENT_LIBS GMP::GMP)
   list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_MP_GMP")
 else()
   list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_MP_INTERNAL")
@@ -292,18 +282,18 @@ endif()
 # FP math
 ################################################################################
 # FIXME: Support ARM "-mfpu=vfp -mfloat-abi=hard"
-if (("${TARGET_ARCHITECTURE}" STREQUAL "x86_64") OR ("${TARGET_ARCHITECTURE}" STREQUAL "i686"))
-  if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Intel"))
-    if ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Intel")
+if ((TARGET_ARCHITECTURE STREQUAL "x86_64") OR (TARGET_ARCHITECTURE STREQUAL "i686"))
+  if ((CMAKE_CXX_COMPILER_ID MATCHES "GNU") OR (CMAKE_CXX_COMPILER_ID MATCHES "Clang") OR (CMAKE_CXX_COMPILER_ID MATCHES "Intel"))
+    if (CMAKE_CXX_COMPILER_ID MATCHES "Intel")
       # Intel's compiler requires linking with libiomp5
       list(APPEND Z3_DEPENDENT_LIBS "iomp5")
     endif()
     set(SSE_FLAGS "-mfpmath=sse" "-msse" "-msse2")
-  elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Intel")
+  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 ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
+  elseif (CMAKE_CXX_COMPILER_ID STREQUAL "MSVC")
     set(SSE_FLAGS "/arch:SSE2")
   else()
     message(FATAL_ERROR "Unknown compiler ${CMAKE_CXX_COMPILER_ID}")
@@ -320,7 +310,7 @@ endif()
 ################################################################################
 set(THREADS_PREFER_PTHREAD_FLAG TRUE)
 find_package(Threads)
-list(APPEND Z3_DEPENDENT_LIBS ${CMAKE_THREAD_LIBS_INIT})
+list(APPEND Z3_DEPENDENT_LIBS Threads::Threads)
 
 ################################################################################
 # Compiler warnings
@@ -411,7 +401,7 @@ if (Z3_ENABLE_CFI)
   if ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang")
     z3_add_cxx_flag("-fsanitize=cfi" REQUIRED)
     z3_add_cxx_flag("-fsanitize-cfi-cross-dso" REQUIRED)
-  elseif ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC")
+  elseif (CMAKE_CXX_COMPILER_ID STREQUAL "MSVC")
     z3_add_cxx_flag("/guard:cf" REQUIRED)
     message(STATUS "Enabling CFI for MSVC")
     foreach (_build_type ${build_types_with_cfi})
@@ -428,14 +418,14 @@ endif()
 ################################################################################
 # MSVC specific flags inherited from old build system
 ################################################################################
-if ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
+if (CMAKE_CXX_COMPILER_ID STREQUAL "MSVC")
   include(${PROJECT_SOURCE_DIR}/cmake/msvc_legacy_quirks.cmake)
 endif()
 
 ################################################################################
 # Pass /RELEASE to the linker so that checksums in PE files are calculated.
 ################################################################################
-if ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
+if (CMAKE_CXX_COMPILER_ID STREQUAL "MSVC")
   string(APPEND CMAKE_EXE_LINKER_FLAGS " /RELEASE")
   string(APPEND CMAKE_SHARED_LINKER_FLAGS " /RELEASE")
 endif()
diff --git a/cmake/compiler_lto.cmake b/cmake/compiler_lto.cmake
index 1fa7ca8d3..abb7fb401 100644
--- a/cmake/compiler_lto.cmake
+++ b/cmake/compiler_lto.cmake
@@ -18,11 +18,11 @@ if (Z3_LINK_TIME_OPTIMIZATION)
 
   set(_lto_compiler_flag "")
   set(_lto_linker_flag "")
-  if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR
-      ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU"))
+  if ((CMAKE_CXX_COMPILER_ID MATCHES "Clang") OR
+      (CMAKE_CXX_COMPILER_ID MATCHES "GNU"))
       set(_lto_compiler_flag "-flto")
       set(_lto_linker_flag "-flto")
-  elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
+  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 983325796..4a5819fe0 100644
--- a/cmake/compiler_warnings.cmake
+++ b/cmake/compiler_warnings.cmake
@@ -46,22 +46,22 @@ set(CLANG_WARNINGS_AS_ERRORS
 ################################################################################
 set(WARNING_FLAGS_TO_CHECK "")
 set(WARNING_AS_ERROR_FLAGS_TO_CHECK "")
-if ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU")
+if (CMAKE_CXX_COMPILER_ID MATCHES "GNU")
   list(APPEND WARNING_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS})
   list(APPEND WARNING_FLAGS_TO_CHECK ${GCC_ONLY_WARNINGS})
   list(APPEND WARNING_AS_ERROR_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS_AS_ERRORS})
   list(APPEND WARNING_AS_ERROR_FLAGS_TO_CHECK ${GCC_WARNINGS_AS_ERRORS})
-elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang")
+elseif (CMAKE_CXX_COMPILER_ID MATCHES "Clang")
   list(APPEND WARNING_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS})
   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})
-elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
+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
   # they already exist.
-  if ("${CMAKE_CXX_FLAGS}" MATCHES "/W3")
+  if (CMAKE_CXX_FLAGS MATCHES "/W3")
     string(REPLACE "/W3" "" _cmake_cxx_flags_remove_w3 "${CMAKE_CXX_FLAGS}")
     set(CMAKE_CXX_FLAGS "${_cmake_cxx_flags_remove_w3}" CACHE STRING "" FORCE)
   endif()
@@ -84,7 +84,7 @@ get_property(
   PROPERTY
   TYPE
 )
-if ("${WARNINGS_AS_ERRORS_CACHE_VAR_TYPE}" STREQUAL "BOOL")
+if (WARNINGS_AS_ERRORS_CACHE_VAR_TYPE STREQUAL "BOOL")
   message(WARNING "Detected legacy WARNINGS_AS_ERRORS option. Upgrading")
   set(WARNINGS_AS_ERRORS_DEFAULT "${WARNINGS_AS_ERRORS}")
   # Delete old entry
@@ -106,25 +106,25 @@ set_property(
   "ON;OFF;SERIOUS_ONLY"
 )
 
-if ("${WARNINGS_AS_ERRORS}" STREQUAL "ON")
+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"))
+  if ((CMAKE_CXX_COMPILER_ID MATCHES "Clang") OR (CMAKE_CXX_COMPILER_ID MATCHES "GNU"))
     list(APPEND Z3_COMPONENT_CXX_FLAGS "-Werror")
-  elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
+  elseif (CMAKE_CXX_COMPILER_ID STREQUAL "MSVC")
     list(APPEND Z3_COMPONENT_CXX_FLAGS "/WX")
   else()
     message(AUTHOR_WARNING "Unknown compiler")
   endif()
-elseif ("${WARNINGS_AS_ERRORS}" STREQUAL "SERIOUS_ONLY")
+elseif (WARNINGS_AS_ERRORS STREQUAL "SERIOUS_ONLY")
   message(STATUS "Treating only serious compiler warnings as errors")
   # Loop through the flags
   foreach (flag ${WARNING_AS_ERROR_FLAGS_TO_CHECK})
     # Add globally because some flags need to be passed at link time.
     z3_add_cxx_flag("${flag}" GLOBAL)
   endforeach()
-elseif ("${WARNINGS_AS_ERRORS}" STREQUAL "OFF")
+elseif (WARNINGS_AS_ERRORS STREQUAL "OFF")
   message(STATUS "Not treating compiler warnings as errors")
-  if ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "MSVC")
+  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/git_utils.cmake b/cmake/git_utils.cmake
index ea091eb6e..9582012a0 100644
--- a/cmake/git_utils.cmake
+++ b/cmake/git_utils.cmake
@@ -26,7 +26,7 @@ function(add_git_dir_dependency GIT_DOT_FILE SUCCESS_VAR)
     # git directory
     file(READ "${GIT_DOT_FILE}" GIT_DOT_FILE_DATA LIMIT 512)
     string(STRIP "${GIT_DOT_FILE_DATA}" GIT_DOT_FILE_DATA_STRIPPED)
-    if ("${GIT_DOT_FILE_DATA_STRIPPED}" MATCHES "^gitdir:[ ]*(.+)$")
+    if (GIT_DOT_FILE_DATA_STRIPPED MATCHES "^gitdir:[ ]*(.+)$")
       # Git worktree
       message(STATUS "Found git worktree")
       set(GIT_WORKTREE_DIR "${CMAKE_MATCH_1}")
@@ -75,7 +75,7 @@ function(add_git_dir_dependency GIT_DOT_FILE SUCCESS_VAR)
   file(READ "${GIT_HEAD_FILE}" GIT_HEAD_DATA LIMIT 128)
   string(STRIP "${GIT_HEAD_DATA}" GIT_HEAD_DATA_STRIPPED)
 
-  if ("${GIT_HEAD_DATA_STRIPPED}" MATCHES "^ref:[ ]*(.+)$")
+  if (GIT_HEAD_DATA_STRIPPED MATCHES "^ref:[ ]*(.+)$")
     # HEAD points at a reference.
     set(GIT_REF "${CMAKE_MATCH_1}")
     if (EXISTS "${GIT_DIR}/${GIT_REF}")
diff --git a/cmake/modules/FindGMP.cmake b/cmake/modules/FindGMP.cmake
index b749750ef..7e771c549 100644
--- a/cmake/modules/FindGMP.cmake
+++ b/cmake/modules/FindGMP.cmake
@@ -13,52 +13,37 @@ find_library(GMP_C_LIBRARIES
   NAMES gmp
   DOC "GMP C libraries"
 )
-if (GMP_C_LIBRARIES)
-  message(STATUS "Found GMP C library: \"${GMP_C_LIBRARIES}\"")
-else()
-  message(STATUS "Could not find GMP C library")
-endif()
 find_library(GMP_CXX_LIBRARIES
   NAMES gmpxx
   DOC "GMP C++ libraries"
 )
-if (GMP_CXX_LIBRARIES)
-  message(STATUS "Found GMP C++ library: \"${GMP_CXX_LIBRARIES}\"")
-else()
-  message(STATUS "Could not find GMP C++ library")
-endif()
 
 # Try to find headers
 find_path(GMP_C_INCLUDES
   NAMES gmp.h
   DOC "GMP C header"
 )
-if (GMP_C_INCLUDES)
-  message(STATUS "Found GMP C include path: \"${GMP_C_INCLUDES}\"")
-else()
-  message(STATUS "Could not find GMP C include path")
-endif()
 
 find_path(GMP_CXX_INCLUDES
   NAMES gmpxx.h
   DOC "GMP C++ header"
 )
-if (GMP_CXX_INCLUDES)
-  message(STATUS "Found GMP C++ include path: \"${GMP_CXX_INCLUDES}\"")
-else()
-  message(STATUS "Could not find GMP C++ include path")
-endif()
-
-if (GMP_C_LIBRARIES AND GMP_CXX_LIBRARIES AND GMP_C_INCLUDES AND GMP_CXX_INCLUDES)
-  set(GMP_INCLUDE_DIRS "${GMP_C_INCLUDES}" "${GMP_CXX_INCLUDES}")
-  list(REMOVE_DUPLICATES GMP_INCLUDE_DIRS)
-  message(STATUS "Found GMP")
-else()
-  message(STATUS "Could not find GMP")
-endif()
 
 # TODO: We should check we can link some simple code against libgmp and libgmpxx
 
 # Handle QUIET and REQUIRED and check the necessary variables were set and if so
 # set ``GMP_FOUND``
-find_package_handle_standard_args(GMP DEFAULT_MSG GMP_INCLUDE_DIRS GMP_C_LIBRARIES GMP_CXX_LIBRARIES)
+find_package_handle_standard_args(GMP
+	REQUIRED_VARS GMP_C_LIBRARIES GMP_C_INCLUDES GMP_CXX_LIBRARIES GMP_CXX_INCLUDES)
+
+if (GMP_FOUND)
+  set(GMP_INCLUDE_DIRS "${GMP_C_INCLUDES}" "${GMP_CXX_INCLUDES}")
+  list(REMOVE_DUPLICATES GMP_INCLUDE_DIRS)
+
+  if (NOT TARGET GMP::GMP)
+    add_library(GMP::GMP UNKNOWN IMPORTED)
+    set_target_properties(GMP::GMP PROPERTIES
+      INTERFACE_INCLUDE_DIRECTORIES "${GMP_C_INCLUDES}"
+      IMPORTED_LOCATION "${GMP_C_LIBRARIES}")
+  endif()
+endif()
diff --git a/cmake/msvc_legacy_quirks.cmake b/cmake/msvc_legacy_quirks.cmake
index 25e9b56c1..0239f0c4a 100644
--- a/cmake/msvc_legacy_quirks.cmake
+++ b/cmake/msvc_legacy_quirks.cmake
@@ -22,7 +22,7 @@ set(Z3_MSVC_LEGACY_DEFINES
   _UNICODE
 )
 
-if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64")
+if (TARGET_ARCHITECTURE STREQUAL "x86_64")
   list(APPEND Z3_MSVC_LEGACY_DEFINES ""
     # Don't set `_LIB`. The old build system sets this for x86_64 release
     # build. This flag doesn't seem to be documented but a stackoverflow
@@ -57,10 +57,10 @@ endif()
 # Note we don't set WIN32 or _WINDOWS because
 # CMake provides that for us. As a sanity check make sure the option
 # is present.
-if (NOT "${CMAKE_CXX_FLAGS}" MATCHES "[-/]D[ ]*WIN32")
+if (NOT CMAKE_CXX_FLAGS MATCHES "[-/]D[ ]*WIN32")
   message(FATAL_ERROR "\"/D WIN32\" is missing")
 endif()
-if (NOT "${CMAKE_CXX_FLAGS}" MATCHES "[-/]D[ ]*_WINDOWS")
+if (NOT CMAKE_CXX_FLAGS MATCHES "[-/]D[ ]*_WINDOWS")
   message(FATAL_ERROR "\"/D _WINDOWS\" is missing")
 endif()
 
@@ -82,7 +82,7 @@ endif()
 # build system kept the frame pointer for all configurations
 # except x86_64 release (I don't know why the frame pointer
 # is kept for i686 release).
-if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64")
+if (TARGET_ARCHITECTURE STREQUAL "x86_64")
   list(APPEND Z3_COMPONENT_CXX_FLAGS
     $<$<CONFIG:Debug>:${NO_OMIT_FRAME_POINTER_MSVC_FLAG}>
     $<$<CONFIG:MinSizeRel>:${NO_OMIT_FRAME_POINTER_MSVC_FLAG}>
@@ -91,7 +91,7 @@ else()
   list(APPEND Z3_COMPONENT_CXX_FLAGS ${NO_OMIT_FRAME_POINTER_MSVC_FLAG})
 endif()
 
-if (("${TARGET_ARCHITECTURE}" STREQUAL "x86_64") OR ("${TARGET_ARCHITECTURE}" STREQUAL "i686"))
+if ((TARGET_ARCHITECTURE STREQUAL "x86_64") OR (TARGET_ARCHITECTURE STREQUAL "i686"))
   # Use __cdecl calling convention. Apparently this is MSVC's default
   # but the old build system set it so for completeness set it too.
   # See https://msdn.microsoft.com/en-us/library/46t77ak2.aspx
@@ -153,9 +153,9 @@ string(APPEND CMAKE_SHARED_LINKER_FLAGS " /SUBSYSTEM:WINDOWS")
 # in the old build system except release x86_64. We try to emulate this here but
 # this is likely the wrong thing to do.
 foreach (_build_type ${_build_types_as_upper})
-  if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64" AND
-      ("${_build_type}" STREQUAL "RELEASE" OR
-      "${_build_type}"  STREQUAL "RELWITHDEBINFO")
+  if (TARGET_ARCHITECTURE STREQUAL "x86_64" AND
+      (_build_type STREQUAL "RELEASE" OR
+      _build_type  STREQUAL "RELWITHDEBINFO")
       )
     message(AUTHOR_WARNING "Skipping legacy linker MSVC options for x86_64 ${_build_type}")
   else()
diff --git a/examples/c++/CMakeLists.txt b/examples/c++/CMakeLists.txt
index a71fd061a..6223ea7c7 100644
--- a/examples/c++/CMakeLists.txt
+++ b/examples/c++/CMakeLists.txt
@@ -28,7 +28,7 @@ add_executable(cpp_example example.cpp)
 target_include_directories(cpp_example PRIVATE ${Z3_CXX_INCLUDE_DIRS})
 target_link_libraries(cpp_example PRIVATE ${Z3_LIBRARIES})
 
-if ("${CMAKE_SYSTEM_NAME}" MATCHES "[Ww]indows")
+if (CMAKE_SYSTEM_NAME MATCHES "[Ww]indows")
   # On Windows we need to copy the Z3 libraries
   # into the same directory as the executable
   # so that they can be found.
diff --git a/examples/c/CMakeLists.txt b/examples/c/CMakeLists.txt
index 943858347..612e7b791 100644
--- a/examples/c/CMakeLists.txt
+++ b/examples/c/CMakeLists.txt
@@ -40,7 +40,7 @@ endif()
 target_include_directories(c_example PRIVATE ${Z3_C_INCLUDE_DIRS})
 target_link_libraries(c_example PRIVATE ${Z3_LIBRARIES})
 
-if ("${CMAKE_SYSTEM_NAME}" MATCHES "[Ww]indows")
+if (CMAKE_SYSTEM_NAME MATCHES "[Ww]indows")
   # On Windows we need to copy the Z3 libraries
   # into the same directory as the executable
   # so that they can be found.
diff --git a/examples/dotnet/CMakeLists.txt b/examples/dotnet/CMakeLists.txt
index 83b0f2ccf..b07ae4219 100644
--- a/examples/dotnet/CMakeLists.txt
+++ b/examples/dotnet/CMakeLists.txt
@@ -1,6 +1,6 @@
 find_package(Dotnet REQUIRED)
 
-if("${TARGET_ARCHITECTURE}" STREQUAL "i686")
+if(TARGET_ARCHITECTURE STREQUAL "i686")
     set(Z3_DOTNET_PLATFORM "x86")
 else()
     set(Z3_DOTNET_PLATFORM "AnyCPU")
diff --git a/examples/maxsat/CMakeLists.txt b/examples/maxsat/CMakeLists.txt
index 1e184e535..6e9e333c1 100644
--- a/examples/maxsat/CMakeLists.txt
+++ b/examples/maxsat/CMakeLists.txt
@@ -35,7 +35,7 @@ if (FORCE_CXX_LINKER)
   )
 endif()
 
-if ("${CMAKE_SYSTEM_NAME}" MATCHES "[Ww]indows")
+if (CMAKE_SYSTEM_NAME MATCHES "[Ww]indows")
   # On Windows we need to copy the Z3 libraries
   # into the same directory as the executable
   # so that they can be found.
diff --git a/examples/tptp/CMakeLists.txt b/examples/tptp/CMakeLists.txt
index d513b0205..9d4caa190 100644
--- a/examples/tptp/CMakeLists.txt
+++ b/examples/tptp/CMakeLists.txt
@@ -28,7 +28,7 @@ add_executable(z3_tptp5 tptp5.cpp tptp5.lex.cpp)
 target_include_directories(z3_tptp5 PRIVATE ${Z3_CXX_INCLUDE_DIRS})
 target_link_libraries(z3_tptp5 PRIVATE ${Z3_LIBRARIES})
 
-if ("${CMAKE_SYSTEM_NAME}" MATCHES "[Ww]indows")
+if (CMAKE_SYSTEM_NAME MATCHES "[Ww]indows")
   # On Windows we need to copy the Z3 libraries
   # into the same directory as the executable
   # so that they can be found.
diff --git a/src/api/dotnet/CMakeLists.txt b/src/api/dotnet/CMakeLists.txt
index ac13b0724..c7ae98762 100644
--- a/src/api/dotnet/CMakeLists.txt
+++ b/src/api/dotnet/CMakeLists.txt
@@ -140,7 +140,7 @@ endforeach()
 # Note, nuget package file names do not have the ${VER_REV} part.
 
 set(Z3_DOTNET_NUPKG_VERSION "${VER_MAJOR}.${VER_MINOR}.${VER_BUILD}")
-if("${TARGET_ARCHITECTURE}" STREQUAL "i686")
+if(TARGET_ARCHITECTURE STREQUAL "i686")
     set(Z3_DOTNET_PLATFORM "x86")
 else()
     set(Z3_DOTNET_PLATFORM "AnyCPU")
diff --git a/src/util/mpz.cpp b/src/util/mpz.cpp
index 5e426eb18..a7c745947 100644
--- a/src/util/mpz.cpp
+++ b/src/util/mpz.cpp
@@ -1716,8 +1716,8 @@ void mpz_manager<SYNCH>::display(std::ostream & out, mpz const & a) const {
         // GMP version
         size_t sz = mpz_sizeinbase(*a.m_ptr, 10) + 2;
         sbuffer<char, 1024> buffer(sz, 0);
-        mpz_get_str(buffer.c_ptr(), 10, *a.m_ptr);
-        out << buffer.c_ptr();
+        mpz_get_str(buffer.data(), 10, *a.m_ptr);
+        out << buffer.data();
 #endif
     } 
 }
@@ -1776,11 +1776,11 @@ void mpz_manager<SYNCH>::display_hex(std::ostream & out, mpz const & a, unsigned
         unsigned requiredLength = num_bits / 4;
         unsigned padding = requiredLength > sz ? requiredLength - sz : 0;
         sbuffer<char, 1024> buffer(sz, 0);
-        mpz_get_str(buffer.c_ptr(), 16, *(a.m_ptr));
+        mpz_get_str(buffer.data(), 16, *(a.m_ptr));
         for (unsigned i = 0; i < padding; ++i) {
             out << "0";
         }
-        out << buffer.c_ptr() + (sz > requiredLength ? sz - requiredLength : 0);
+        out << buffer.data() + (sz > requiredLength ? sz - requiredLength : 0);
 #endif
     }
     out.copyfmt(fmt);
@@ -1830,11 +1830,11 @@ void mpz_manager<SYNCH>::display_bin(std::ostream & out, mpz const & a, unsigned
         size_t sz = mpz_sizeinbase(*(a.m_ptr), 2);
         unsigned padding = num_bits > sz ? num_bits - sz : 0;
         sbuffer<char, 1024> buffer(sz, 0);
-        mpz_get_str(buffer.c_ptr(), 2, *(a.m_ptr));
+        mpz_get_str(buffer.data(), 2, *(a.m_ptr));
         for (unsigned i = 0; i < padding; ++i) {
             out << "0";
         }
-        out << buffer.c_ptr() + (sz > num_bits ? sz - num_bits : 0);
+        out << buffer.data() + (sz > num_bits ? sz - num_bits : 0);
 #endif
     }
 }