From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 20 Jun 2014 18:17:01 +0000 (-0400)
Subject: Some minor cleanup and documentation.
X-Git-Tag: cvc5-1.0.0~6755
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f99a56440cb20d5771162e7382e238f0705182fe;p=cvc5.git

Some minor cleanup and documentation.
---

diff --git a/INSTALL b/INSTALL
index c1258e3ed..bec3936c3 100644
--- 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 f75febe02..f227952fe 100644
--- 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 95f35a5a6..36494e1de 100644
--- 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 be64e3ea1..937a4e8c8 100644
--- 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