diff -Naur z3-z3-4.8.3.orig/examples/tptp/tptp5.cpp z3-z3-4.8.3/examples/tptp/tptp5.cpp
--- z3-z3-4.8.3.orig/examples/tptp/tptp5.cpp	2018-11-22 17:05:10.861686100 -0500
+++ z3-z3-4.8.3/examples/tptp/tptp5.cpp	2018-11-22 17:05:14.862721000 -0500
@@ -1057,7 +1057,7 @@
     }
 
     bool mk_env_filename(const char* rel_name, std::string& inc_name) {
-#ifdef _WINDOWS
+#if defined(_MSC_VER)
         char buffer[1024];
         size_t sz;
         errno_t err = getenv_s( 
diff -Naur z3-z3-4.8.3.orig/scripts/mk_util.py z3-z3-4.8.3/scripts/mk_util.py
--- z3-z3-4.8.3.orig/scripts/mk_util.py	2018-11-22 17:05:10.903686600 -0500
+++ z3-z3-4.8.3/scripts/mk_util.py	2018-11-22 17:46:04.413565100 -0500
@@ -76,6 +76,7 @@
 IS_CYGWIN=False
 IS_CYGWIN_MINGW=False
 IS_MSYS2=False
+IS_MSYS2_MINGW=False
 VERBOSE=True
 DEBUG_MODE=False
 SHOW_CPPS = True
@@ -165,6 +166,9 @@
 def is_msys2():
     return IS_MSYS2
 
+def is_msys2_mingw():
+    return IS_MSYS2_MINGW
+
 def norm_path(p):
     return os.path.expanduser(os.path.normpath(p))
 
@@ -240,7 +244,7 @@
 
 def exec_compiler_cmd(cmd):
     r = exec_cmd(cmd)
-    if is_windows() or is_cygwin_mingw() or is_cygwin() or is_msys2():
+    if is_windows() or is_cygwin_mingw() or is_cygwin() or is_msys2_mingw() or is_msys2():
         rmf('a.exe')
     else:
         rmf('a.out')
@@ -635,10 +639,13 @@
             IS_CYGWIN_MINGW=True
     elif os.uname()[0].startswith('MSYS_NT') or os.uname()[0].startswith('MINGW'):
         IS_MSYS2=True
-        if os.uname()[4] == 'x86_64':
-            LINUX_X64=True
+        if (CC != None and "mingw" in CC):
+            IS_MSYS2_MINGW=True
         else:
-            LINUX_X64=False
+            if os.uname()[4] == 'x86_64':
+                LINUX_X64=True
+            else:
+                LINUX_X64=False
             
 
 def display_help(exit_code):
@@ -2188,6 +2195,9 @@
                 # Some ocamlmklib's don't like -g; observed on cygwin, but may be others as well.
                 OCAMLMKLIB += ' -g'
 
+            if is_msys2() and not(is_msys2_mingw()):
+                LIBZ3 = 'libz3.dll'
+
             z3mls = os.path.join(self.sub_dir, 'z3ml')
             out.write('%s.cma: %s %s %s\n' % (z3mls, cmos, stubso, z3dllso))
             out.write('\t%s -o %s -I %s %s %s %s\n' % (OCAMLMKLIB, z3mls, self.sub_dir, stubso, cmos, LIBZ3))
@@ -2250,7 +2260,7 @@
             out.write(' %s' % ((os.path.join(self.sub_dir, 'z3ml.cmxa'))))
             out.write(' %s' % ((os.path.join(self.sub_dir, 'z3ml.cmxs'))))
             out.write(' %s' % ((os.path.join(self.sub_dir, 'dllz3ml'))))
-            if is_windows() or is_cygwin_mingw():
+            if is_windows() or is_cygwin_mingw() or is_msys2_mingw():
                 out.write('.dll')
             else:
                 out.write('.so') # .so also on OSX!
@@ -2776,7 +2786,7 @@
             SO_EXT         = '.dll'
             SLIBFLAGS      = '-shared'
             EXE_EXT        = '.exe'
-            LIB_EXT        = '.lib'
+            LIB_EXT        = '.a'
         else:
             raise MKException('Unsupported platform: %s' % sysname)
         if is64():
@@ -2791,7 +2801,7 @@
             SLIBFLAGS    = '%s -m32' % SLIBFLAGS
         if TRACE or DEBUG_MODE:
             CPPFLAGS     = '%s -D_TRACE' % CPPFLAGS
-        if is_cygwin_mingw():
+        if is_cygwin_mingw() or is_msys2_mingw():
             # when cross-compiling with MinGW, we need to statically link its standard libraries
             # and to make it create an import library.
             SLIBEXTRAFLAGS = '%s -static-libgcc -static-libstdc++ -Wl,--out-implib,libz3.dll.a' % SLIBEXTRAFLAGS
@@ -2829,6 +2839,8 @@
             print('C Compiler  :   %s' % CC)
             if is_cygwin_mingw():
                 print('MinGW32 cross:  %s' % (is_cygwin_mingw()))
+            if is_msys2_mingw():
+                print('MinGW32 cross:  %s' % (is_msys2_mingw()))
             print('Archive Tool:   %s' % AR)
             print('Arithmetic:     %s' % ARITH)
             print('OpenMP:         %s' % HAS_OMP)
diff -Naur z3-z3-4.8.3.orig/scripts/update_api.py z3-z3-4.8.3/scripts/update_api.py
--- z3-z3-4.8.3.orig/scripts/update_api.py	2018-11-22 17:05:10.905743500 -0500
+++ z3-z3-4.8.3/scripts/update_api.py	2018-11-22 17:18:23.986311000 -0500
@@ -1707,7 +1707,7 @@
 from .z3types import *
 from .z3consts import *
 
-_ext = 'dll' if sys.platform in ('win32', 'cygwin') else 'dylib' if sys.platform == 'darwin' else 'so'
+_ext = 'dll' if sys.platform in ('win32', 'cygwin', 'msys') else 'dylib' if sys.platform == 'darwin' else 'so'
 _lib = None
 _default_dirs = ['.',
                  os.path.dirname(os.path.abspath(__file__)),
diff -Naur z3-z3-4.8.3.orig/src/api/python/setup.py z3-z3-4.8.3/src/api/python/setup.py
--- z3-z3-4.8.3.orig/src/api/python/setup.py	2018-11-22 17:05:11.014741900 -0500
+++ z3-z3-4.8.3/src/api/python/setup.py	2018-11-22 17:17:38.124501500 -0500
@@ -30,7 +30,7 @@
 if BUILD_PLATFORM in ('darwin', 'osx'):
     LIBRARY_FILE = "libz3.dylib"
     EXECUTABLE_FILE = "z3"
-elif BUILD_PLATFORM in ('win32', 'cygwin', 'win'):
+elif BUILD_PLATFORM in ('win32', 'cygwin', 'win', 'msys'):
     LIBRARY_FILE = "libz3.dll"
     EXECUTABLE_FILE = "z3.exe"
 else:
diff -Naur z3-z3-4.8.3.orig/src/muz/fp/datalog_parser.cpp z3-z3-4.8.3/src/muz/fp/datalog_parser.cpp
--- z3-z3-4.8.3.orig/src/muz/fp/datalog_parser.cpp	2018-11-22 17:05:11.517735700 -0500
+++ z3-z3-4.8.3/src/muz/fp/datalog_parser.cpp	2018-11-22 17:19:17.336361600 -0500
@@ -99,7 +99,7 @@
          m_data_size(0) {
         m_data.resize(2*s_expansion_step);
         resize_data(0);
-#if _WINDOWS
+#if defined(_MSC_VER)
         errno_t err = fopen_s(&m_file, fname, "rb");
         m_ok = (m_file != NULL) && (err == 0);
 #else
diff -Naur z3-z3-4.8.3.orig/src/shell/main.cpp z3-z3-4.8.3/src/shell/main.cpp
--- z3-z3-4.8.3.orig/src/shell/main.cpp	2018-11-22 17:05:12.074728100 -0500
+++ z3-z3-4.8.3/src/shell/main.cpp	2018-11-22 17:19:59.215640700 -0500
@@ -377,7 +377,7 @@
             UNREACHABLE();
         }
         memory::finalize();
-#ifdef _WINDOWS
+#if defined(_MSC_VER)
         _CrtDumpMemoryLeaks();
 #endif
         return return_value;
diff -Naur z3-z3-4.8.3.orig/src/test/for_each_file.cpp z3-z3-4.8.3/src/test/for_each_file.cpp
--- z3-z3-4.8.3.orig/src/test/for_each_file.cpp	2018-11-22 17:05:11.894729800 -0500
+++ z3-z3-4.8.3/src/test/for_each_file.cpp	2018-11-22 17:20:22.507283000 -0500
@@ -17,7 +17,7 @@
 Revision History:
 
 --*/
-#ifdef _WINDOWS
+#if defined(_MSC_VER)
 #include <string>
 #include <windows.h>
 #include <strsafe.h>
diff -Naur z3-z3-4.8.3.orig/src/test/interval.cpp z3-z3-4.8.3/src/test/interval.cpp
--- z3-z3-4.8.3.orig/src/test/interval.cpp	2018-11-22 17:05:11.931673600 -0500
+++ z3-z3-4.8.3/src/test/interval.cpp	2018-11-22 17:20:51.434085200 -0500
@@ -201,7 +201,7 @@
 static char g_buffer[BUFFER_SZ];
 
 char const * get_next_file_name() {
-#ifdef _WINDOWS
+#if defined(_MSC_VER)
     sprintf_s(g_buffer, BUFFER_SZ, "interval_lemma_%d.smt2", g_problem_id);
 #else
     sprintf(g_buffer, "interval_lemma_%d.smt2", g_problem_id);
diff -Naur z3-z3-4.8.3.orig/src/test/quant_elim.cpp z3-z3-4.8.3/src/test/quant_elim.cpp
--- z3-z3-4.8.3.orig/src/test/quant_elim.cpp	2018-11-22 17:05:11.951729800 -0500
+++ z3-z3-4.8.3/src/test/quant_elim.cpp	2018-11-22 17:21:39.008092300 -0500
@@ -497,7 +497,7 @@
    
 
     memory::finalize();
-#ifdef _WINDOWS
+#if defined(_MSC_VER)
     _CrtDumpMemoryLeaks();
 #endif
     exit(0);
diff -Naur z3-z3-4.8.3.orig/src/test/quant_solve.cpp z3-z3-4.8.3/src/test/quant_solve.cpp
--- z3-z3-4.8.3.orig/src/test/quant_solve.cpp	2018-11-22 17:05:11.952729000 -0500
+++ z3-z3-4.8.3/src/test/quant_solve.cpp	2018-11-22 17:21:59.902171600 -0500
@@ -255,7 +255,7 @@
 
 #if 0
     memory::finalize();
-#ifdef _WINDOWS
+#if defined(_MSC_VER)
     _CrtDumpMemoryLeaks();
 #endif
     exit(0);
diff -Naur z3-z3-4.8.3.orig/src/util/mpn.cpp z3-z3-4.8.3/src/util/mpn.cpp
--- z3-z3-4.8.3.orig/src/util/mpn.cpp	2018-11-22 17:05:12.105738700 -0500
+++ z3-z3-4.8.3/src/util/mpn.cpp	2018-11-22 17:25:40.058461900 -0500
@@ -362,7 +362,7 @@
     TRACE("mpn_to_string", tout << "[mpn] to_string "; display_raw(tout, a, lng); tout << " == "; );
 
     if (lng == 1) {
-#ifdef _WINDOWS
+#if defined(_MSC_VER)
         sprintf_s(buf, lbuf, "%u", *a);
 #else
         snprintf(buf, lbuf, "%u", *a);
diff -Naur z3-z3-4.8.3.orig/src/util/util.h z3-z3-4.8.3/src/util/util.h
--- z3-z3-4.8.3.orig/src/util/util.h	2018-11-22 17:05:12.260727400 -0500
+++ z3-z3-4.8.3/src/util/util.h	2018-11-22 17:28:24.553951500 -0500
@@ -46,7 +46,7 @@
 #define UINT64_MAX 0xffffffffffffffffull
 #endif
 
-#ifdef _WINDOWS
+#if defined(_MSC_VER)
 #define SPRINTF_D(_buffer_, _i_) sprintf_s(_buffer_, Z3_ARRAYSIZE(_buffer_), "%d", _i_)
 #define SPRINTF_U(_buffer_, _u_) sprintf_s(_buffer_, Z3_ARRAYSIZE(_buffer_), "%u", _u_)
 #define _Exit exit