diff --git a/RELEASE_NOTES b/RELEASE_NOTES
index 551bc3f16..6cddb6038 100644
--- a/RELEASE_NOTES
+++ b/RELEASE_NOTES
@@ -30,6 +30,10 @@ Version 4.2
 - Z3 by default switches to an incremental solver when a Solver object is used to solve many queries.
   In the this version, we switch back to the tactic framework if the incremental solver returns "unknown".
 
+- Now, Z3 can be compiled inside cygwin using gcc.
+
+- Fixed bug in the unsat core generation.
+
 First source code release (October 2, 2012)
 ===========================================
 
diff --git a/lib/scoped_timer.cpp b/lib/scoped_timer.cpp
index c2583921d..bde735a69 100644
--- a/lib/scoped_timer.cpp
+++ b/lib/scoped_timer.cpp
@@ -16,6 +16,11 @@ Author:
 Revision History:
 
 --*/
+#ifdef _CYGWIN
+// Hack to make CreateTimerQueueTimer available on cygwin
+#define _WIN32_WINNT 0x0600
+#endif
+
 #include"z3_exception.h"
 #include"z3_omp.h"
 #if defined(_WINDOWS) || defined(_CYGWIN)
diff --git a/shell/datalog_frontend.cpp b/shell/datalog_frontend.cpp
index 216203914..2408f595f 100644
--- a/shell/datalog_frontend.cpp
+++ b/shell/datalog_frontend.cpp
@@ -22,6 +22,10 @@ Revision History:
 #include<time.h>
 #include<signal.h>
 #include"stopwatch.h"
+#ifdef _CYGWIN
+#undef min
+#undef max
+#endif
 #include"front_end_params.h"
 #include"datalog_parser.h"
 #include"arith_decl_plugin.h"