diff options
| -rw-r--r-- | INSTALL | 2 | ||||
| -rw-r--r-- | NEWS | 1 | ||||
| -rw-r--r-- | src/printer/smt2/smt2_printer.cpp | 2 | ||||
| -rw-r--r-- | test/unit/Makefile.am | 4 |
4 files changed, 3 insertions, 6 deletions
@@ -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 @@ -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 |