Some minor cleanup and documentation.

diff --git a/INSTALL b/INSTALL
index c1258e3edb8082b0f259177e2f1d8d769a711652..bec3936c3e864ee4cfb65bec8bf8d32a51497bab 100644 (file)
--- a/INSTALL
+++ b/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

diff --git a/NEWS b/NEWS
index f75febe02e418ddc46378fe3a5330558aa01fb30..f227952fe32c02d25b988b561646bf6e9e19f4d6 100644 (file)
--- a/NEWS
+++ b/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

diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 95f35a5a6838eff832fe438f0a56cfeeccaff36b..36494e1dee2ac77c226f7f35977d7d4c70ac9b53 100644 (file)
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/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 << " ";

diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am
index be64e3ea120b7bcfdfde42428c4b3fcf4fd7d9fc..937a4e8c83108e93eb2aa8b9cb77655ad436cb2a 100644 (file)
--- a/test/unit/Makefile.am
+++ b/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