diff --git a/.gitignore b/.gitignore
index 29c49a130..3fe3a3110 100644
--- a/.gitignore
+++ b/.gitignore
@@ -46,6 +46,7 @@ bld_rel/*
 bld_dbg_x64/*
 bld_rel_x64/*
 .vscode
+*build*/**
 # Auto generated files.
 config.log
 config.status
diff --git a/CMakeLists.txt b/CMakeLists.txt
index a3d3bcfa0..cffe1a4d7 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -160,7 +160,7 @@ list(APPEND Z3_COMPONENT_CXX_DEFINES $<$<CONFIG:RelWithDebInfo>:_EXTERNAL_RELEAS
 ################################################################################
 # Find Python
 ################################################################################
-find_package(PythonInterp REQUIRED)
+find_package(PythonInterp 3 REQUIRED)
 message(STATUS "PYTHON_EXECUTABLE: ${PYTHON_EXECUTABLE}")
 
 ################################################################################
@@ -230,7 +230,7 @@ else()
   message(FATAL_ERROR "Platform \"${CMAKE_SYSTEM_NAME}\" not recognised")
 endif()
 
-list(APPEND Z3_COMPONENT_EXTRA_INCLUDE_DIRS 
+list(APPEND Z3_COMPONENT_EXTRA_INCLUDE_DIRS
   "${PROJECT_BINARY_DIR}/src"
   "${PROJECT_SOURCE_DIR}/src"
 )
@@ -293,8 +293,8 @@ if ((TARGET_ARCHITECTURE STREQUAL "x86_64") OR (TARGET_ARCHITECTURE STREQUAL "i6
     set(SSE_FLAGS "-mfpmath=sse" "-msse" "-msse2")
   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") 
+    # Intel's compiler requires linking with libiomp5
+    list(APPEND Z3_DEPENDENT_LIBS "iomp5")
   elseif (CMAKE_CXX_COMPILER_ID STREQUAL "MSVC")
     set(SSE_FLAGS "/arch:SSE2")
   else()
@@ -624,7 +624,7 @@ install(
 ################################################################################
 # Examples
 ################################################################################
-cmake_dependent_option(Z3_ENABLE_EXAMPLE_TARGETS 
+cmake_dependent_option(Z3_ENABLE_EXAMPLE_TARGETS
     "Build Z3 api examples" ON
     "CMAKE_SOURCE_DIR STREQUAL PROJECT_SOURCE_DIR" OFF)
 if (Z3_ENABLE_EXAMPLE_TARGETS)
diff --git a/src/util/parray.h b/src/util/parray.h
index 0c3173f6c..f8f2d7e54 100644
--- a/src/util/parray.h
+++ b/src/util/parray.h
@@ -91,7 +91,7 @@ private:
     }
 
     void dec_ref(unsigned sz, value * vs) {
-        if (C::ref_count) 
+        if (C::ref_count)
             for (unsigned i = 0; i < sz; i++)
                 m_vmanager.dec_ref(vs[i]);
     }
@@ -151,7 +151,7 @@ private:
         size_t new_capacity  = curr_capacity == 0 ? 2 : (3 * curr_capacity + 1) >> 1;
         value * new_vs       = allocate_values(new_capacity);
         if (curr_capacity > 0) {
-            for (size_t i = 0; i < curr_capacity; i++) 
+            for (size_t i = 0; i < curr_capacity; i++)
                 new_vs[i] = vs[i];
             deallocate_values(vs);
         }
@@ -177,7 +177,7 @@ private:
         inc_ref(v);
         vs[sz] = v;
         sz++;
-    }     
+    }
 
     void rpush_back(cell * c, value const & v) {
         SASSERT(c->kind() == ROOT);
@@ -269,7 +269,7 @@ public:
     }
 
     value_manager & manager() { return m_vmanager; }
-    
+
     void mk(ref & r) {
         dec_ref(r.m_ref);
         cell * new_c = mk(ROOT);
@@ -283,12 +283,12 @@ public:
         r.m_ref          = nullptr;
         r.m_updt_counter = 0;
     }
-    
+
     void copy(ref const & s, ref & t) {
         inc_ref(s.m_ref);
         dec_ref(t.m_ref);
         t.m_ref = s.m_ref;
-        t.m_updt_counter = 0; 
+        t.m_updt_counter = 0;
     }
 
     unsigned size(ref const & r) const {
@@ -310,7 +310,7 @@ public:
     }
 
     void check_size(cell* c) const {
-        unsigned r;
+        [[maybe_unused]] unsigned r;
         while (c) {
             switch (c->kind()) {
             case SET:
@@ -333,7 +333,7 @@ public:
 
     value const & get(ref const & r, unsigned i) const {
         SASSERT(i < size(r));
-        
+
         unsigned trail_sz = 0;
         cell * c = r.m_ref;
 
@@ -451,7 +451,7 @@ public:
         inc_ref(v);
         new_c->m_elem      = v;
         new_c->m_next      = r.m_ref;
-        r.m_ref            = new_c; 
+        r.m_ref            = new_c;
         SASSERT(new_c->m_ref_count == 1);
     }
 
@@ -536,7 +536,7 @@ public:
         r.m_updt_counter = 0;
         SASSERT(r.root());
     }
-    
+
     void reroot(ref & r) {
         if (r.root())
             return;
@@ -545,7 +545,7 @@ public:
         unsigned r_sz = size(r);
         unsigned trail_split_idx = r_sz / C::factor;
         unsigned i = 0;
-        cell * c   = r.m_ref;        
+        cell * c   = r.m_ref;
         while (c->kind() != ROOT && i < trail_split_idx) {
             cs.push_back(c);
             c = c->next();
@@ -556,7 +556,7 @@ public:
             unfold(c);
         }
         DEBUG_CODE(check_size(c););
-        SASSERT(c->kind() == ROOT);      
+        SASSERT(c->kind() == ROOT);
         for (i = cs.size(); i-- > 0; ) {
             cell * p = cs[i];
             SASSERT(c->m_kind == ROOT);
@@ -574,7 +574,7 @@ public:
             case PUSH_BACK:
                 c->m_kind = POP_BACK;
                 if (sz == capacity(vs))
-                    expand(vs);                
+                    expand(vs);
                 vs[sz] = p->m_elem;
                 ++sz;
                 c->m_idx = sz;