From 42572ec93a8fb6798367da035c61100339aab601 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 13 Oct 2012 14:03:03 -0700
Subject: [PATCH 1/2] added missing script

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 c++/build.sh | 9 +++++++++
 1 file changed, 9 insertions(+)
 create mode 100755 c++/build.sh

diff --git a/c++/build.sh b/c++/build.sh
new file mode 100755
index 000000000..e829332f0
--- /dev/null
+++ b/c++/build.sh
@@ -0,0 +1,9 @@
+if g++ -fopenmp -o example example.cpp -lz3; then
+    echo "Example was successfully compiled."
+    echo "To run example, execute:"
+    echo "  ./example"
+else
+    echo "You must install Z3 before compiling this example."
+    echo "To install Z3, execute the following command in the Z3 root directory."
+    echo "   sudo make install"
+fi

From a1599436697a4aa818868f3454515481594df2d6 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 13 Oct 2012 14:07:39 -0700
Subject: [PATCH 2/2] cygwin support

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 RELEASE_NOTES              | 4 ++++
 lib/scoped_timer.cpp       | 5 +++++
 shell/datalog_frontend.cpp | 4 ++++
 3 files changed, 13 insertions(+)

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"