VCEGAR 1.3 BINARY INSTALLATION
	******************************

1. 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 path variable
and is working as expected.

2. Include the vcegar binary in your path variable.

3. You are ready to go!

Report problems to {hjain, kroening} AT cs DOT cmu DOT edu  

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

        UPGRADING VCEGAR from 1.1 to 1.3
        ********************************

If you already have a previous version of VCEGAR installed, then you
can just replace the old vcegar binary with the new one.

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

        List of changes from VCEGAR 1.1 to VCEGAR 1.3
        **********************************************
 
1. zChaff/zcore is no longer needed. Minisat 1.14 is used as a
decision procedure. It is linked internally, so there is no need to
download MiniSat separately.

2. Improved simulation of abstract transitions using caching.

3. Changes related to discovery of predicates, simplification of
weakest pre-conditions.

4. New options for generating predicate clusters using spurious
transitions.
-----------------------------------------------------------------------