VCEGAR 1.1 BINARY INSTALLATION for Windows under Cygwin environment
	*******************************************************************

1. You need to have cygwin installed. If you do not already have this
you can get it from http://www.cygwin.com/.

Once cygwin is installed you need to add the "cygwin\bin" directory to
your windows path. If you follow default instructions when installing
cygwin, you will need to add C:\cygwin\bin to the windows path
variable.

2. Download and install the Cadence SMV model checker. The website for
obtaining SMV is: http://www.kenmcmil.com/smv.html. Make sure that
Cadence SMV executable named "smv" is included in your (windows) path
variable and is working as expected.

3. Download and install the zchaff SAT solver and unsat core extractor
(zcore) which comes as part of the zchaff SAT solver. The website is:
http://www.princeton.edu/~chaff/.

Suppose you download zchaff 2004.11.15.  Then the steps you need to
perform (for generating zcore) are as follows:

   a. Uncomment "#define VERIFY_ON" in zchaff_solver.cpp (line 48).
   b. In the main routine of zverify_df.cpp replace "_dump_core =
      false" with "_dump_core = true". You need to do this only at one
      place (line 771).
   c. make all             [inside cygwin environment]
   d. cp zverify_df zcore

Once again make sure that zchaff and zcore are working as expected on
some small examples. Also add zchaff and zcore to your windows path
variable.

If you have trouble with any of the above steps let us know.

4. Include the vcegar binary in your path variable.

5. You are ready to go! You should be able to run vcegar from cygwin
or windows command prompt.

Report problems to {hjain AT cs DOT cmu DOT edu}  or {daniel.kroening AT inf DOT ethz DOT ch}

-----------------------------------------------------------------------