mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 04:03:39 +00:00
Code Activity

cygwin support

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-10-13 14:07:39 -07:00
parent 3cf96f7475
commit a159943669
3 changed files with 13 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
RELEASE_NOTES
View file

@ -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. - 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". 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) First source code release (October 2, 2012)
=========================================== ===========================================

5
lib/scoped_timer.cpp
View file

@ -16,6 +16,11 @@ Author:
Revision History: Revision History:
--*/ --*/
#ifdef _CYGWIN
// Hack to make CreateTimerQueueTimer available on cygwin
#define _WIN32_WINNT 0x0600
#endif
#include"z3_exception.h" #include"z3_exception.h"
#include"z3_omp.h" #include"z3_omp.h"
#if defined(_WINDOWS) || defined(_CYGWIN) #if defined(_WINDOWS) || defined(_CYGWIN)

4
shell/datalog_frontend.cpp
View file

@ -22,6 +22,10 @@ Revision History:
#include<time.h> #include<time.h>
#include<signal.h> #include<signal.h>
#include"stopwatch.h" #include"stopwatch.h"
#ifdef _CYGWIN
#undef min
#undef max
#endif
#include"front_end_params.h" #include"front_end_params.h"
#include"datalog_parser.h" #include"datalog_parser.h"
#include"arith_decl_plugin.h" #include"arith_decl_plugin.h"