Update README for 1.5 release (#182)

diff --git a/README b/README
index ac30685366a9db202746cb73fa7c66f76e073246..da2457fed70f9e92ba9028aee7cf3c012b5e5219 100644 (file)
--- a/README
+++ b/README
@@ -1,15 +1,15 @@
 This is CVC4 release version 1.5.  For build and installation notes,
 please see the INSTALL file included with this distribution.
 
-The project leaders are Clark Barrett (Stanford University) and Cesare Tinelli
-(The University of Iowa).  For a full list of authors, please refer to the
-AUTHORS file in the source distribution.
+The project leaders are Clark Barrett (Stanford University) and Cesare
+Tinelli (The University of Iowa).  For a full list of authors, please
+refer to the AUTHORS file in the source distribution.
 
 CVC4 is a tool for determining the satisfiability of a first order
 formula modulo a first order theory (or a combination of such
-theories). It is the fourth in the Cooperating Validity Checker family
-of tools (CVC, CVC Lite, CVC3) but does not directly incorporate code
-from any previous version.
+theories).  It is the fourth in the Cooperating Validity Checker
+family of tools (CVC, CVC Lite, CVC3) but does not directly
+incorporate code from any previous version.
 
 CVC4 is intended to be an open and extensible SMT engine.  It can be
 used as a stand-alone tool or as a library.  It has been designed to
@@ -37,20 +37,21 @@ We are always happy to hear feedback from our users:
   http://cvc4.stanford.edu/#Technical_Support.
 
 * if you need to report a bug with CVC4, or make a feature request,
-  please visit our bugtracker at http://cvc4.cs.stanford.edu/bugs/ or write
-  to the cvc-bugs@cs.stanford.edu mailing list.  We are very grateful for
-  bug reports, as they help us improve CVC4, and patches are generally
-  reviewed and accepted quickly.
+  please visit our bugtracker at http://cvc4.cs.stanford.edu/bugs/ or
+  write to the cvc-bugs@cs.stanford.edu mailing list.  We are very
+  grateful for bug reports, as they help us improve CVC4, and patches
+  are generally reviewed and accepted quickly.
 
 * if you are using CVC4 in your work, or incorporating it into
   software of your own, we'd like to invite you to leave a description
   and link to your project/software on our "Third Party Applications"
-  page at http://cvc4.cs.stanford.edu/wiki/Public:Third_Party_Applications
+  page at
+  http://cvc4.cs.stanford.edu/wiki/Public:Third_Party_Applications
 
-* if you are interested in contributing code (for example, a new decision
-  procedure implementation) to the CVC4 project, please contact one of the
-  project leaders.  We'd be happy to point you to some internals documentation
-  to help you out.
+* if you are interested in contributing code (for example, a new
+  decision procedure implementation) to the CVC4 project, please
+  contact one of the project leaders.  We'd be happy to point you to
+  some internals documentation to help you out.
 
 Thank you for using CVC4!
 
@@ -72,14 +73,14 @@ procedure implementations, added support for using MiniSat in the
 core, and had generally better performance.
 
 CVC4 is the new version, the fifth generation of this validity checker
-line that is now celebrating sixteen years of heritage.  It represents
-a complete re-evaluation of the core architecture to be both
-performant and to serve as a cutting-edge research vehicle for the
-next several years.  Rather than taking CVC3 and redesigning problem
-parts, we've taken a clean-room approach, starting from scratch.
-Before using any designs from CVC3, we have thoroughly scrutinized,
-vetted, and updated them.  Many parts of CVC4 bear only a superficial
-resemblance, if any, to their correspondent in CVC3.
+line that is now celebrating twenty-one years of heritage.  It
+represents a complete re-evaluation of the core architecture to be
+both performant and to serve as a cutting-edge research vehicle for
+the next several years.  Rather than taking CVC3 and redesigning
+problem parts, we've taken a clean-room approach, starting from
+scratch.  Before using any designs from CVC3, we have thoroughly
+scrutinized, vetted, and updated them.  Many parts of CVC4 bear only a
+superficial resemblance, if any, to their correspondent in CVC3.
 
 However, CVC4 is fundamentally similar to CVC3 and many other modern
 SMT solvers: it is a DPLL(T) solver, with a SAT solver at its core and
@@ -97,4 +98,5 @@ in short order.
 
 *** For more information
 
-More information about CVC4 is available at: http://cvc4.cs.stanford.edu/
+More information about CVC4 is available at:
+http://cvc4.cs.stanford.edu/