Additions in Release-1.1
========================

  - Command line options to enable the preprocessor of CirCUs
  - Command line options to suppress printing satisfying assignment in CirCUs. 
    By default, CirCUs will print out satisfying assignment. 
  - Recent version of CirCUs
  - Recent version of Sateen
	    

CUSP is a Satisfiability Project that combines CirCUs (SAT solver) 
and Sateen (SMT solver). It has been developed at the University of Colorado
at Boulder. CirCUs is a SAT solver based on the DPLL procedure and 
conflict clause recording.  CirCUs includes most current popular techniques
such as two-watched literals scheme for BCP, activity-based decision 
heuristics, clause deletion strategies, restarting heuristics, and first
UIP-based clause learning.  Current version of CirCUs adopts strong 
conflict analysis, one that often learns better clauses than those of the
first Unique Implication Point (UIP).  Sateen combines CirCUs with 
theory-specific procedures. It uses the lazy approach that relies on
incremental refinements of a propositional abstraction of the given formula 
during the enumeration of its solutions.  Current version of Sateen
deals with Difference Logic (IDL, RDL), in which arithmetic atomic formulae 
constrain the difference between the values of pairs of integer or
real variables.