Some minor cleanup and documentation.

Author: mdeters

INSTALL

@@ -139,7 +139,7 @@ CVC4 to use abc configure with --with-abc and --with-abc-dir=PATH, where
 PATH corresponds to the install path of ABC. To run CVC4 using ABC use
 the --bitblast-aig command line argument.
 Please visit http://www.eecs.berkeley.edu/~alanmi/abc/ for more details
-on ABC. 
+on ABC.
 
 The GNU Readline library is optionally used to provide command
 editing, tab completion, and history functionality at the CVC prompt

NEWS

@@ -3,6 +3,7 @@ This file contains a summary of important user-visible changes.
 Changes since 1.3
 =================
 
+* Building with libc++ instead of libstdc++ (on Mac especially).
 * The LFSC proof checker has been incorporated into CVC4 sources.
 * By default, CVC4 builds in "production" mode (optimized, with fewer
   internal checks on).  The common alternative is a "debug" build, which

src/printer/smt2/smt2_printer.cpp

@@ -1049,7 +1049,7 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) thr
 
     const Datatype & d = i->getDatatype();
 
-    out << "(" << maybeQuoteSymbol(d.getName()) << "  ";
+    out << "(" << maybeQuoteSymbol(d.getName()) << " ";
     for(Datatype::const_iterator ctor = d.begin(), ctor_end = d.end();
         ctor != ctor_end; ++ctor){
       if( ctor!=d.begin() ) out << " ";

test/unit/Makefile.am

@@ -58,10 +58,6 @@ UNIT_TESTS += \
 	main/interactive_shell_black
 endif
 
-# disabled/failing:
-#	theory/theory_bv_white \
-#
-
 export VERBOSE = 1
 
 # Things that aren't tests but that tests rely on and need to