More language bindings work:

* with a patched SWIG, the ocaml bindings build correctly.
** I will provide my patch to the SWIG dev team.
* fixed some class interfaces to play more nicely with SWIG.
* php, perl, tcl now work; examples added.
* improved binding module building and installation.

Also:

Stop #defining NULL ((void*) 0).  This has been in cvc4_public.h for
a long, long time, I forget why I added it in the first place, and
it's a very, very bad idea.  In C++, certain things are permitted
for NULL that aren't permitted for ((void*) 0), like for instance
implicit conversion to any pointer type.  We didn't see an issue
here (until now, when interfacing with SWIG), because GCC is usually
pretty smart at working around such a broken #definition of NULL.
But that's fragile.

New exception-free Command architecture.  Previously, some command
invocations were wrapped in a try {} catch() {} and printed out an
error.  This is much more consistent now.  Each Command invocation
results in a CommandStatus.  The status can be "unsupported",
"error", or "success" (these are each derived classes, though, not
strings, so that they can be easily printed in a language-specific
way... e.g., in SMT-LIBv2, they are printed in a manner consistent
with the spec, and "success" is not printed if the print-success
option is off.)  All Command functionality are now no-throw
functions, which @cconway reports is a Good Thing for Google
(where all C++ exceptions are suspect), and also I think is much
cleaner than the old way in this instance.

Added an --smtlib2 option that enables an "SMT-LIBv2 compliance
mode"---really it just sets a few other options like strictParsing,
inputLanguage, and printSuccess.  In the future we might put other
options into a compliance mode, or we might choose to make it the
default.

38 files changed, 1267 insertions, 634 deletions

diff --git a/examples/Makefile.am b/examples/Makefile.am
index 46de3689b..9f9404ce9 100644
--- a/examples/Makefile.am
+++ b/examples/Makefile.am
@@ -51,9 +51,13 @@ SimpleVCCompat.class: SimpleVCCompat.java
 
 EXTRA_DIST = \
 	SimpleVC.java \
-	SimpleVC.py \
-	SimpleVC.ml \
 	SimpleVCCompat.java \
+	SimpleVC.ml \
+	SimpleVC.php \
+	SimpleVC.pl \
+	SimpleVC.py \
+	SimpleVC.rb \
+	SimpleVC.tcl \
 	README
 
 if STATIC_BINARY
diff --git a/examples/SimpleVC.ml b/examples/SimpleVC.ml
index f7caa9e3d..dc75752db 100644
--- a/examples/SimpleVC.ml
+++ b/examples/SimpleVC.ml
@@ -18,7 +18,7 @@
 ***
 *** To run, use something like:
 ***
-***   LD_LIBRARY_PATH=../builds/src/bindings/.libs \
+***   LD_LIBRARY_PATH=../builds/src/bindings/ocaml/.libs \
 ***     ../builds/src/bindings/cvc4_ocaml_top -I ../builds/src/bindings/ocaml \
 ***     SimpleVC.ml
 ***
diff --git a/examples/SimpleVC.php b/examples/SimpleVC.php
new file mode 100755
index 000000000..eb58860cc
--- /dev/null
+++ b/examples/SimpleVC.php
@@ -0,0 +1,56 @@
+#! /usr/bin/php
+##! \file SimpleVC.php
+### \verbatim
+### Original author: mdeters
+### Major contributors: none
+### Minor contributors (to current version): none
+### This file is part of the CVC4 prototype.
+### Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+### Courant Institute of Mathematical Sciences
+### New York University
+### See the file COPYING in the top-level source directory for licensing
+### information.\endverbatim
+###
+### \brief A simple demonstration of the PHP interface
+###
+### A simple demonstration of the PHP interface.  Compare to the
+### C++ interface in simple_vc_cxx.cpp; they are quite similar.
+###
+### To run, use something like:
+###
+###   ln -s ../builds/src/bindings/php/.libs/CVC4.so CVC4.so
+###   ln -s ../builds/src/bindings/php/CVC4.php CVC4.php
+###   ./SimpleVC.php
+####
+
+use strict;
+use CVC4;
+
+my $em = new CVC4::ExprManager();
+my $smt = new CVC4::SmtEngine($em);
+
+# Prove that for integers x and y:
+#   x > 0 AND y > 0  =>  2x + y >= 3
+
+my $integer = $em->integerType();
+
+my $x = $em->mkVar("x", $integer);
+my $y = $em->mkVar("y", $integer);
+my $zero = $em->mkConst(new CVC4::Integer(0));
+
+my $x_positive = $em->mkExpr($CVC4::GT, $x, $zero);
+my $y_positive = $em->mkExpr($CVC4::GT, $y, $zero);
+
+my $two = $em->mkConst(new CVC4::Integer(2));
+my $twox = $em->mkExpr($CVC4::MULT, $two, $x);
+my $twox_plus_y = $em->mkExpr($CVC4::PLUS, $twox, $y);
+
+my $three = $em->mkConst(new CVC4::Integer(3));
+my $twox_plus_y_geq_3 = $em->mkExpr($CVC4::GEQ, $twox_plus_y, $three);
+
+my $formula = new CVC4::BoolExpr($em->mkExpr($CVC4::AND, $x_positive, $y_positive))->impExpr(new CVC4::BoolExpr($twox_plus_y_geq_3));
+
+print "Checking validity of formula " . $formula->toString() . " with CVC4.\n";
+print "CVC4 should report VALID.\n";
+print "Result from CVC4 is: " . $smt->query($formula)->toString() . "\n";
+
diff --git a/examples/SimpleVC.pl b/examples/SimpleVC.pl
new file mode 100755
index 000000000..6666d49e1
--- /dev/null
+++ b/examples/SimpleVC.pl
@@ -0,0 +1,56 @@
+#! /usr/bin/perl -w
+##! \file SimpleVC.pl
+### \verbatim
+### Original author: mdeters
+### Major contributors: none
+### Minor contributors (to current version): none
+### This file is part of the CVC4 prototype.
+### Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+### Courant Institute of Mathematical Sciences
+### New York University
+### See the file COPYING in the top-level source directory for licensing
+### information.\endverbatim
+###
+### \brief A simple demonstration of the Perl interface
+###
+### A simple demonstration of the Perl interface.  Compare to the
+### C++ interface in simple_vc_cxx.cpp; they are quite similar.
+###
+### To run, use something like:
+###
+###   ln -s ../builds/src/bindings/perl/.libs/CVC4.so CVC4.so
+###   ln -s ../builds/src/bindings/perl/CVC4.pm CVC4.pm
+###   ./SimpleVC.pl
+####
+
+use strict;
+use CVC4;
+
+my $em = new CVC4::ExprManager();
+my $smt = new CVC4::SmtEngine($em);
+
+# Prove that for integers x and y:
+#   x > 0 AND y > 0  =>  2x + y >= 3
+
+my $integer = $em->integerType();
+
+my $x = $em->mkVar("x", $integer);
+my $y = $em->mkVar("y", $integer);
+my $zero = $em->mkConst(new CVC4::Integer(0));
+
+my $x_positive = $em->mkExpr($CVC4::GT, $x, $zero);
+my $y_positive = $em->mkExpr($CVC4::GT, $y, $zero);
+
+my $two = $em->mkConst(new CVC4::Integer(2));
+my $twox = $em->mkExpr($CVC4::MULT, $two, $x);
+my $twox_plus_y = $em->mkExpr($CVC4::PLUS, $twox, $y);
+
+my $three = $em->mkConst(new CVC4::Integer(3));
+my $twox_plus_y_geq_3 = $em->mkExpr($CVC4::GEQ, $twox_plus_y, $three);
+
+my $formula = new CVC4::BoolExpr($em->mkExpr($CVC4::AND, $x_positive, $y_positive))->impExpr(new CVC4::BoolExpr($twox_plus_y_geq_3));
+
+print "Checking validity of formula " . $formula->toString() . " with CVC4.\n";
+print "CVC4 should report VALID.\n";
+print "Result from CVC4 is: " . $smt->query($formula)->toString() . "\n";
+
diff --git a/examples/SimpleVC.py b/examples/SimpleVC.py
index 545e095f9..d2bd6d4c3 100644..100755
--- a/examples/SimpleVC.py
+++ b/examples/SimpleVC.py
@@ -1,4 +1,4 @@
-######################                                                        ##
+#! /usr/bin/python
 ##! \file SimpleVC.py
 ### \verbatim
 ### Original author: mdeters
@@ -18,8 +18,9 @@
 ###
 ### To run, use something like:
 ###
-###   ln -s ../builds/src/bindings/.libs/libcvc4bindings_python.so.0.0.0 _CVC4.so
-###   PYTHONPATH=../builds/src/bindings/python python SimpleVC.py
+###   ln -s ../builds/src/bindings/python/CVC4.py CVC4.py
+###   ln -s ../builds/src/bindings/python/.libs/CVC4.so _CVC4.so
+###   ./SimpleVC.py
 ####
 
 import CVC4
diff --git a/examples/SimpleVC.rb b/examples/SimpleVC.rb
index ef4d82983..36af3c215 100644..100755
--- a/examples/SimpleVC.rb
+++ b/examples/SimpleVC.rb
@@ -1,4 +1,4 @@
-######################                                                        ##
+#! /usr/bin/ruby
 ##! \file SimpleVC.rb
 ### \verbatim
 ### Original author: mdeters
@@ -18,8 +18,8 @@
 ###
 ### To run, use something like:
 ###
-###   ln -s ../builds/src/bindings/.libs/libcvc4bindings_ruby.so.0.0.0 CVC4.so
-###   ruby SimpleVC.rb
+###   ln -s ../builds/src/bindings/ruby/.libs/CVC4.so CVC4.so
+###   ./SimpleVC.rb
 ####
 
 require 'CVC4'
diff --git a/examples/SimpleVC.tcl b/examples/SimpleVC.tcl
new file mode 100755
index 000000000..d2030f044
--- /dev/null
+++ b/examples/SimpleVC.tcl
@@ -0,0 +1,54 @@
+#! /usr/bin/tclsh
+##! \file SimpleVC.tcl
+### \verbatim
+### Original author: mdeters
+### Major contributors: none
+### Minor contributors (to current version): none
+### This file is part of the CVC4 prototype.
+### Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+### Courant Institute of Mathematical Sciences
+### New York University
+### See the file COPYING in the top-level source directory for licensing
+### information.\endverbatim
+###
+### \brief A simple demonstration of the Tcl interface
+###
+### A simple demonstration of the Tcl interface.  Compare to the
+### C++ interface in simple_vc_cxx.cpp; they are quite similar.
+###
+### To run, use something like:
+###
+###   ln -s ../builds/src/bindings/tcl/.libs/CVC4.so CVC4.so
+###   ./SimpleVC.tcl
+####
+
+load CVC4.so CVC4
+
+ExprManager em
+SmtEngine smt em
+
+# Prove that for integers x and y:
+#   x > 0 AND y > 0  =>  2x + y >= 3
+
+set integer [ExprManager_integerType em]
+
+set x [ExprManager_mkVar em "x" $integer]
+set y [ExprManager_mkVar em "y" $integer]
+set zero [ExprManager_mkConst em [Integer _ 0]]
+
+set x_positive [ExprManager_mkExpr em $GT $x $zero]
+set y_positive [ExprManager_mkExpr em $GT $y $zero]
+
+set two [ExprManager_mkConst em [Integer _ 2]]
+set twox [ExprManager_mkExpr em $MULT $two $x]
+set twox_plus_y [ExprManager_mkExpr em $PLUS $twox $y]
+
+set three [ExprManager_mkConst em [Integer _ 3]]
+set twox_plus_y_geq_3 [ExprManager_mkExpr em $GEQ $twox_plus_y $three]
+
+set formula [BoolExpr_impExpr [BoolExpr _1 [ExprManager_mkExpr em $AND $x_positive $y_positive]] [BoolExpr _2 $twox_plus_y_geq_3]]
+
+puts "Checking validity of formula [Expr_toString $formula] with CVC4."
+puts "CVC4 should report VALID."
+puts "Result from CVC4 is: [Result_toString [SmtEngine_query smt $formula]]"
+
diff --git a/src/bindings/Makefile.am b/src/bindings/Makefile.am
index ca09fc3d5..bfc116fd6 100644
--- a/src/bindings/Makefile.am
+++ b/src/bindings/Makefile.am
@@ -12,99 +12,139 @@
 #
 LIBCVC4BINDINGS_VERSION = @CVC4_BINDINGS_LIBRARY_VERSION@
 
+AUTOMAKE_OPTIONS = subdir-objects
+
 AM_CPPFLAGS = \
 	-D__BUILDING_CVC4BINDINGSLIB \
 	-I@srcdir@/../include -I@srcdir@/.. -I@builddir@/..
 AM_CXXFLAGS = -Wall
 
-SUBDIRS = . compat
+SUBDIRS = compat
+
+# any binding-specific flags to pass to swig
+java_cpp_SWIGFLAGS = -package edu.nyu.acsys.CVC4
 
 lib_LTLIBRARIES =
 bin_PROGRAMS =
 javadatadir = $(datadir)/java
+javalibdir = $(datadir)/java
 ocamldatadir = $(libdir)/ocaml/cvc4
+ocamllibdir = $(libdir)/ocaml/cvc4
+perldatadir = $(datadir)/perl5
+perllibdir = $(libdir)/perl5
+phpdatadir = $(datadir)/php
+phplibdir = $(libdir)/php
+pythondatadir = $(datadir)/pyshared
+pythonlibdir = $(libdir)/pyshared
+csharpdatadir = $(datadir)/csharp
+csharplibdir = $(libdir)/csharp
+rubylibdir = $(libdir)/ruby
+tcllibdir = $(libdir)/tcltk
 javadata_DATA =
+javalib_LTLIBRARIES=
 ocamldata_DATA =
+ocamllib_LTLIBRARIES=
+perldata_DATA =
+perllib_LTLIBRARIES =
+phpdata_DATA =
+phplib_LTLIBRARIES =
+pythondata_DATA =
+pythonlib_LTLIBRARIES =
+csharpdata_DATA =
+csharplib_LTLIBRARIES =
+rubylib_LTLIBRARIES =
+tcllib_LTLIBRARIES =
 if CVC4_LANGUAGE_BINDING_JAVA
-lib_LTLIBRARIES += libcvc4bindings_java.la
+javalib_LTLIBRARIES += java/CVC4.la
 javadata_DATA += cvc4.jar
-libcvc4bindings_java_la_LDFLAGS = \
+java_CVC4_la_LDFLAGS = \
+	-module \
 	-version-info $(LIBCVC4BINDINGS_VERSION)
-libcvc4bindings_java_la_LIBADD = \
+java_CVC4_la_LIBADD = \
 	-L@builddir@/.. -lcvc4 \
 	-L@builddir@/../parser -lcvc4parser
 endif
 if CVC4_LANGUAGE_BINDING_CSHARP
-lib_LTLIBRARIES += libcvc4bindings_csharp.la
-libcvc4bindings_csharp_la_LDFLAGS = \
+csharplib_LTLIBRARIES += csharp/CVC4.la
+csharp_CVC4_la_LDFLAGS = \
+	-module \
 	-version-info $(LIBCVC4BINDINGS_VERSION)
-libcvc4bindings_csharp_la_LIBADD = \
+csharp_CVC4_la_LIBADD = \
 	-L@builddir@/.. -lcvc4 \
 	-L@builddir@/../parser -lcvc4parser
 endif
 if CVC4_LANGUAGE_BINDING_PERL
-lib_LTLIBRARIES += libcvc4bindings_perl.la
-libcvc4bindings_perl_la_LDFLAGS = \
+perllib_LTLIBRARIES += perl/CVC4.la
+perl_CVC4_la_LDFLAGS = \
+	-module \
 	-version-info $(LIBCVC4BINDINGS_VERSION)
-libcvc4bindings_perl_la_LIBADD = \
+perl_CVC4_la_LIBADD = \
 	-L@builddir@/.. -lcvc4 \
 	-L@builddir@/../parser -lcvc4parser
+perldata_DATA += perl/CVC4.pm
 endif
 if CVC4_LANGUAGE_BINDING_PHP
-lib_LTLIBRARIES += libcvc4bindings_php.la
-libcvc4bindings_php_la_LDFLAGS = \
+phplib_LTLIBRARIES += php/CVC4.la
+php_CVC4_la_LDFLAGS = \
+	-module \
 	-version-info $(LIBCVC4BINDINGS_VERSION)
-libcvc4bindings_php_la_LIBADD = \
+php_CVC4_la_LIBADD = \
 	-L@builddir@/.. -lcvc4 \
 	-L@builddir@/../parser -lcvc4parser
+phpdata_DATA += php/CVC4.php
 endif
 if CVC4_LANGUAGE_BINDING_PYTHON
-lib_LTLIBRARIES += libcvc4bindings_python.la
-libcvc4bindings_python_la_LDFLAGS = \
+pythonlib_LTLIBRARIES += python/CVC4.la
+python_CVC4_la_LDFLAGS = \
+	-module \
 	-version-info $(LIBCVC4BINDINGS_VERSION)
-libcvc4bindings_python_la_LIBADD = \
+python_CVC4_la_LIBADD = \
 	-L@builddir@/.. -lcvc4 \
 	-L@builddir@/../parser -lcvc4parser
+pythondata_DATA += python/CVC4.py
 endif
 if CVC4_LANGUAGE_BINDING_OCAML
-lib_LTLIBRARIES += libcvc4bindings_ocaml.la
+ocamllib_LTLIBRARIES += ocaml/CVC4.la
 bin_PROGRAMS += cvc4_ocaml_top
 # We provide a make rule below, but we have to tell automake to lay off, too,
 # otherwise it tries (and fails) to package the nonexistent cvc4_ocaml_top.c!
 cvc4_ocaml_top_SOURCES =
 ocamldata_DATA += ocaml/swig.cmo ocaml/swig.cmi ocaml/swigp4.cmo ocaml/swigp4.cmi ocaml/CVC4.cmo ocaml/CVC4.cmi
-libcvc4bindings_ocaml_la_LDFLAGS = \
+ocaml_CVC4_la_LDFLAGS = \
+	-module \
 	-version-info $(LIBCVC4BINDINGS_VERSION)
-libcvc4bindings_ocaml_la_LIBADD = \
+ocaml_CVC4_la_LIBADD = \
 	-L@builddir@/.. -lcvc4 \
 	-L@builddir@/../parser -lcvc4parser
 endif
 if CVC4_LANGUAGE_BINDING_RUBY
-lib_LTLIBRARIES += libcvc4bindings_ruby.la
-libcvc4bindings_ruby_la_LDFLAGS = \
+rubylib_LTLIBRARIES += ruby/CVC4.la
+ruby_CVC4_la_LDFLAGS = \
+	-module \
 	-version-info $(LIBCVC4BINDINGS_VERSION)
-libcvc4bindings_ruby_la_LIBADD = \
+ruby_CVC4_la_LIBADD = \
 	-L@builddir@/.. -lcvc4 \
 	-L@builddir@/../parser -lcvc4parser
 endif
 if CVC4_LANGUAGE_BINDING_TCL
-lib_LTLIBRARIES += libcvc4bindings_tcl.la
-libcvc4bindings_tcl_la_LDFLAGS = \
+tcllib_LTLIBRARIES += tcl/CVC4.la
+tcl_CVC4_la_LDFLAGS = \
+	-module \
 	-version-info $(LIBCVC4BINDINGS_VERSION)
-libcvc4bindings_tcl_la_LIBADD = \
+tcl_CVC4_la_LIBADD = \
 	-L@builddir@/.. -lcvc4 \
 	-L@builddir@/../parser -lcvc4parser
 endif
 
-nodist_libcvc4bindings_java_la_SOURCES = java.cpp
-libcvc4bindings_java_la_CXXFLAGS = -fno-strict-aliasing
-nodist_libcvc4bindings_csharp_la_SOURCES = csharp.cpp
-nodist_libcvc4bindings_perl_la_SOURCES = perl.cpp
-nodist_libcvc4bindings_php_la_SOURCES = php.cpp
-nodist_libcvc4bindings_python_la_SOURCES = python.cpp
-nodist_libcvc4bindings_ocaml_la_SOURCES = ocaml.cpp
-nodist_libcvc4bindings_ruby_la_SOURCES = ruby.cpp
-nodist_libcvc4bindings_tcl_la_SOURCES = tcl.cpp
+nodist_java_CVC4_la_SOURCES = java.cpp
+java_CVC4_la_CXXFLAGS = -fno-strict-aliasing
+nodist_csharp_CVC4_la_SOURCES = csharp.cpp
+nodist_perl_CVC4_la_SOURCES = perl.cpp
+nodist_php_CVC4_la_SOURCES = php.cpp
+nodist_python_CVC4_la_SOURCES = python.cpp
+nodist_ocaml_CVC4_la_SOURCES = ocaml.cpp
+nodist_ruby_CVC4_la_SOURCES = ruby.cpp
+nodist_tcl_CVC4_la_SOURCES = tcl.cpp
 
 CLEANFILES = \
 	java.cpp \
@@ -123,7 +163,7 @@ MOSTLYCLEANFILES = \
 	$(patsubst %,%.d,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))) \
 	cvc4.jar
 
-libcvc4bindings_java_la-java.lo java.lo: java.cpp
+java_CVC4_la-java.lo java.lo: java.cpp
 	$(AM_V_CXX)$(LTCXXCOMPILE) -c $(JAVA_CPPFLAGS) -o $@ $<
 cvc4.jar: java.cpp
 	$(AM_V_GEN) \
@@ -133,16 +173,17 @@ cvc4.jar: java.cpp
 	$(JAVAC) -classpath . -d classes `find . -name '*.java'`; \
 	cd classes); \
 	$(JAR) cf $@ -C java/classes .
-java.cpp:;
+#java.cpp:;
 csharp.lo: csharp.cpp
 	$(AM_V_CXX)$(LTCXXCOMPILE) -c $(CSHARP_CPPFLAGS) -o $@ $<
-csharp.cpp:;
+#csharp.cpp:;
 perl.lo: perl.cpp
 	$(AM_V_CXX)$(LTCXXCOMPILE) -c $(PERL_CPPFLAGS) -o $@ $<
-perl.cpp:;
+#perl.cpp:;
+perl/CVC4.pm: perl.cpp
 php.lo: php.cpp
 	$(AM_V_CXX)$(LTCXXCOMPILE) -c $(PHP_CPPFLAGS) -Iphp -o $@ $<
-php.cpp:;
+#php.cpp:;
 python.lo: python.cpp
 	$(AM_V_CXX)$(LTCXXCOMPILE) -c $(PYTHON_CPPFLAGS) -o $@ $<
 ocaml.lo: ocaml.cpp
@@ -155,26 +196,18 @@ ocaml/swigp4.cmo: ocaml/swigp4.ml; $(AM_V_GEN)$(OCAMLFIND) ocamlc -package camlp
 ocaml/swig.ml:; $(AM_V_GEN)cd ocaml && $(SWIG) -ocaml -co swig.ml
 ocaml/swig.mli:; $(AM_V_GEN)cd ocaml && $(SWIG) -ocaml -co swig.mli
 ocaml/swigp4.ml:; $(AM_V_GEN)cd ocaml && $(SWIG) -ocaml -co swigp4.ml
-ocaml.cpp:;
-cvc4_ocaml_top: libcvc4bindings_ocaml.la ocaml/swig.cmo ocaml/swig.cmi ocaml/swigp4.cmo ocaml/CVC4.cmo ocaml/CVC4.cmi libcvc4bindings_ocaml.la
+#ocaml.cpp:;
+cvc4_ocaml_top: ocaml/CVC4.la ocaml/swig.cmo ocaml/swig.cmi ocaml/swigp4.cmo ocaml/CVC4.cmo ocaml/CVC4.cmi
 	$(AM_V_GEN)\
-	$(OCAMLFIND) ocamlmktop -I $(ocamldatadir) -custom -o cvc4_ocaml_top -package camlp4 dynlink.cma camlp4o.cma ocaml/swig.cmo ocaml/swigp4.cmo ocaml/CVC4.cmo -cclib -L.libs -cclib -L. -cclib -lcvc4bindings_ocaml -cclib -lstdc++
+	$(OCAMLFIND) ocamlmktop -I $(ocamldatadir) -custom -o cvc4_ocaml_top -package camlp4 dynlink.cma camlp4o.cma ocaml/swig.cmo ocaml/swigp4.cmo ocaml/CVC4.cmo -cclib ocaml/.libs/CVC4.so -cclib -lstdc++
 ruby.lo: ruby.cpp
 	$(AM_V_CXX)$(LTCXXCOMPILE) -c $(RUBY_CPPFLAGS) -o $@ $<
 tcl.lo: tcl.cpp
 	$(AM_V_CXX)$(LTCXXCOMPILE) -c $(TCL_CPPFLAGS) -o $@ $<
-tcl.cpp:;
-java.cpp: @srcdir@/../cvc4.i
-	$(AM_V_at)mkdir -p $(patsubst %.cpp,%,$@)
-	$(AM_V_GEN)$(SWIG) -Wall -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. -c++ -$(patsubst %.cpp,%,$@) -outdir $(patsubst %.cpp,%,$@) -package edu.nyu.acsys.CVC4 -o $@ $<
-# somehow, NULL gets translated to ((void*)0) prematurely, and this causes compiler errors ?!
-ruby.cpp python.cpp: @srcdir@/../cvc4.i
-	$(AM_V_at)mkdir -p $(patsubst %.cpp,%,$@)
-	$(AM_V_GEN)$(SWIG) -Wall -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. -c++ -$(patsubst %.cpp,%,$@) -outdir $(patsubst %.cpp,%,$@) -o $@ $<
-	$(AM_V_at)mv $@ $@.old && sed 's,((void\*) 0),NULL,g' $@.old > $@
-$(patsubst %,%.cpp,$(filter-out c c++ java,$(CVC4_LANGUAGE_BINDINGS))): %.cpp: @srcdir@/../cvc4.i
+#tcl.cpp:;
+$(patsubst %,%.cpp,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))): %.cpp: @srcdir@/../cvc4.i
 	$(AM_V_at)mkdir -p $(patsubst %.cpp,%,$@)
-	$(AM_V_GEN)$(SWIG) -Wall -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. -c++ -$(patsubst %.cpp,%,$@) -outdir $(patsubst %.cpp,%,$@) -o $@ $<
+	$(AM_V_GEN)$(SWIG) -Wall -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. -c++ -$(patsubst %.cpp,%,$@) -outdir $(patsubst %.cpp,%,$@) $($(subst .,_,$@)_SWIGFLAGS) -o $@ $<
 
 $(patsubst %,%.d,$(filter-out c c++,$(CVC4_LANGUAGE_BINDINGS))): %.d: @srcdir@/../cvc4.i
 	$(AM_V_GEN)$(SWIG) -I@srcdir@/../include -I@srcdir@/.. -I@builddir@/.. -c++ -MM -o $(patsubst %.d,%.cpp,$@) $<
diff --git a/src/cvc4.i b/src/cvc4.i
index 7723aee6e..8505d5128 100644
--- a/src/cvc4.i
+++ b/src/cvc4.i
@@ -25,11 +25,14 @@ namespace std {
 // caml_invalid_argument and caml_flush, which breaks C++
 // standard headers; undo this damage
 //
-// Unfortunately, this doesn't happen early enough.  swig puts an
-// include <stdexcept> very early, which breaks linking due to a
+// Unfortunately, this code isn't inserted early enough.  swig puts
+// an include <stdexcept> very early, which breaks linking due to a
 // nonexistent std::caml_invalid_argument symbol.. ridiculous!
 //
 #ifdef SWIGOCAML
+#  if defined(flush) || defined(invalid_argument)
+#    error "flush" or "invalid_argument" (or both) is defined by the ocaml headers.  You must #undef it above before inclusion of <stdexcept>.
+#  endif /* flush */
 #  undef flush
 #  undef invalid_argument
 #endif /* SWIGOCAML */
diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 345d7f956..47c6d1eb5 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -21,6 +21,7 @@
 #include <utility>
 #include <iterator>
 #include <sstream>
+#include <exception>
 
 #include "expr/command.h"
 #include "smt/smt_engine.h"
@@ -34,7 +35,10 @@ using namespace std;
 
 namespace CVC4 {
 
-std::ostream& operator<<(std::ostream& out, const Command& c) {
+const int CommandPrintSuccess::s_iosIndex = std::ios_base::xalloc();
+const CommandSuccess* CommandSuccess::s_instance = new CommandSuccess();
+
+std::ostream& operator<<(std::ostream& out, const Command& c) throw() {
   c.toStream(out,
              Node::setdepth::getDepth(out),
              Node::printtypes::getPrintTypes(out),
@@ -42,7 +46,7 @@ std::ostream& operator<<(std::ostream& out, const Command& c) {
   return out;
 }
 
-ostream& operator<<(ostream& out, const Command* c) {
+ostream& operator<<(ostream& out, const Command* c) throw() {
   if(c == NULL) {
     out << "null";
   } else {
@@ -51,180 +55,259 @@ ostream& operator<<(ostream& out, const Command* c) {
   return out;
 }
 
+std::ostream& operator<<(std::ostream& out, const CommandStatus& s) throw() {
+  s.toStream(out, Node::setlanguage::getLanguage(out));
+  return out;
+}
+
+ostream& operator<<(ostream& out, const CommandStatus* s) throw() {
+  if(s == NULL) {
+    out << "null";
+  } else {
+    out << *s;
+  }
+  return out;
+}
+
 /* class Command */
 
-void Command::invoke(SmtEngine* smtEngine, std::ostream& out) {
+Command::Command() throw() : d_commandStatus(NULL) {
+}
+
+Command::~Command() throw() {
+  if(d_commandStatus != NULL && d_commandStatus != CommandSuccess::instance()) {
+    delete d_commandStatus;
+  }
+}
+
+bool Command::ok() const throw() {
+  // either we haven't run the command yet, or it ran successfully
+  return d_commandStatus == NULL || dynamic_cast<const CommandSuccess*>(d_commandStatus) != NULL;
+}
+
+void Command::invoke(SmtEngine* smtEngine, std::ostream& out) throw() {
   invoke(smtEngine);
   printResult(out);
 }
 
-std::string Command::toString() const {
+std::string Command::toString() const throw() {
   std::stringstream ss;
   toStream(ss);
   return ss.str();
 }
 
 void Command::toStream(std::ostream& out, int toDepth, bool types,
-                       OutputLanguage language) const {
+                       OutputLanguage language) const throw() {
   Printer::getPrinter(language)->toStream(out, this, toDepth, types);
 }
 
-void Command::printResult(std::ostream& out) const {
+void CommandStatus::toStream(std::ostream& out, OutputLanguage language) const throw() {
+  Printer::getPrinter(language)->toStream(out, this);
+}
+
+void Command::printResult(std::ostream& out) const throw() {
+  if(d_commandStatus != NULL) {
+    out << *d_commandStatus;
+  }
 }
 
 /* class EmptyCommand */
 
-EmptyCommand::EmptyCommand(std::string name) :
+EmptyCommand::EmptyCommand(std::string name) throw() :
   d_name(name) {
 }
 
-std::string EmptyCommand::getName() const {
+std::string EmptyCommand::getName() const throw() {
   return d_name;
 }
 
-void EmptyCommand::invoke(SmtEngine* smtEngine) {
+void EmptyCommand::invoke(SmtEngine* smtEngine) throw() {
   /* empty commands have no implementation */
+  d_commandStatus = CommandSuccess::instance();
 }
 
 /* class AssertCommand */
 
-AssertCommand::AssertCommand(const BoolExpr& e) :
+AssertCommand::AssertCommand(const BoolExpr& e) throw() :
   d_expr(e) {
 }
 
-BoolExpr AssertCommand::getExpr() const {
+BoolExpr AssertCommand::getExpr() const throw() {
   return d_expr;
 }
 
-void AssertCommand::invoke(SmtEngine* smtEngine) {
-  smtEngine->assertFormula(d_expr);
+void AssertCommand::invoke(SmtEngine* smtEngine) throw() {
+  try {
+    smtEngine->assertFormula(d_expr);
+    d_commandStatus = CommandSuccess::instance();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
+  }
 }
 
 /* class PushCommand */
 
-void PushCommand::invoke(SmtEngine* smtEngine) {
-  smtEngine->push();
+void PushCommand::invoke(SmtEngine* smtEngine) throw() {
+  try {
+    smtEngine->push();
+    d_commandStatus = CommandSuccess::instance();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
+  }
 }
 
 /* class PopCommand */
 
-void PopCommand::invoke(SmtEngine* smtEngine) {
-  smtEngine->pop();
+void PopCommand::invoke(SmtEngine* smtEngine) throw() {
+  try {
+    smtEngine->pop();
+    d_commandStatus = CommandSuccess::instance();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
+  }
 }
 
 /* class CheckSatCommand */
 
-CheckSatCommand::CheckSatCommand() :
+CheckSatCommand::CheckSatCommand() throw() :
   d_expr() {
 }
 
-CheckSatCommand::CheckSatCommand(const BoolExpr& expr) :
+CheckSatCommand::CheckSatCommand(const BoolExpr& expr) throw() :
   d_expr(expr) {
 }
 
-BoolExpr CheckSatCommand::getExpr() const {
+BoolExpr CheckSatCommand::getExpr() const throw() {
   return d_expr;
 }
 
-void CheckSatCommand::invoke(SmtEngine* smtEngine) {
-  d_result = smtEngine->checkSat(d_expr);
+void CheckSatCommand::invoke(SmtEngine* smtEngine) throw() {
+  try {
+    d_result = smtEngine->checkSat(d_expr);
+    d_commandStatus = CommandSuccess::instance();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
+  }
 }
 
-Result CheckSatCommand::getResult() const {
+Result CheckSatCommand::getResult() const throw() {
   return d_result;
 }
 
-void CheckSatCommand::printResult(std::ostream& out) const {
-  out << d_result << endl;
+void CheckSatCommand::printResult(std::ostream& out) const throw() {
+  if(! ok()) {
+    this->Command::printResult(out);
+  } else {
+    out << d_result << endl;
+  }
 }
 
 /* class QueryCommand */
 
-QueryCommand::QueryCommand(const BoolExpr& e) :
+QueryCommand::QueryCommand(const BoolExpr& e) throw() :
   d_expr(e) {
 }
 
-BoolExpr QueryCommand::getExpr() const {
+BoolExpr QueryCommand::getExpr() const throw() {
   return d_expr;
 }
 
-void QueryCommand::invoke(SmtEngine* smtEngine) {
-  d_result = smtEngine->query(d_expr);
+void QueryCommand::invoke(SmtEngine* smtEngine) throw() {
+  try {
+    d_result = smtEngine->query(d_expr);
+    d_commandStatus = CommandSuccess::instance();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
+  }
 }
 
-Result QueryCommand::getResult() const {
+Result QueryCommand::getResult() const throw() {
   return d_result;
 }
 
-void QueryCommand::printResult(std::ostream& out) const {
-  out << d_result << endl;
+void QueryCommand::printResult(std::ostream& out) const throw() {
+  if(! ok()) {
+    this->Command::printResult(out);
+  } else {
+    out << d_result << endl;
+  }
 }
 
 /* class QuitCommand */
 
-QuitCommand::QuitCommand() {
+QuitCommand::QuitCommand() throw() {
 }
 
-void QuitCommand::invoke(SmtEngine* smtEngine) {
+void QuitCommand::invoke(SmtEngine* smtEngine) throw() {
   Dump("benchmark") << *this;
+  d_commandStatus = CommandSuccess::instance();
 }
 
 /* class CommentCommand */
 
-CommentCommand::CommentCommand(std::string comment) : d_comment(comment) {
+CommentCommand::CommentCommand(std::string comment) throw() : d_comment(comment) {
 }
 
-std::string CommentCommand::getComment() const {
+std::string CommentCommand::getComment() const throw() {
   return d_comment;
 }
 
-void CommentCommand::invoke(SmtEngine* smtEngine) {
+void CommentCommand::invoke(SmtEngine* smtEngine) throw() {
   Dump("benchmark") << *this;
+  d_commandStatus = CommandSuccess::instance();
 }
 
 /* class CommandSequence */
 
-CommandSequence::CommandSequence() :
+CommandSequence::CommandSequence() throw() :
   d_index(0) {
 }
 
-CommandSequence::~CommandSequence() {
+CommandSequence::~CommandSequence() throw() {
   for(unsigned i = d_index; i < d_commandSequence.size(); ++i) {
     delete d_commandSequence[i];
   }
 }
 
-void CommandSequence::addCommand(Command* cmd) {
+void CommandSequence::addCommand(Command* cmd) throw() {
   d_commandSequence.push_back(cmd);
 }
 
-void CommandSequence::invoke(SmtEngine* smtEngine) {
+void CommandSequence::invoke(SmtEngine* smtEngine) throw() {
   for(; d_index < d_commandSequence.size(); ++d_index) {
     d_commandSequence[d_index]->invoke(smtEngine);
+    if(! d_commandSequence[d_index]->ok()) {
+      // abort execution
+      d_commandStatus = d_commandSequence[d_index]->getCommandStatus();
+      return;
+    }
     delete d_commandSequence[d_index];
   }
+
+  AlwaysAssert(d_commandStatus == NULL);
+  d_commandStatus = CommandSuccess::instance();
 }
 
-void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out) {
+void CommandSequence::invoke(SmtEngine* smtEngine, std::ostream& out) throw() {
   for(; d_index < d_commandSequence.size(); ++d_index) {
     d_commandSequence[d_index]->invoke(smtEngine, out);
     delete d_commandSequence[d_index];
   }
 }
 
-CommandSequence::const_iterator CommandSequence::begin() const {
+CommandSequence::const_iterator CommandSequence::begin() const throw() {
   return d_commandSequence.begin();
 }
 
-CommandSequence::const_iterator CommandSequence::end() const {
+CommandSequence::const_iterator CommandSequence::end() const throw() {
   return d_commandSequence.end();
 }
 
-CommandSequence::iterator CommandSequence::begin() {
+CommandSequence::iterator CommandSequence::begin() throw() {
   return d_commandSequence.begin();
 }
 
-CommandSequence::iterator CommandSequence::end() {
+CommandSequence::iterator CommandSequence::end() throw() {
   return d_commandSequence.end();
 }
 
@@ -232,53 +315,53 @@ CommandSequence::iterator CommandSequence::end() {
 
 /* class DeclarationDefinitionCommand */
 
-DeclarationDefinitionCommand::DeclarationDefinitionCommand(const std::string& id) :
+DeclarationDefinitionCommand::DeclarationDefinitionCommand(const std::string& id) throw() :
   d_symbol(id) {
 }
 
-std::string DeclarationDefinitionCommand::getSymbol() const {
+std::string DeclarationDefinitionCommand::getSymbol() const throw() {
   return d_symbol;
 }
 
 /* class DeclareFunctionCommand */
 
-DeclareFunctionCommand::DeclareFunctionCommand(const std::string& id, Type t) :
+DeclareFunctionCommand::DeclareFunctionCommand(const std::string& id, Type t) throw() :
   DeclarationDefinitionCommand(id),
   d_type(t) {
 }
 
-Type DeclareFunctionCommand::getType() const {
+Type DeclareFunctionCommand::getType() const throw() {
   return d_type;
 }
 
-void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) {
+void DeclareFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
   Dump("declarations") << *this << endl;
 }
 
 /* class DeclareTypeCommand */
 
-DeclareTypeCommand::DeclareTypeCommand(const std::string& id, size_t arity, Type t) :
+DeclareTypeCommand::DeclareTypeCommand(const std::string& id, size_t arity, Type t) throw() :
   DeclarationDefinitionCommand(id),
   d_arity(arity),
   d_type(t) {
 }
 
-size_t DeclareTypeCommand::getArity() const {
+size_t DeclareTypeCommand::getArity() const throw() {
   return d_arity;
 }
 
-Type DeclareTypeCommand::getType() const {
+Type DeclareTypeCommand::getType() const throw() {
   return d_type;
 }
 
-void DeclareTypeCommand::invoke(SmtEngine* smtEngine) {
+void DeclareTypeCommand::invoke(SmtEngine* smtEngine) throw() {
   Dump("declarations") << *this << endl;
 }
 
 /* class DefineTypeCommand */
 
 DefineTypeCommand::DefineTypeCommand(const std::string& id,
-                                     Type t) :
+                                     Type t) throw() :
   DeclarationDefinitionCommand(id),
   d_params(),
   d_type(t) {
@@ -286,29 +369,30 @@ DefineTypeCommand::DefineTypeCommand(const std::string& id,
 
 DefineTypeCommand::DefineTypeCommand(const std::string& id,
                                      const std::vector<Type>& params,
-                                     Type t) :
+                                     Type t) throw() :
   DeclarationDefinitionCommand(id),
   d_params(params),
   d_type(t) {
 }
 
-const std::vector<Type>& DefineTypeCommand::getParameters() const {
+const std::vector<Type>& DefineTypeCommand::getParameters() const throw() {
   return d_params;
 }
 
-Type DefineTypeCommand::getType() const {
+Type DefineTypeCommand::getType() const throw() {
   return d_type;
 }
 
-void DefineTypeCommand::invoke(SmtEngine* smtEngine) {
+void DefineTypeCommand::invoke(SmtEngine* smtEngine) throw() {
   Dump("declarations") << *this << endl;
+  d_commandStatus = CommandSuccess::instance();
 }
 
 /* class DefineFunctionCommand */
 
 DefineFunctionCommand::DefineFunctionCommand(const std::string& id,
                                              Expr func,
-                                             Expr formula) :
+                                             Expr formula) throw() :
   DeclarationDefinitionCommand(id),
   d_func(func),
   d_formals(),
@@ -318,30 +402,31 @@ DefineFunctionCommand::DefineFunctionCommand(const std::string& id,
 DefineFunctionCommand::DefineFunctionCommand(const std::string& id,
                                              Expr func,
                                              const std::vector<Expr>& formals,
-                                             Expr formula) :
+                                             Expr formula) throw() :
   DeclarationDefinitionCommand(id),
   d_func(func),
   d_formals(formals),
   d_formula(formula) {
 }
 
-Expr DefineFunctionCommand::getFunction() const {
+Expr DefineFunctionCommand::getFunction() const throw() {
   return d_func;
 }
 
-const std::vector<Expr>& DefineFunctionCommand::getFormals() const {
+const std::vector<Expr>& DefineFunctionCommand::getFormals() const throw() {
   return d_formals;
 }
 
-Expr DefineFunctionCommand::getFormula() const {
+Expr DefineFunctionCommand::getFormula() const throw() {
   return d_formula;
 }
 
-void DefineFunctionCommand::invoke(SmtEngine* smtEngine) {
+void DefineFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
   //Dump("declarations") << *this << endl; -- done by SmtEngine
   if(!d_func.isNull()) {
     smtEngine->defineFunction(d_func, d_formals, d_formula);
   }
+  d_commandStatus = CommandSuccess::instance();
 }
 
 /* class DefineNamedFunctionCommand */
@@ -349,314 +434,339 @@ void DefineFunctionCommand::invoke(SmtEngine* smtEngine) {
 DefineNamedFunctionCommand::DefineNamedFunctionCommand(const std::string& id,
                                                        Expr func,
                                                        const std::vector<Expr>& formals,
-                                                       Expr formula) :
+                                                       Expr formula) throw() :
   DefineFunctionCommand(id, func, formals, formula) {
 }
 
-void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) {
+void DefineNamedFunctionCommand::invoke(SmtEngine* smtEngine) throw() {
   this->DefineFunctionCommand::invoke(smtEngine);
   if(!d_func.isNull() && d_func.getType().isBoolean()) {
-    smtEngine->addToAssignment(d_func.getExprManager()->mkExpr(kind::APPLY,
-                                                               d_func));
+    smtEngine->addToAssignment(d_func.getExprManager()->mkExpr(kind::APPLY, d_func));
   }
+  d_commandStatus = CommandSuccess::instance();
 }
 
 /* class Simplify */
 
-SimplifyCommand::SimplifyCommand(Expr term) :
+SimplifyCommand::SimplifyCommand(Expr term) throw() :
   d_term(term) {
 }
 
-Expr SimplifyCommand::getTerm() const {
+Expr SimplifyCommand::getTerm() const throw() {
   return d_term;
 }
 
-void SimplifyCommand::invoke(SmtEngine* smtEngine) {
+void SimplifyCommand::invoke(SmtEngine* smtEngine) throw() {
   d_result = smtEngine->simplify(d_term);
+  d_commandStatus = CommandSuccess::instance();
 }
 
-Expr SimplifyCommand::getResult() const {
+Expr SimplifyCommand::getResult() const throw() {
   return d_result;
 }
 
-void SimplifyCommand::printResult(std::ostream& out) const {
-  out << d_result << endl;
+void SimplifyCommand::printResult(std::ostream& out) const throw() {
+  if(! ok()) {
+    this->Command::printResult(out);
+  } else {
+    out << d_result << endl;
+  }
 }
 
 /* class GetValueCommand */
 
-GetValueCommand::GetValueCommand(Expr term) :
+GetValueCommand::GetValueCommand(Expr term) throw() :
   d_term(term) {
 }
 
-Expr GetValueCommand::getTerm() const {
+Expr GetValueCommand::getTerm() const throw() {
   return d_term;
 }
 
-void GetValueCommand::invoke(SmtEngine* smtEngine) {
+void GetValueCommand::invoke(SmtEngine* smtEngine) throw() {
   d_result = d_term.getExprManager()->mkExpr(kind::TUPLE, d_term,
                                              smtEngine->getValue(d_term));
+  d_commandStatus = CommandSuccess::instance();
 }
 
-Expr GetValueCommand::getResult() const {
+Expr GetValueCommand::getResult() const throw() {
   return d_result;
 }
 
-void GetValueCommand::printResult(std::ostream& out) const {
-  out << d_result << endl;
+void GetValueCommand::printResult(std::ostream& out) const throw() {
+  if(! ok()) {
+    this->Command::printResult(out);
+  } else {
+    out << d_result << endl;
+  }
 }
 
 /* class GetAssignmentCommand */
 
-GetAssignmentCommand::GetAssignmentCommand() {
+GetAssignmentCommand::GetAssignmentCommand() throw() {
 }
 
-void GetAssignmentCommand::invoke(SmtEngine* smtEngine) {
-  d_result = smtEngine->getAssignment();
+void GetAssignmentCommand::invoke(SmtEngine* smtEngine) throw() {
+  try {
+    d_result = smtEngine->getAssignment();
+    d_commandStatus = CommandSuccess::instance();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
+  }
 }
 
-SExpr GetAssignmentCommand::getResult() const {
+SExpr GetAssignmentCommand::getResult() const throw() {
   return d_result;
 }
 
-void GetAssignmentCommand::printResult(std::ostream& out) const {
-  out << d_result << endl;
+void GetAssignmentCommand::printResult(std::ostream& out) const throw() {
+  if(! ok()) {
+    this->Command::printResult(out);
+  } else {
+    out << d_result << endl;
+  }
 }
 
 /* class GetProofCommand */
 
-GetProofCommand::GetProofCommand() {
+GetProofCommand::GetProofCommand() throw() {
 }
 
-void GetProofCommand::invoke(SmtEngine* smtEngine) {
-  d_result = smtEngine->getProof();
+void GetProofCommand::invoke(SmtEngine* smtEngine) throw() {
+  try {
+    d_result = smtEngine->getProof();
+    d_commandStatus = CommandSuccess::instance();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
+  }
 }
 
-Proof* GetProofCommand::getResult() const {
+Proof* GetProofCommand::getResult() const throw() {
   return d_result;
 }
 
-void GetProofCommand::printResult(std::ostream& out) const {
-  d_result->toStream(out);
+void GetProofCommand::printResult(std::ostream& out) const throw() {
+  if(! ok()) {
+    this->Command::printResult(out);
+  } else {
+    d_result->toStream(out);
+  }
 }
 
 /* class GetAssertionsCommand */
 
-GetAssertionsCommand::GetAssertionsCommand() {
+GetAssertionsCommand::GetAssertionsCommand() throw() {
 }
 
-void GetAssertionsCommand::invoke(SmtEngine* smtEngine) {
-  stringstream ss;
-  const vector<Expr> v = smtEngine->getAssertions();
-  copy( v.begin(), v.end(), ostream_iterator<Expr>(ss, "\n") );
-  d_result = ss.str();
+void GetAssertionsCommand::invoke(SmtEngine* smtEngine) throw() {
+  try {
+    stringstream ss;
+    const vector<Expr> v = smtEngine->getAssertions();
+    copy( v.begin(), v.end(), ostream_iterator<Expr>(ss, "\n") );
+    d_result = ss.str();
+    d_commandStatus = CommandSuccess::instance();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
+  }
 }
 
-std::string GetAssertionsCommand::getResult() const {
+std::string GetAssertionsCommand::getResult() const throw() {
   return d_result;
 }
 
-void GetAssertionsCommand::printResult(std::ostream& out) const {
-  out << d_result;
+void GetAssertionsCommand::printResult(std::ostream& out) const throw() {
+  if(! ok()) {
+    this->Command::printResult(out);
+  } else {
+    out << d_result;
+  }
 }
 
 /* class SetBenchmarkStatusCommand */
 
-SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) :
+SetBenchmarkStatusCommand::SetBenchmarkStatusCommand(BenchmarkStatus status) throw() :
   d_status(status) {
 }
 
-BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const {
+BenchmarkStatus SetBenchmarkStatusCommand::getStatus() const throw() {
   return d_status;
 }
 
-void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) {
-  stringstream ss;
-  ss << d_status;
-  SExpr status = ss.str();
+void SetBenchmarkStatusCommand::invoke(SmtEngine* smtEngine) throw() {
   try {
+    stringstream ss;
+    ss << d_status;
+    SExpr status = ss.str();
     smtEngine->setInfo(":status", status);
-    //d_result = "success";
-  } catch(ModalException&) {
-    d_result = "error";
-  } catch(BadOptionException&) {
-    // should not happen
-    d_result = "error";
+    d_commandStatus = CommandSuccess::instance();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
   }
 }
 
 /* class SetBenchmarkLogicCommand */
 
-SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) :
+SetBenchmarkLogicCommand::SetBenchmarkLogicCommand(std::string logic) throw() :
   d_logic(logic) {
 }
 
-std::string SetBenchmarkLogicCommand::getLogic() const {
+std::string SetBenchmarkLogicCommand::getLogic() const throw() {
   return d_logic;
 }
 
-void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) {
+void SetBenchmarkLogicCommand::invoke(SmtEngine* smtEngine) throw() {
   try {
     smtEngine->setLogic(d_logic);
-    //d_result = "success";
-  } catch(ModalException&) {
-    d_result = "error";
+    d_commandStatus = CommandSuccess::instance();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
   }
 }
 
 /* class SetInfoCommand */
 
-SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr) :
+SetInfoCommand::SetInfoCommand(std::string flag, const SExpr& sexpr) throw() :
   d_flag(flag),
   d_sexpr(sexpr) {
 }
 
-std::string SetInfoCommand::getFlag() const {
+std::string SetInfoCommand::getFlag() const throw() {
   return d_flag;
 }
 
-SExpr SetInfoCommand::getSExpr() const {
+SExpr SetInfoCommand::getSExpr() const throw() {
   return d_sexpr;
 }
 
-void SetInfoCommand::invoke(SmtEngine* smtEngine) {
+void SetInfoCommand::invoke(SmtEngine* smtEngine) throw() {
   try {
     smtEngine->setInfo(d_flag, d_sexpr);
-    //d_result = "success";
-  } catch(ModalException&) {
-    d_result = "error";
+    d_commandStatus = CommandSuccess::instance();
   } catch(BadOptionException&) {
-    d_result = "unsupported";
-  }
-}
-
-std::string SetInfoCommand::getResult() const {
-  return d_result;
-}
-
-void SetInfoCommand::printResult(std::ostream& out) const {
-  if(d_result != "") {
-    out << d_result << endl;
+    d_commandStatus = new CommandUnsupported();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
   }
 }
 
 /* class GetInfoCommand */
 
-GetInfoCommand::GetInfoCommand(std::string flag) :
+GetInfoCommand::GetInfoCommand(std::string flag) throw() :
   d_flag(flag) {
 }
 
-std::string GetInfoCommand::getFlag() const {
+std::string GetInfoCommand::getFlag() const throw() {
   return d_flag;
 }
 
-void GetInfoCommand::invoke(SmtEngine* smtEngine) {
+void GetInfoCommand::invoke(SmtEngine* smtEngine) throw() {
   try {
     stringstream ss;
     ss << smtEngine->getInfo(d_flag);
     d_result = ss.str();
+    d_commandStatus = CommandSuccess::instance();
   } catch(BadOptionException&) {
-    d_result = "unsupported";
+    d_commandStatus = new CommandUnsupported();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
   }
 }
 
-std::string GetInfoCommand::getResult() const {
+std::string GetInfoCommand::getResult() const throw() {
   return d_result;
 }
 
-void GetInfoCommand::printResult(std::ostream& out) const {
-  if(d_result != "") {
+void GetInfoCommand::printResult(std::ostream& out) const throw() {
+  if(! ok()) {
+    this->Command::printResult(out);
+  } else if(d_result != "") {
     out << d_result << endl;
   }
 }
 
 /* class SetOptionCommand */
 
-SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr) :
+SetOptionCommand::SetOptionCommand(std::string flag, const SExpr& sexpr) throw() :
   d_flag(flag),
   d_sexpr(sexpr) {
 }
 
-std::string SetOptionCommand::getFlag() const {
+std::string SetOptionCommand::getFlag() const throw() {
   return d_flag;
 }
 
-SExpr SetOptionCommand::getSExpr() const {
+SExpr SetOptionCommand::getSExpr() const throw() {
   return d_sexpr;
 }
 
-void SetOptionCommand::invoke(SmtEngine* smtEngine) {
+void SetOptionCommand::invoke(SmtEngine* smtEngine) throw() {
   try {
     smtEngine->setOption(d_flag, d_sexpr);
-    //d_result = "success";
-  } catch(ModalException&) {
-    d_result = "error";
+    d_commandStatus = CommandSuccess::instance();
   } catch(BadOptionException&) {
-    d_result = "unsupported";
-  }
-}
-
-std::string SetOptionCommand::getResult() const {
-  return d_result;
-}
-
-void SetOptionCommand::printResult(std::ostream& out) const {
-  if(d_result != "") {
-    out << d_result << endl;
+    d_commandStatus = new CommandUnsupported();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
   }
 }
 
 /* class GetOptionCommand */
 
-GetOptionCommand::GetOptionCommand(std::string flag) :
+GetOptionCommand::GetOptionCommand(std::string flag) throw() :
   d_flag(flag) {
 }
 
-std::string GetOptionCommand::getFlag() const {
+std::string GetOptionCommand::getFlag() const throw() {
   return d_flag;
 }
 
-void GetOptionCommand::invoke(SmtEngine* smtEngine) {
+void GetOptionCommand::invoke(SmtEngine* smtEngine) throw() {
   try {
     d_result = smtEngine->getOption(d_flag).getValue();
+    d_commandStatus = CommandSuccess::instance();
   } catch(BadOptionException&) {
-    d_result = "unsupported";
+    d_commandStatus = new CommandUnsupported();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
   }
 }
 
-std::string GetOptionCommand::getResult() const {
+std::string GetOptionCommand::getResult() const throw() {
   return d_result;
 }
 
-void GetOptionCommand::printResult(std::ostream& out) const {
-  if(d_result != "") {
+void GetOptionCommand::printResult(std::ostream& out) const throw() {
+  if(! ok()) {
+    this->Command::printResult(out);
+  } else if(d_result != "") {
     out << d_result << endl;
   }
 }
 
 /* class DatatypeDeclarationCommand */
 
-DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) :
+DatatypeDeclarationCommand::DatatypeDeclarationCommand(const DatatypeType& datatype) throw() :
   d_datatypes() {
   d_datatypes.push_back(datatype);
 }
 
-DatatypeDeclarationCommand::DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) :
+DatatypeDeclarationCommand::DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) throw() :
   d_datatypes(datatypes) {
 }
 
 const std::vector<DatatypeType>&
-DatatypeDeclarationCommand::getDatatypes() const {
+DatatypeDeclarationCommand::getDatatypes() const throw() {
   return d_datatypes;
 }
 
-void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) {
+void DatatypeDeclarationCommand::invoke(SmtEngine* smtEngine) throw() {
   Dump("declarations") << *this << endl;
+  d_commandStatus = CommandSuccess::instance();
 }
 
 /* output stream insertion operator for benchmark statuses */
 std::ostream& operator<<(std::ostream& out,
-                         BenchmarkStatus status) {
+                         BenchmarkStatus status) throw() {
   switch(status) {
 
   case SMT_SATISFIABLE:
diff --git a/src/expr/command.h b/src/expr/command.h
index b686025fe..cf8c1b615 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -41,9 +41,12 @@ namespace CVC4 {
 
 class SmtEngine;
 class Command;
+class CommandStatus;
 
-std::ostream& operator<<(std::ostream&, const Command&) CVC4_PUBLIC;
-std::ostream& operator<<(std::ostream&, const Command*) CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream&, const Command&) throw() CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream&, const Command*) throw() CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream&, const CommandStatus&) throw() CVC4_PUBLIC;
+std::ostream& operator<<(std::ostream&, const CommandStatus*) throw() CVC4_PUBLIC;
 
 /** The status an SMT benchmark can have */
 enum BenchmarkStatus {
@@ -56,21 +59,156 @@ enum BenchmarkStatus {
 };
 
 std::ostream& operator<<(std::ostream& out,
-                         BenchmarkStatus status) CVC4_PUBLIC;
+                         BenchmarkStatus status) throw() CVC4_PUBLIC;
+
+/**
+ * IOStream manipulator to print success messages or not.
+ *
+ *   out << Command::printsuccess(false) << CommandSuccess();
+ *
+ * prints nothing, but
+ *
+ *   out << Command::printsuccess(true) << CommandSuccess();
+ *
+ * prints a success message (in a manner appropriate for the current
+ * output language).
+ */
+class CVC4_PUBLIC CommandPrintSuccess {
+  /**
+   * The allocated index in ios_base for our depth setting.
+   */
+  static const int s_iosIndex;
+
+  /**
+   * The default setting, for ostreams that haven't yet had a
+   * setdepth() applied to them.
+   */
+  static const int s_defaultPrintSuccess = false;
+
+  /**
+   * When this manipulator is used, the setting is stored here.
+   */
+  bool d_printSuccess;
+
+public:
+  /**
+   * Construct a CommandPrintSuccess with the given setting.
+   */
+  CommandPrintSuccess(bool printSuccess) throw() : d_printSuccess(printSuccess) {}
+
+  inline void applyPrintSuccess(std::ostream& out) throw() {
+    out.iword(s_iosIndex) = d_printSuccess;
+  }
+
+  static inline bool getPrintSuccess(std::ostream& out) throw() {
+    return out.iword(s_iosIndex);
+  }
+
+  static inline void setPrintSuccess(std::ostream& out, bool printSuccess) throw() {
+    out.iword(s_iosIndex) = printSuccess;
+  }
+
+  /**
+   * Set the print-success state on the output stream for the current
+   * stack scope.  This makes sure the old state is reset on the
+   * stream after normal OR exceptional exit from the scope, using the
+   * RAII C++ idiom.
+   */
+  class Scope {
+    std::ostream& d_out;
+    bool d_oldPrintSuccess;
+
+  public:
+
+    inline Scope(std::ostream& out, bool printSuccess) throw() :
+      d_out(out),
+      d_oldPrintSuccess(CommandPrintSuccess::getPrintSuccess(out)) {
+      CommandPrintSuccess::setPrintSuccess(out, printSuccess);
+    }
+
+    inline ~Scope() throw() {
+      CommandPrintSuccess::setPrintSuccess(d_out, d_oldPrintSuccess);
+    }
+
+  };/* class CommandPrintSuccess::Scope */
+
+};/* class CommandPrintSuccess */
+
+/**
+ * Sets the default print-success setting when pretty-printing an Expr
+ * to an ostream.  Use like this:
+ *
+ *   // let out be an ostream, e an Expr
+ *   out << Expr::setdepth(n) << e << endl;
+ *
+ * The depth stays permanently (until set again) with the stream.
+ */
+inline std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps) throw() CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream& out, CommandPrintSuccess cps) throw() {
+  cps.applyPrintSuccess(out);
+  return out;
+}
+
+class CVC4_PUBLIC CommandStatus {
+protected:
+  // shouldn't construct a CommandStatus (use a derived class)
+  CommandStatus() throw() {}
+public:
+  virtual ~CommandStatus() throw() {}
+  void toStream(std::ostream& out,
+                OutputLanguage language = language::output::LANG_AST) const throw();
+};/* class CommandStatus */
+
+class CVC4_PUBLIC CommandSuccess : public CommandStatus {
+  static const CommandSuccess* s_instance;
+public:
+  static const CommandSuccess* instance() throw() { return s_instance; }
+};/* class CommandSuccess */
+
+class CVC4_PUBLIC CommandUnsupported : public CommandStatus {
+};/* class CommandSuccess */
+
+class CVC4_PUBLIC CommandFailure : public CommandStatus {
+  std::string d_message;
+public:
+  CommandFailure(std::string message) throw() : d_message(message) {}
+  ~CommandFailure() throw() {}
+  std::string getMessage() const throw() { return d_message; }
+};/* class CommandFailure */
 
 class CVC4_PUBLIC Command {
+protected:
+  /**
+   * This field contains a command status if the command has been
+   * invoked, or NULL if it has not.  This field is either a
+   * dynamically-allocated pointer, or it's a pointer to the singleton
+   * CommandSuccess instance.  Doing so is somewhat asymmetric, but
+   * it avoids the need to dynamically allocate memory in the common
+   * case of a successful command.
+   */
+  const CommandStatus* d_commandStatus;
+
 public:
-  virtual ~Command() {}
+  typedef CommandPrintSuccess printsuccess;
+
+  Command() throw();
+  virtual ~Command() throw();
 
-  virtual void invoke(SmtEngine* smtEngine) = 0;
-  virtual void invoke(SmtEngine* smtEngine, std::ostream& out);
+  virtual void invoke(SmtEngine* smtEngine) throw() = 0;
+  virtual void invoke(SmtEngine* smtEngine, std::ostream& out) throw();
 
   virtual void toStream(std::ostream& out, int toDepth = -1, bool types = false,
-                        OutputLanguage language = language::output::LANG_AST) const;
+                        OutputLanguage language = language::output::LANG_AST) const throw();
+
+  std::string toString() const throw();
+
+  /** Either the command hasn't run yet, or it completed successfully. */
+  bool ok() const throw();
 
-  std::string toString() const;
+  /** Get the command status (it's NULL if we haven't run yet). */
+  const CommandStatus* getCommandStatus() const throw() { return d_commandStatus; }
 
-  virtual void printResult(std::ostream& out) const;
+  virtual void printResult(std::ostream& out) const throw();
 
 };/* class Command */
 
@@ -82,45 +220,51 @@ class CVC4_PUBLIC EmptyCommand : public Command {
 protected:
   std::string d_name;
 public:
-  EmptyCommand(std::string name = "");
-  std::string getName() const;
-  void invoke(SmtEngine* smtEngine);
+  EmptyCommand(std::string name = "") throw();
+  ~EmptyCommand() throw() {}
+  std::string getName() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class EmptyCommand */
 
 class CVC4_PUBLIC AssertCommand : public Command {
 protected:
   BoolExpr d_expr;
 public:
-  AssertCommand(const BoolExpr& e);
-  BoolExpr getExpr() const;
-  void invoke(SmtEngine* smtEngine);
+  AssertCommand(const BoolExpr& e) throw();
+  ~AssertCommand() throw() {}
+  BoolExpr getExpr() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class AssertCommand */
 
 class CVC4_PUBLIC PushCommand : public Command {
 public:
-  void invoke(SmtEngine* smtEngine);
+  ~PushCommand() throw() {}
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class PushCommand */
 
 class CVC4_PUBLIC PopCommand : public Command {
 public:
-  void invoke(SmtEngine* smtEngine);
+  ~PopCommand() throw() {}
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class PopCommand */
 
 class CVC4_PUBLIC DeclarationDefinitionCommand : public Command {
 protected:
   std::string d_symbol;
 public:
-  DeclarationDefinitionCommand(const std::string& id);
-  std::string getSymbol() const;
+  DeclarationDefinitionCommand(const std::string& id) throw();
+  ~DeclarationDefinitionCommand() throw() {}
+  std::string getSymbol() const throw();
 };/* class DeclarationDefinitionCommand */
 
 class CVC4_PUBLIC DeclareFunctionCommand : public DeclarationDefinitionCommand {
 protected:
   Type d_type;
 public:
-  DeclareFunctionCommand(const std::string& id, Type type);
-  Type getType() const;
-  void invoke(SmtEngine* smtEngine);
+  DeclareFunctionCommand(const std::string& id, Type type) throw();
+  ~DeclareFunctionCommand() throw() {}
+  Type getType() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class DeclareFunctionCommand */
 
 class CVC4_PUBLIC DeclareTypeCommand : public DeclarationDefinitionCommand {
@@ -128,10 +272,11 @@ protected:
   size_t d_arity;
   Type d_type;
 public:
-  DeclareTypeCommand(const std::string& id, size_t arity, Type t);
-  size_t getArity() const;
-  Type getType() const;
-  void invoke(SmtEngine* smtEngine);
+  DeclareTypeCommand(const std::string& id, size_t arity, Type t) throw();
+  ~DeclareTypeCommand() throw() {}
+  size_t getArity() const throw();
+  Type getType() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class DeclareTypeCommand */
 
 class CVC4_PUBLIC DefineTypeCommand : public DeclarationDefinitionCommand {
@@ -139,11 +284,12 @@ protected:
   std::vector<Type> d_params;
   Type d_type;
 public:
-  DefineTypeCommand(const std::string& id, Type t);
-  DefineTypeCommand(const std::string& id, const std::vector<Type>& params, Type t);
-  const std::vector<Type>& getParameters() const;
-  Type getType() const;
-  void invoke(SmtEngine* smtEngine);
+  DefineTypeCommand(const std::string& id, Type t) throw();
+  DefineTypeCommand(const std::string& id, const std::vector<Type>& params, Type t) throw();
+  ~DefineTypeCommand() throw() {}
+  const std::vector<Type>& getParameters() const throw();
+  Type getType() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class DefineTypeCommand */
 
 class CVC4_PUBLIC DefineFunctionCommand : public DeclarationDefinitionCommand {
@@ -152,13 +298,14 @@ protected:
   std::vector<Expr> d_formals;
   Expr d_formula;
 public:
-  DefineFunctionCommand(const std::string& id, Expr func, Expr formula);
+  DefineFunctionCommand(const std::string& id, Expr func, Expr formula) throw();
   DefineFunctionCommand(const std::string& id, Expr func,
-                        const std::vector<Expr>& formals, Expr formula);
-  Expr getFunction() const;
-  const std::vector<Expr>& getFormals() const;
-  Expr getFormula() const;
-  void invoke(SmtEngine* smtEngine);
+                        const std::vector<Expr>& formals, Expr formula) throw();
+  ~DefineFunctionCommand() throw() {}
+  Expr getFunction() const throw();
+  const std::vector<Expr>& getFormals() const throw();
+  Expr getFormula() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class DefineFunctionCommand */
 
 /**
@@ -169,8 +316,8 @@ public:
 class CVC4_PUBLIC DefineNamedFunctionCommand : public DefineFunctionCommand {
 public:
   DefineNamedFunctionCommand(const std::string& id, Expr func,
-                             const std::vector<Expr>& formals, Expr formula);
-  void invoke(SmtEngine* smtEngine);
+                             const std::vector<Expr>& formals, Expr formula) throw();
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class DefineNamedFunctionCommand */
 
 class CVC4_PUBLIC CheckSatCommand : public Command {
@@ -178,12 +325,13 @@ protected:
   BoolExpr d_expr;
   Result d_result;
 public:
-  CheckSatCommand();
-  CheckSatCommand(const BoolExpr& expr);
-  BoolExpr getExpr() const;
-  void invoke(SmtEngine* smtEngine);
-  Result getResult() const;
-  void printResult(std::ostream& out) const;
+  CheckSatCommand() throw();
+  CheckSatCommand(const BoolExpr& expr) throw();
+  ~CheckSatCommand() throw() {}
+  BoolExpr getExpr() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
+  Result getResult() const throw();
+  void printResult(std::ostream& out) const throw();
 };/* class CheckSatCommand */
 
 class CVC4_PUBLIC QueryCommand : public Command {
@@ -191,11 +339,12 @@ protected:
   BoolExpr d_expr;
   Result d_result;
 public:
-  QueryCommand(const BoolExpr& e);
-  BoolExpr getExpr() const;
-  void invoke(SmtEngine* smtEngine);
-  Result getResult() const;
-  void printResult(std::ostream& out) const;
+  QueryCommand(const BoolExpr& e) throw();
+  ~QueryCommand() throw() {}
+  BoolExpr getExpr() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
+  Result getResult() const throw();
+  void printResult(std::ostream& out) const throw();
 };/* class QueryCommand */
 
 // this is TRANSFORM in the CVC presentation language
@@ -204,11 +353,12 @@ protected:
   Expr d_term;
   Expr d_result;
 public:
-  SimplifyCommand(Expr term);
-  Expr getTerm() const;
-  void invoke(SmtEngine* smtEngine);
-  Expr getResult() const;
-  void printResult(std::ostream& out) const;
+  SimplifyCommand(Expr term) throw();
+  ~SimplifyCommand() throw() {}
+  Expr getTerm() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
+  Expr getResult() const throw();
+  void printResult(std::ostream& out) const throw();
 };/* class SimplifyCommand */
 
 class CVC4_PUBLIC GetValueCommand : public Command {
@@ -216,75 +366,77 @@ protected:
   Expr d_term;
   Expr d_result;
 public:
-  GetValueCommand(Expr term);
-  Expr getTerm() const;
-  void invoke(SmtEngine* smtEngine);
-  Expr getResult() const;
-  void printResult(std::ostream& out) const;
+  GetValueCommand(Expr term) throw();
+  ~GetValueCommand() throw() {}
+  Expr getTerm() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
+  Expr getResult() const throw();
+  void printResult(std::ostream& out) const throw();
 };/* class GetValueCommand */
 
 class CVC4_PUBLIC GetAssignmentCommand : public Command {
 protected:
   SExpr d_result;
 public:
-  GetAssignmentCommand();
-  void invoke(SmtEngine* smtEngine);
-  SExpr getResult() const;
-  void printResult(std::ostream& out) const;
+  GetAssignmentCommand() throw();
+  ~GetAssignmentCommand() throw() {}
+  void invoke(SmtEngine* smtEngine) throw();
+  SExpr getResult() const throw();
+  void printResult(std::ostream& out) const throw();
 };/* class GetAssignmentCommand */
 
 class CVC4_PUBLIC GetProofCommand : public Command {
 protected:
   Proof* d_result;
 public:
-  GetProofCommand();
-  void invoke(SmtEngine* smtEngine);
-  Proof* getResult() const;
-  void printResult(std::ostream& out) const;
+  GetProofCommand() throw();
+  ~GetProofCommand() throw() {}
+  void invoke(SmtEngine* smtEngine) throw();
+  Proof* getResult() const throw();
+  void printResult(std::ostream& out) const throw();
 };/* class GetProofCommand */
 
 class CVC4_PUBLIC GetAssertionsCommand : public Command {
 protected:
   std::string d_result;
 public:
-  GetAssertionsCommand();
-  void invoke(SmtEngine* smtEngine);
-  std::string getResult() const;
-  void printResult(std::ostream& out) const;
+  GetAssertionsCommand() throw();
+  ~GetAssertionsCommand() throw() {}
+  void invoke(SmtEngine* smtEngine) throw();
+  std::string getResult() const throw();
+  void printResult(std::ostream& out) const throw();
 };/* class GetAssertionsCommand */
 
 class CVC4_PUBLIC SetBenchmarkStatusCommand : public Command {
 protected:
-  std::string d_result;
   BenchmarkStatus d_status;
 public:
-  SetBenchmarkStatusCommand(BenchmarkStatus status);
-  BenchmarkStatus getStatus() const;
-  void invoke(SmtEngine* smtEngine);
+  SetBenchmarkStatusCommand(BenchmarkStatus status) throw();
+  ~SetBenchmarkStatusCommand() throw() {}
+  BenchmarkStatus getStatus() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class SetBenchmarkStatusCommand */
 
 class CVC4_PUBLIC SetBenchmarkLogicCommand : public Command {
 protected:
-  std::string d_result;
   std::string d_logic;
 public:
-  SetBenchmarkLogicCommand(std::string logic);
-  std::string getLogic() const;
-  void invoke(SmtEngine* smtEngine);
+  SetBenchmarkLogicCommand(std::string logic) throw();
+  ~SetBenchmarkLogicCommand() throw() {}
+  std::string getLogic() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class SetBenchmarkLogicCommand */
 
 class CVC4_PUBLIC SetInfoCommand : public Command {
 protected:
   std::string d_flag;
   SExpr d_sexpr;
-  std::string d_result;
 public:
-  SetInfoCommand(std::string flag, const SExpr& sexpr);
-  std::string getFlag() const;
-  SExpr getSExpr() const;
-  void invoke(SmtEngine* smtEngine);
-  std::string getResult() const;
-  void printResult(std::ostream& out) const;
+  SetInfoCommand(std::string flag, const SExpr& sexpr) throw();
+  ~SetInfoCommand() throw() {}
+  std::string getFlag() const throw();
+  SExpr getSExpr() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class SetInfoCommand */
 
 class CVC4_PUBLIC GetInfoCommand : public Command {
@@ -292,25 +444,24 @@ protected:
   std::string d_flag;
   std::string d_result;
 public:
-  GetInfoCommand(std::string flag);
-  std::string getFlag() const;
-  void invoke(SmtEngine* smtEngine);
-  std::string getResult() const;
-  void printResult(std::ostream& out) const;
+  GetInfoCommand(std::string flag) throw();
+  ~GetInfoCommand() throw() {}
+  std::string getFlag() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
+  std::string getResult() const throw();
+  void printResult(std::ostream& out) const throw();
 };/* class GetInfoCommand */
 
 class CVC4_PUBLIC SetOptionCommand : public Command {
 protected:
   std::string d_flag;
   SExpr d_sexpr;
-  std::string d_result;
 public:
-  SetOptionCommand(std::string flag, const SExpr& sexpr);
-  std::string getFlag() const;
-  SExpr getSExpr() const;
-  void invoke(SmtEngine* smtEngine);
-  std::string getResult() const;
-  void printResult(std::ostream& out) const;
+  SetOptionCommand(std::string flag, const SExpr& sexpr) throw();
+  ~SetOptionCommand() throw() {}
+  std::string getFlag() const throw();
+  SExpr getSExpr() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class SetOptionCommand */
 
 class CVC4_PUBLIC GetOptionCommand : public Command {
@@ -318,35 +469,39 @@ protected:
   std::string d_flag;
   std::string d_result;
 public:
-  GetOptionCommand(std::string flag);
-  std::string getFlag() const;
-  void invoke(SmtEngine* smtEngine);
-  std::string getResult() const;
-  void printResult(std::ostream& out) const;
+  GetOptionCommand(std::string flag) throw();
+  ~GetOptionCommand() throw() {}
+  std::string getFlag() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
+  std::string getResult() const throw();
+  void printResult(std::ostream& out) const throw();
 };/* class GetOptionCommand */
 
 class CVC4_PUBLIC DatatypeDeclarationCommand : public Command {
 private:
   std::vector<DatatypeType> d_datatypes;
 public:
-  DatatypeDeclarationCommand(const DatatypeType& datatype);
-  DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes);
-  const std::vector<DatatypeType>& getDatatypes() const;
-  void invoke(SmtEngine* smtEngine);
+  DatatypeDeclarationCommand(const DatatypeType& datatype) throw();
+  ~DatatypeDeclarationCommand() throw() {}
+  DatatypeDeclarationCommand(const std::vector<DatatypeType>& datatypes) throw();
+  const std::vector<DatatypeType>& getDatatypes() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class DatatypeDeclarationCommand */
 
 class CVC4_PUBLIC QuitCommand : public Command {
 public:
-  QuitCommand();
-  void invoke(SmtEngine* smtEngine);
+  QuitCommand() throw();
+  ~QuitCommand() throw() {}
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class QuitCommand */
 
 class CVC4_PUBLIC CommentCommand : public Command {
   std::string d_comment;
 public:
-  CommentCommand(std::string comment);
-  std::string getComment() const;
-  void invoke(SmtEngine* smtEngine);
+  CommentCommand(std::string comment) throw();
+  ~CommentCommand() throw() {}
+  std::string getComment() const throw();
+  void invoke(SmtEngine* smtEngine) throw();
 };/* class CommentCommand */
 
 class CVC4_PUBLIC CommandSequence : public Command {
@@ -356,27 +511,28 @@ private:
   /** Next command to be executed */
   unsigned int d_index;
 public:
-  CommandSequence();
-  ~CommandSequence();
+  CommandSequence() throw();
+  ~CommandSequence() throw();
 
-  void addCommand(Command* cmd);
+  void addCommand(Command* cmd) throw();
 
-  void invoke(SmtEngine* smtEngine);
-  void invoke(SmtEngine* smtEngine, std::ostream& out);
+  void invoke(SmtEngine* smtEngine) throw();
+  void invoke(SmtEngine* smtEngine, std::ostream& out) throw();
 
   typedef std::vector<Command*>::iterator iterator;
   typedef std::vector<Command*>::const_iterator const_iterator;
 
-  const_iterator begin() const;
-  const_iterator end() const;
+  const_iterator begin() const throw();
+  const_iterator end() const throw();
 
-  iterator begin();
-  iterator end();
+  iterator begin() throw();
+  iterator end() throw();
 
 };/* class CommandSequence */
 
 class CVC4_PUBLIC DeclarationSequence : public CommandSequence {
 public:
+  ~DeclarationSequence() throw() {}
 };/* class DeclarationSequence */
 
 }/* CVC4 namespace */
diff --git a/src/expr/command.i b/src/expr/command.i
index 3a029b785..a4bf5473e 100644
--- a/src/expr/command.i
+++ b/src/expr/command.i
@@ -2,11 +2,11 @@
 #include "expr/command.h"
 %}
 
-%ignore CVC4::operator<<(std::ostream&, const Command&);
-%ignore CVC4::operator<<(std::ostream&, const Command*);
-%ignore CVC4::operator<<(std::ostream&, BenchmarkStatus status);
+%ignore CVC4::operator<<(std::ostream&, const Command&) throw();
+%ignore CVC4::operator<<(std::ostream&, const Command*) throw();
+%ignore CVC4::operator<<(std::ostream&, BenchmarkStatus status) throw();
 
-%rename(beginConst) CVC4::CommandSequence::begin() const;
-%rename(endConst) CVC4::CommandSequence::end() const;
+%rename(beginConst) CVC4::CommandSequence::begin() const throw();
+%rename(endConst) CVC4::CommandSequence::end() const throw();
 
 %include "expr/command.h"
diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 619fd5280..29aa1a737 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -56,31 +56,28 @@ std::ostream& operator<<(std::ostream& out, const Expr& e) {
   return out << e.getNode();
 }
 
-TypeCheckingException::TypeCheckingException(const TypeCheckingException& t)
-: Exception(t.d_msg), d_expr(new Expr(t.getExpression()))
-  {}
-
+TypeCheckingException::TypeCheckingException(const TypeCheckingException& t) throw() :
+  Exception(t.d_msg), d_expr(new Expr(t.getExpression())) {
+}
 
-TypeCheckingException::TypeCheckingException(const Expr& expr, std::string message)
-: Exception(message), d_expr(new Expr(expr))
-{
+TypeCheckingException::TypeCheckingException(const Expr& expr, std::string message) throw() :
+  Exception(message), d_expr(new Expr(expr)) {
 }
 
 TypeCheckingException::TypeCheckingException(ExprManager* em,
-                                             const TypeCheckingExceptionPrivate* exc)
-: Exception(exc->getMessage()), d_expr(new Expr(em, new Node(exc->getNode())))
-{
+                                             const TypeCheckingExceptionPrivate* exc) throw() :
+  Exception(exc->getMessage()), d_expr(new Expr(em, new Node(exc->getNode()))) {
 }
 
-TypeCheckingException::~TypeCheckingException() throw () {
+TypeCheckingException::~TypeCheckingException() throw() {
   delete d_expr;
 }
 
-void TypeCheckingException::toStream(std::ostream& os) const {
+void TypeCheckingException::toStream(std::ostream& os) const throw() {
   os << "Error type-checking " << d_expr << ": " << d_msg << endl << *d_expr;
 }
 
-Expr TypeCheckingException::getExpression() const {
+Expr TypeCheckingException::getExpression() const throw() {
   return *d_expr;
 }
 
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index 616a7c8ff..b54ec20d4 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -81,32 +81,32 @@ private:
 
 protected:
 
-  TypeCheckingException() : Exception() {}
-  TypeCheckingException(const Expr& expr, std::string message);
+  TypeCheckingException() throw() : Exception() {}
+  TypeCheckingException(const Expr& expr, std::string message) throw();
   TypeCheckingException(ExprManager* em,
-                        const TypeCheckingExceptionPrivate* exc);
+                        const TypeCheckingExceptionPrivate* exc) throw();
 
 public:
 
   /** Copy constructor */
-  TypeCheckingException(const TypeCheckingException& t);
+  TypeCheckingException(const TypeCheckingException& t) throw();
 
   /** Destructor */
-  ~TypeCheckingException() throw ();
+  ~TypeCheckingException() throw();
 
   /**
    * Get the Expr that caused the type-checking to fail.
    *
    * @return the expr
    */
-  Expr getExpression() const;
+  Expr getExpression() const throw();
 
   /**
    * Returns the message corresponding to the type-checking failure.
    * We prefer toStream() to toString() because that keeps the expr-depth
    * and expr-language settings present in the stream.
    */
-  void toStream(std::ostream& out) const;
+  void toStream(std::ostream& out) const throw();
 
   friend class ExprManager;
 };/* class TypeCheckingException */
@@ -457,9 +457,13 @@ public:
    *
    *   // let a, b, c, and d be variables of sort U
    *   Expr e = em->mkExpr(OR, a, b, em->mkExpr(AND, c, em->mkExpr(NOT, d)))
-   *   out << e;
+   *   out << printtypes(true) << e;
    *
    * gives "(OR a:U b:U (AND c:U (NOT d:U)))", but
+   *
+   *   out << printtypes(false) << [same expr as above]
+   *
+   * gives "(OR a b (AND c (NOT d)))"
    */
   typedef expr::ExprPrintTypes printtypes;
 
@@ -824,7 +828,7 @@ public:
 
 ${getConst_instantiations}
 
-#line 828 "${template}"
+#line 832 "${template}"
 
 namespace expr {
 
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 586d0cb13..695e572ab 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -26,7 +26,7 @@ using namespace std;
 namespace CVC4 {
 
 TypeCheckingExceptionPrivate::TypeCheckingExceptionPrivate(TNode node,
-                                                           std::string message) :
+                                                           std::string message) throw() :
   Exception(message),
   d_node(new Node(node)) {
 }
@@ -35,11 +35,11 @@ TypeCheckingExceptionPrivate::~TypeCheckingExceptionPrivate() throw () {
   delete d_node;
 }
 
-void TypeCheckingExceptionPrivate::toStream(std::ostream& os) const {
+void TypeCheckingExceptionPrivate::toStream(std::ostream& os) const throw() {
   os << "Error type-checking " << d_node << ": " << d_msg << std::endl << *d_node;
 }
 
-Node TypeCheckingExceptionPrivate::getNode() const {
+NodeTemplate<true> TypeCheckingExceptionPrivate::getNode() const throw() {
   return *d_node;
 }
 
diff --git a/src/expr/node.h b/src/expr/node.h
index 2751c96a8..57b02b05b 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -65,7 +65,7 @@ private:
 
 protected:
 
-  TypeCheckingExceptionPrivate() : Exception() {}
+  TypeCheckingExceptionPrivate() throw() : Exception() {}
 
 public:
 
@@ -74,7 +74,7 @@ public:
    * @param node the problematic node
    * @param message the message explaining the failure
    */
-  TypeCheckingExceptionPrivate(NodeTemplate<false> node, std::string message);
+  TypeCheckingExceptionPrivate(NodeTemplate<false> node, std::string message) throw();
 
   /** Destructor */
   ~TypeCheckingExceptionPrivate() throw ();
@@ -83,14 +83,14 @@ public:
    * Get the Node that caused the type-checking to fail.
    * @return the node
    */
-  NodeTemplate<true> getNode() const;
+  NodeTemplate<true> getNode() const throw();
 
   /**
    * Returns the message corresponding to the type-checking failure.
    * We prefer toStream() to toString() because that keeps the expr-depth
    * and expr-language settings present in the stream.
    */
-  void toStream(std::ostream& out) const;
+  void toStream(std::ostream& out) const throw();
 
 };/* class TypeCheckingExceptionPrivate */
 
diff --git a/src/expr/type.i b/src/expr/type.i
index 314903342..acde96955 100644
--- a/src/expr/type.i
+++ b/src/expr/type.i
@@ -18,6 +18,7 @@
 %rename(toIntegerType) CVC4::Type::operator IntegerType() const;
 %rename(toRealType) CVC4::Type::operator RealType() const;
 %rename(toPseudobooleanType) CVC4::Type::operator PseudobooleanType() const;
+%rename(toStringType) CVC4::Type::operator StringType() const;
 %rename(toBitVectorType) CVC4::Type::operator BitVectorType() const;
 %rename(toFunctionType) CVC4::Type::operator FunctionType() const;
 %rename(toTupleType) CVC4::Type::operator TupleType() const;
diff --git a/src/include/cvc4_public.h b/src/include/cvc4_public.h
index 6dec72736..398ec57e2 100644
--- a/src/include/cvc4_public.h
+++ b/src/include/cvc4_public.h
@@ -85,8 +85,4 @@
 #define EXPECT_TRUE(x) __builtin_expect( (x), true )
 #define EXPECT_FALSE(x) __builtin_expect( (x), false )
 
-#ifndef NULL
-#  define NULL ((void*) 0)
-#endif
-
 #endif /* __CVC4_PUBLIC_H */
diff --git a/src/main/interactive_shell.cpp b/src/main/interactive_shell.cpp
index f2d6f1714..dca554330 100644
--- a/src/main/interactive_shell.cpp
+++ b/src/main/interactive_shell.cpp
@@ -268,11 +268,11 @@ Command* InteractiveShell::readCommand() {
         if(dynamic_cast<DeclareFunctionCommand*>(cmd) != NULL) {
           s_declarations.insert(dynamic_cast<DeclareFunctionCommand*>(cmd)->getSymbol());
         } else if(dynamic_cast<DefineFunctionCommand*>(cmd) != NULL) {
-          s_declarations.insert(dynamic_cast<DeclareFunctionCommand*>(cmd)->getSymbol());
+          s_declarations.insert(dynamic_cast<DefineFunctionCommand*>(cmd)->getSymbol());
         } else if(dynamic_cast<DeclareTypeCommand*>(cmd) != NULL) {
-          s_declarations.insert(dynamic_cast<DeclareFunctionCommand*>(cmd)->getSymbol());
+          s_declarations.insert(dynamic_cast<DeclareTypeCommand*>(cmd)->getSymbol());
         } else if(dynamic_cast<DefineTypeCommand*>(cmd) != NULL) {
-          s_declarations.insert(dynamic_cast<DeclareFunctionCommand*>(cmd)->getSymbol());
+          s_declarations.insert(dynamic_cast<DefineTypeCommand*>(cmd)->getSymbol());
         }
 #endif /* HAVE_LIBREADLINE */
       }
diff --git a/src/parser/parser_exception.h b/src/parser/parser_exception.h
index d32914d8e..1f2d619ce 100644
--- a/src/parser/parser_exception.h
+++ b/src/parser/parser_exception.h
@@ -33,20 +33,20 @@ namespace parser {
 class CVC4_PUBLIC ParserException : public Exception {
 public:
   // Constructors
-  ParserException() :
+  ParserException() throw() :
     d_filename(),
     d_line(0),
     d_column(0) {
   }
 
-  ParserException(const std::string& msg) :
+  ParserException(const std::string& msg) throw() :
     Exception(msg),
     d_filename(),
     d_line(0),
     d_column(0) {
   }
 
-  ParserException(const char* msg) :
+  ParserException(const char* msg) throw() :
     Exception(msg),
     d_filename(),
     d_line(0),
@@ -54,7 +54,7 @@ public:
   }
 
   ParserException(const std::string& msg, const std::string& filename,
-                  unsigned long line, unsigned long column) :
+                  unsigned long line, unsigned long column) throw() :
     Exception(msg),
     d_filename(filename),
     d_line(line),
@@ -64,7 +64,7 @@ public:
   // Destructor
   virtual ~ParserException() throw() {}
 
-  virtual void toStream(std::ostream& os) const {
+  virtual void toStream(std::ostream& os) const throw() {
     if( d_line > 0 ) {
       os <<  "Parse Error: " << d_filename << ":" << d_line << "."
          << d_column << ": " << d_msg;
@@ -73,15 +73,15 @@ public:
     }
   }
 
-  std::string getFilename() const {
+  std::string getFilename() const throw() {
     return d_filename;
   }
 
-  int getLine() const {
+  int getLine() const throw() {
     return d_line;
   }
 
-  int getColumn() const {
+  int getColumn() const throw() {
     return d_column;
   }
 
diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index 082765765..b941957c4 100644
--- a/src/printer/ast/ast_printer.cpp
+++ b/src/printer/ast/ast_printer.cpp
@@ -34,7 +34,7 @@ namespace printer {
 namespace ast {
 
 void AstPrinter::toStream(std::ostream& out, TNode n,
-                          int toDepth, bool types) const {
+                          int toDepth, bool types) const throw() {
   // null
   if(n.getKind() == kind::NULL_EXPR) {
     out << "null";
@@ -95,13 +95,13 @@ void AstPrinter::toStream(std::ostream& out, TNode n,
     }
   }
   out << ')';
-}/* AstPrinter::toStream() */
+}/* AstPrinter::toStream(TNode) */
 
 template <class T>
-static bool tryToStream(std::ostream& out, const Command* c);
+static bool tryToStream(std::ostream& out, const Command* c) throw();
 
 void AstPrinter::toStream(std::ostream& out, const Command* c,
-                          int toDepth, bool types) const {
+                          int toDepth, bool types) const throw() {
   expr::ExprSetDepth::Scope sdScope(out, toDepth);
   expr::ExprPrintTypes::Scope ptScope(out, types);
 
@@ -134,27 +134,44 @@ void AstPrinter::toStream(std::ostream& out, const Command* c,
     return;
   }
 
-  Unhandled("don't know how to print a Command of class: %s", typeid(*c).name());
+  out << "ERROR: don't know how to print a Command of class: "
+      << typeid(*c).name() << endl;
 
-}/* AstPrinter::toStream() */
+}/* AstPrinter::toStream(Command*) */
 
-static void toStream(std::ostream& out, const EmptyCommand* c) {
+template <class T>
+static bool tryToStream(std::ostream& out, const CommandStatus* s) throw();
+
+void AstPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw() {
+
+  if(tryToStream<CommandSuccess>(out, s) ||
+     tryToStream<CommandFailure>(out, s) ||
+     tryToStream<CommandUnsupported>(out, s)) {
+    return;
+  }
+
+  out << "ERROR: don't know how to print a CommandStatus of class: "
+      << typeid(*s).name() << endl;
+
+}/* AstPrinter::toStream(CommandStatus*) */
+
+static void toStream(std::ostream& out, const EmptyCommand* c)  throw() {
   out << "EmptyCommand(" << c->getName() << ")";
 }
 
-static void toStream(std::ostream& out, const AssertCommand* c) {
+static void toStream(std::ostream& out, const AssertCommand* c) throw() {
   out << "Assert(" << c->getExpr() << ")";
 }
 
-static void toStream(std::ostream& out, const PushCommand* c) {
+static void toStream(std::ostream& out, const PushCommand* c) throw() {
   out << "Push()";
 }
 
-static void toStream(std::ostream& out, const PopCommand* c) {
+static void toStream(std::ostream& out, const PopCommand* c) throw() {
   out << "Pop()";
 }
 
-static void toStream(std::ostream& out, const CheckSatCommand* c) {
+static void toStream(std::ostream& out, const CheckSatCommand* c) throw() {
   BoolExpr e = c->getExpr();
   if(e.isNull()) {
     out << "CheckSat()";
@@ -163,15 +180,15 @@ static void toStream(std::ostream& out, const CheckSatCommand* c) {
   }
 }
 
-static void toStream(std::ostream& out, const QueryCommand* c) {
+static void toStream(std::ostream& out, const QueryCommand* c) throw() {
   out << "Query(" << c->getExpr() << ')';
 }
 
-static void toStream(std::ostream& out, const QuitCommand* c) {
+static void toStream(std::ostream& out, const QuitCommand* c) throw() {
   out << "Quit()";
 }
 
-static void toStream(std::ostream& out, const DeclarationSequence* c) {
+static void toStream(std::ostream& out, const DeclarationSequence* c) throw() {
   out << "DeclarationSequence[" << endl;
   for(CommandSequence::const_iterator i = c->begin();
       i != c->end();
@@ -181,7 +198,7 @@ static void toStream(std::ostream& out, const DeclarationSequence* c) {
   out << "]";
 }
 
-static void toStream(std::ostream& out, const CommandSequence* c) {
+static void toStream(std::ostream& out, const CommandSequence* c) throw() {
   out << "CommandSequence[" << endl;
   for(CommandSequence::const_iterator i = c->begin();
       i != c->end();
@@ -191,11 +208,11 @@ static void toStream(std::ostream& out, const CommandSequence* c) {
   out << "]";
 }
 
-static void toStream(std::ostream& out, const DeclareFunctionCommand* c) {
+static void toStream(std::ostream& out, const DeclareFunctionCommand* c) throw() {
   out << "Declare(" << c->getSymbol() << "," << c->getType() << ")";
 }
 
-static void toStream(std::ostream& out, const DefineFunctionCommand* c) {
+static void toStream(std::ostream& out, const DefineFunctionCommand* c) throw() {
   Expr func = c->getFunction();
   const std::vector<Expr>& formals = c->getFormals();
   Expr formula = c->getFormula();
@@ -208,12 +225,12 @@ static void toStream(std::ostream& out, const DefineFunctionCommand* c) {
   out << "], << " << formula << " >> )";
 }
 
-static void toStream(std::ostream& out, const DeclareTypeCommand* c) {
+static void toStream(std::ostream& out, const DeclareTypeCommand* c) throw() {
   out << "DeclareType(" << c->getSymbol() << "," << c->getArity() << ","
       << c->getType() << ")";
 }
 
-static void toStream(std::ostream& out, const DefineTypeCommand* c) {
+static void toStream(std::ostream& out, const DefineTypeCommand* c) throw() {
   const vector<Type>& params = c->getParameters();
   out << "DefineType(" << c->getSymbol() << ",[";
   if(params.size() > 0) {
@@ -224,48 +241,48 @@ static void toStream(std::ostream& out, const DefineTypeCommand* c) {
   out << "]," << c->getType() << ")";
 }
 
-static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) {
+static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) throw() {
   out << "DefineNamedFunction( ";
   toStream(out, static_cast<const DefineFunctionCommand*>(c));
   out << " )";
 }
 
-static void toStream(std::ostream& out, const SimplifyCommand* c) {
+static void toStream(std::ostream& out, const SimplifyCommand* c) throw() {
   out << "Simplify( << " << c->getTerm() << " >> )";
 }
 
-static void toStream(std::ostream& out, const GetValueCommand* c) {
+static void toStream(std::ostream& out, const GetValueCommand* c) throw() {
   out << "GetValue( << " << c->getTerm() << " >> )";
 }
 
-static void toStream(std::ostream& out, const GetAssignmentCommand* c) {
+static void toStream(std::ostream& out, const GetAssignmentCommand* c) throw() {
   out << "GetAssignment()";
 }
-static void toStream(std::ostream& out, const GetAssertionsCommand* c) {
+static void toStream(std::ostream& out, const GetAssertionsCommand* c) throw() {
   out << "GetAssertions()";
 }
-static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) {
+static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) throw() {
   out << "SetBenchmarkStatus(" << c->getStatus() << ")";
 }
-static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) {
+static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) throw() {
   out << "SetBenchmarkLogic(" << c->getLogic() << ")";
 }
-static void toStream(std::ostream& out, const SetInfoCommand* c) {
+static void toStream(std::ostream& out, const SetInfoCommand* c) throw() {
   out << "SetInfo(" << c->getFlag() << ", " << c->getSExpr() << ")";
 }
 
-static void toStream(std::ostream& out, const GetInfoCommand* c) {
+static void toStream(std::ostream& out, const GetInfoCommand* c) throw() {
   out << "GetInfo(" << c->getFlag() << ")";
 }
-static void toStream(std::ostream& out, const SetOptionCommand* c) {
+static void toStream(std::ostream& out, const SetOptionCommand* c) throw() {
   out << "SetOption(" << c->getFlag() << ", " << c->getSExpr() << ")";
 }
 
-static void toStream(std::ostream& out, const GetOptionCommand* c) {
+static void toStream(std::ostream& out, const GetOptionCommand* c) throw() {
   out << "GetOption(" << c->getFlag() << ")";
 }
 
-static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) {
+static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) throw() {
   const vector<DatatypeType>& datatypes = c->getDatatypes();
   out << "DatatypeDeclarationCommand([";
   for(vector<DatatypeType>::const_iterator i = datatypes.begin(),
@@ -277,12 +294,12 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) {
   out << "])";
 }
 
-static void toStream(std::ostream& out, const CommentCommand* c) {
+static void toStream(std::ostream& out, const CommentCommand* c) throw() {
   out << "CommentCommand([" << c->getComment() << "])";
 }
 
 template <class T>
-static bool tryToStream(std::ostream& out, const Command* c) {
+static bool tryToStream(std::ostream& out, const Command* c) throw() {
   if(typeid(*c) == typeid(T)) {
     toStream(out, dynamic_cast<const T*>(c));
     return true;
@@ -290,6 +307,29 @@ static bool tryToStream(std::ostream& out, const Command* c) {
   return false;
 }
 
+static void toStream(std::ostream& out, const CommandSuccess* s) throw() {
+  if(Command::printsuccess::getPrintSuccess(out)) {
+    out << "OK" << endl;
+  }
+}
+
+static void toStream(std::ostream& out, const CommandUnsupported* s) throw() {
+  out << "UNSUPPORTED" << endl;
+}
+
+static void toStream(std::ostream& out, const CommandFailure* s) throw() {
+  out << s->getMessage() << endl;
+}
+
+template <class T>
+static bool tryToStream(std::ostream& out, const CommandStatus* s) throw() {
+  if(typeid(*s) == typeid(T)) {
+    toStream(out, dynamic_cast<const T*>(s));
+    return true;
+  }
+  return false;
+}
+
 }/* CVC4::printer::ast namespace */
 }/* CVC4::printer namespace */
 }/* CVC4 namespace */
diff --git a/src/printer/ast/ast_printer.h b/src/printer/ast/ast_printer.h
index 69c39915b..2cae4c672 100644
--- a/src/printer/ast/ast_printer.h
+++ b/src/printer/ast/ast_printer.h
@@ -31,8 +31,9 @@ namespace ast {
 
 class AstPrinter : public CVC4::Printer {
 public:
-  void toStream(std::ostream& out, TNode n, int toDepth, bool types) const;
-  void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const;
+  void toStream(std::ostream& out, TNode n, int toDepth, bool types) const throw();
+  void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const throw();
+  void toStream(std::ostream& out, const CommandStatus* s) const throw();
 };/* class AstPrinter */
 
 }/* CVC4::printer::ast namespace */
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index fa1855ebe..0d47c9c6c 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -37,7 +37,7 @@ namespace printer {
 namespace cvc {
 
 void CvcPrinter::toStream(std::ostream& out, TNode n,
-                          int toDepth, bool types) const {
+                          int toDepth, bool types) const throw() {
   // null
   if(n.getKind() == kind::NULL_EXPR) {
     out << "NULL";
@@ -110,7 +110,7 @@ void CvcPrinter::toStream(std::ostream& out, TNode n,
         out << "TYPE";
         break;
       default:
-        Unhandled(tc);
+        out << tc;
       }
       break;
     case kind::BUILTIN:
@@ -357,15 +357,16 @@ void CvcPrinter::toStream(std::ostream& out, TNode n,
     return;
   }
 
+  // shouldn't ever happen (unless new metakinds are added)
   Unhandled();
 
-}/* CvcPrinter::toStream() */
+}/* CvcPrinter::toStream(TNode) */
 
 template <class T>
-static bool tryToStream(std::ostream& out, const Command* c);
+static bool tryToStream(std::ostream& out, const Command* c) throw();
 
 void CvcPrinter::toStream(std::ostream& out, const Command* c,
-                           int toDepth, bool types) const {
+                           int toDepth, bool types) const throw() {
   expr::ExprSetDepth::Scope sdScope(out, toDepth);
   expr::ExprPrintTypes::Scope ptScope(out, types);
 
@@ -398,23 +399,40 @@ void CvcPrinter::toStream(std::ostream& out, const Command* c,
     return;
   }
 
-  Unhandled("don't know how to print this command in CVC's presentation language: %s", c->toString().c_str());
+  out << "ERROR: don't know how to print a Command of class: "
+      << typeid(*c).name() << endl;
 
-}/* CvcPrinter::toStream() */
+}/* CvcPrinter::toStream(Command*) */
 
-static void toStream(std::ostream& out, const AssertCommand* c) {
+template <class T>
+static bool tryToStream(std::ostream& out, const CommandStatus* s) throw();
+
+void CvcPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw() {
+
+  if(tryToStream<CommandSuccess>(out, s) ||
+     tryToStream<CommandFailure>(out, s) ||
+     tryToStream<CommandUnsupported>(out, s)) {
+    return;
+  }
+
+  out << "ERROR: don't know how to print a CommandStatus of class: "
+      << typeid(*s).name() << endl;
+
+}/* CvcPrinter::toStream(CommandStatus*) */
+
+static void toStream(std::ostream& out, const AssertCommand* c) throw() {
   out << "ASSERT " << c->getExpr() << ";";
 }
 
-static void toStream(std::ostream& out, const PushCommand* c) {
+static void toStream(std::ostream& out, const PushCommand* c) throw() {
   out << "PUSH;";
 }
 
-static void toStream(std::ostream& out, const PopCommand* c) {
+static void toStream(std::ostream& out, const PopCommand* c) throw() {
   out << "POP;";
 }
 
-static void toStream(std::ostream& out, const CheckSatCommand* c) {
+static void toStream(std::ostream& out, const CheckSatCommand* c) throw() {
   BoolExpr e = c->getExpr();
   if(!e.isNull()) {
     out << "CHECKSAT " << e << ";";
@@ -423,7 +441,7 @@ static void toStream(std::ostream& out, const CheckSatCommand* c) {
   }
 }
 
-static void toStream(std::ostream& out, const QueryCommand* c) {
+static void toStream(std::ostream& out, const QueryCommand* c) throw() {
   BoolExpr e = c->getExpr();
   if(!e.isNull()) {
     out << "QUERY " << e << ";";
@@ -432,11 +450,11 @@ static void toStream(std::ostream& out, const QueryCommand* c) {
   }
 }
 
-static void toStream(std::ostream& out, const QuitCommand* c) {
+static void toStream(std::ostream& out, const QuitCommand* c) throw() {
   //out << "EXIT;";
 }
 
-static void toStream(std::ostream& out, const CommandSequence* c) {
+static void toStream(std::ostream& out, const CommandSequence* c) throw() {
   for(CommandSequence::const_iterator i = c->begin();
       i != c->end();
       ++i) {
@@ -444,7 +462,7 @@ static void toStream(std::ostream& out, const CommandSequence* c) {
   }
 }
 
-static void toStream(std::ostream& out, const DeclarationSequence* c) {
+static void toStream(std::ostream& out, const DeclarationSequence* c) throw() {
   DeclarationSequence::const_iterator i = c->begin();
   for(;;) {
     DeclarationDefinitionCommand* dd =
@@ -458,11 +476,11 @@ static void toStream(std::ostream& out, const DeclarationSequence* c) {
   }
 }
 
-static void toStream(std::ostream& out, const DeclareFunctionCommand* c) {
+static void toStream(std::ostream& out, const DeclareFunctionCommand* c) throw() {
   out << c->getSymbol() << " : " << c->getType() << ";";
 }
 
-static void toStream(std::ostream& out, const DefineFunctionCommand* c) {
+static void toStream(std::ostream& out, const DefineFunctionCommand* c) throw() {
   Expr func = c->getFunction();
   const vector<Expr>& formals = c->getFormals();
   Expr formula = c->getFormula();
@@ -477,67 +495,69 @@ static void toStream(std::ostream& out, const DefineFunctionCommand* c) {
   out << "): " << formula << ";";
 }
 
-static void toStream(std::ostream& out, const DeclareTypeCommand* c) {
+static void toStream(std::ostream& out, const DeclareTypeCommand* c) throw() {
   if(c->getArity() > 0) {
-    Unhandled("Don't know how to print parameterized type declaration "
-              "in CVC language:\n%s", c->toString().c_str());
+    out << "ERROR: Don't know how to print parameterized type declaration "
+           "in CVC language:" << endl << c->toString() << endl;
+  } else {
+    out << c->getSymbol() << " : TYPE;";
   }
-  out << c->getSymbol() << " : TYPE;";
 }
 
-static void toStream(std::ostream& out, const DefineTypeCommand* c) {
+static void toStream(std::ostream& out, const DefineTypeCommand* c) throw() {
   if(c->getParameters().size() > 0) {
-    Unhandled("Don't know how to print parameterized type definition "
-              "in CVC language:\n%s", c->toString().c_str());
+    out << "ERROR: Don't know how to print parameterized type definition "
+           "in CVC language:" << endl << c->toString() << endl;
+  } else {
+    out << c->getSymbol() << " : TYPE = " << c->getType() << ";";
   }
-  out << c->getSymbol() << " : TYPE = " << c->getType() << ";";
 }
 
-static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) {
+static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) throw() {
   toStream(out, static_cast<const DefineFunctionCommand*>(c));
 }
 
-static void toStream(std::ostream& out, const SimplifyCommand* c) {
+static void toStream(std::ostream& out, const SimplifyCommand* c) throw() {
   out << "TRANSFORM " << c->getTerm() << ";";
 }
 
-static void toStream(std::ostream& out, const GetValueCommand* c) {
+static void toStream(std::ostream& out, const GetValueCommand* c) throw() {
   out << "% (get-value " << c->getTerm() << ")";
 }
 
-static void toStream(std::ostream& out, const GetAssignmentCommand* c) {
+static void toStream(std::ostream& out, const GetAssignmentCommand* c) throw() {
   out << "% (get-assignment)";
 }
 
-static void toStream(std::ostream& out, const GetAssertionsCommand* c) {
+static void toStream(std::ostream& out, const GetAssertionsCommand* c) throw() {
   out << "% (get-assertions)";
 }
 
-static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) {
+static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) throw() {
   out << "% (set-info :status " << c->getStatus() << ")";
 }
 
-static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) {
+static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) throw() {
   out << "% (set-logic " << c->getLogic() << ")";
 }
 
-static void toStream(std::ostream& out, const SetInfoCommand* c) {
+static void toStream(std::ostream& out, const SetInfoCommand* c) throw() {
   out << "% (set-info " << c->getFlag() << " " << c->getSExpr() << ")";
 }
 
-static void toStream(std::ostream& out, const GetInfoCommand* c) {
+static void toStream(std::ostream& out, const GetInfoCommand* c) throw() {
   out << "% (get-info " << c->getFlag() << ")";
 }
 
-static void toStream(std::ostream& out, const SetOptionCommand* c) {
+static void toStream(std::ostream& out, const SetOptionCommand* c) throw() {
   out << "% (set-option " << c->getFlag() << " " << c->getSExpr() << ")";
 }
 
-static void toStream(std::ostream& out, const GetOptionCommand* c) {
+static void toStream(std::ostream& out, const GetOptionCommand* c) throw() {
   out << "% (get-option " << c->getFlag() << ")";
 }
 
-static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) {
+static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) throw() {
   const vector<DatatypeType>& datatypes = c->getDatatypes();
   for(vector<DatatypeType>::const_iterator i = datatypes.begin(),
         i_end = datatypes.end();
@@ -547,15 +567,15 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) {
   }
 }
 
-static void toStream(std::ostream& out, const CommentCommand* c) {
+static void toStream(std::ostream& out, const CommentCommand* c) throw() {
   out << "% " << c->getComment();
 }
 
-static void toStream(std::ostream& out, const EmptyCommand* c) {
+static void toStream(std::ostream& out, const EmptyCommand* c) throw() {
 }
 
 template <class T>
-static bool tryToStream(std::ostream& out, const Command* c) {
+static bool tryToStream(std::ostream& out, const Command* c) throw() {
   if(typeid(*c) == typeid(T)) {
     toStream(out, dynamic_cast<const T*>(c));
     return true;
@@ -563,6 +583,29 @@ static bool tryToStream(std::ostream& out, const Command* c) {
   return false;
 }
 
+static void toStream(std::ostream& out, const CommandSuccess* s) throw() {
+  if(Command::printsuccess::getPrintSuccess(out)) {
+    out << "OK" << endl;
+  }
+}
+
+static void toStream(std::ostream& out, const CommandUnsupported* s) throw() {
+  out << "UNSUPPORTED" << endl;
+}
+
+static void toStream(std::ostream& out, const CommandFailure* s) throw() {
+  out << s->getMessage() << endl;
+}
+
+template <class T>
+static bool tryToStream(std::ostream& out, const CommandStatus* s) throw() {
+  if(typeid(*s) == typeid(T)) {
+    toStream(out, dynamic_cast<const T*>(s));
+    return true;
+  }
+  return false;
+}
+
 }/* CVC4::printer::cvc namespace */
 }/* CVC4::printer namespace */
 }/* CVC4 namespace */
diff --git a/src/printer/cvc/cvc_printer.h b/src/printer/cvc/cvc_printer.h
index fd478dbe5..ba66145fc 100644
--- a/src/printer/cvc/cvc_printer.h
+++ b/src/printer/cvc/cvc_printer.h
@@ -31,8 +31,9 @@ namespace cvc {
 
 class CvcPrinter : public CVC4::Printer {
 public:
-  void toStream(std::ostream& out, TNode n, int toDepth, bool types) const;
-  void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const;
+  void toStream(std::ostream& out, TNode n, int toDepth, bool types) const throw();
+  void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const throw();
+  void toStream(std::ostream& out, const CommandStatus* s) const throw();
 };/* class CvcPrinter */
 
 }/* CVC4::printer::cvc namespace */
diff --git a/src/printer/printer.cpp b/src/printer/printer.cpp
index 6714d355e..e3b2ed796 100644
--- a/src/printer/printer.cpp
+++ b/src/printer/printer.cpp
@@ -29,25 +29,26 @@ namespace CVC4 {
 
 Printer* Printer::d_printers[language::output::LANG_MAX];
 
-Printer* Printer::makePrinter(OutputLanguage lang) {
+Printer* Printer::makePrinter(OutputLanguage lang) throw() {
   using namespace CVC4::language::output;
 
   switch(lang) {
   case LANG_SMTLIB:
-    return new printer::smt::SmtPrinter;
+    return new printer::smt::SmtPrinter();
 
   case LANG_SMTLIB_V2:
-    return new printer::smt2::Smt2Printer;
+    return new printer::smt2::Smt2Printer();
 
   case LANG_CVC4:
-    return new printer::cvc::CvcPrinter;
+    return new printer::cvc::CvcPrinter();
 
   case LANG_AST:
-    return new printer::ast::AstPrinter;
+    return new printer::ast::AstPrinter();
 
   default:
     Unhandled(lang);
   }
+
 }/* Printer::makePrinter() */
 
 }/* CVC4 namespace */
diff --git a/src/printer/printer.h b/src/printer/printer.h
index 7294ab231..9bcbba3b0 100644
--- a/src/printer/printer.h
+++ b/src/printer/printer.h
@@ -32,11 +32,19 @@ class Printer {
   static Printer* d_printers[language::output::LANG_MAX];
 
   /** Make a Printer for a given OutputLanguage */
-  static Printer* makePrinter(OutputLanguage lang);
+  static Printer* makePrinter(OutputLanguage lang) throw();
+
+  // disallow copy, assignment
+  Printer(const Printer&) CVC4_UNUSED;
+  Printer& operator=(const Printer&) CVC4_UNUSED;
+
+protected:
+  // derived classes can construct, but no one else.
+  Printer() throw() {}
 
 public:
   /** Get the Printer for a given OutputLanguage */
-  static Printer* getPrinter(OutputLanguage lang) {
+  static Printer* getPrinter(OutputLanguage lang) throw() {
     if(d_printers[lang] == NULL) {
       d_printers[lang] = makePrinter(lang);
     }
@@ -45,11 +53,15 @@ public:
 
   /** Write a Node out to a stream with this Printer. */
   virtual void toStream(std::ostream& out, TNode n,
-                        int toDepth, bool types) const = 0;
+                        int toDepth, bool types) const throw() = 0;
 
   /** Write a Command out to a stream with this Printer. */
   virtual void toStream(std::ostream& out, const Command* c,
-                        int toDepth, bool types) const = 0;
+                        int toDepth, bool types) const throw() = 0;
+
+  /** Write a CommandStatus out to a stream with this Printer. */
+  virtual void toStream(std::ostream& out, const CommandStatus* s) const throw() = 0;
+
 };/* class Printer */
 
 }/* CVC4 namespace */
diff --git a/src/printer/smt/smt_printer.cpp b/src/printer/smt/smt_printer.cpp
index ed7f8febf..2ac514988 100644
--- a/src/printer/smt/smt_printer.cpp
+++ b/src/printer/smt/smt_printer.cpp
@@ -34,15 +34,19 @@ namespace printer {
 namespace smt {
 
 void SmtPrinter::toStream(std::ostream& out, TNode n,
-                          int toDepth, bool types) const {
+                          int toDepth, bool types) const throw() {
   n.toStream(out, toDepth, types, language::output::LANG_SMTLIB_V2);
 }/* SmtPrinter::toStream() */
 
 void SmtPrinter::toStream(std::ostream& out, const Command* c,
-                          int toDepth, bool types) const {
+                          int toDepth, bool types) const throw() {
   c->toStream(out, toDepth, types, language::output::LANG_SMTLIB_V2);
 }/* SmtPrinter::toStream() */
 
+void SmtPrinter::toStream(std::ostream& out, const CommandStatus* s) const throw() {
+  s->toStream(out, language::output::LANG_SMTLIB_V2);
+}
+
 }/* CVC4::printer::smt namespace */
 }/* CVC4::printer namespace */
 }/* CVC4 namespace */
diff --git a/src/printer/smt/smt_printer.h b/src/printer/smt/smt_printer.h
index 14d6c09e1..370e0908c 100644
--- a/src/printer/smt/smt_printer.h
+++ b/src/printer/smt/smt_printer.h
@@ -31,8 +31,9 @@ namespace smt {
 
 class SmtPrinter : public CVC4::Printer {
 public:
-  void toStream(std::ostream& out, TNode n, int toDepth, bool types) const;
-  void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const;
+  void toStream(std::ostream& out, TNode n, int toDepth, bool types) const throw();
+  void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const throw();
+  void toStream(std::ostream& out, const CommandStatus* s) const throw();
 };/* class SmtPrinter */
 
 }/* CVC4::printer::smt namespace */
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 6741d5d2d..0f5fcd73b 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -31,12 +31,12 @@ namespace CVC4 {
 namespace printer {
 namespace smt2 {
 
-string smtKindString(Kind k);
+static string smtKindString(Kind k) throw();
 
-void printBvParameterizedOp(std::ostream& out, TNode n);
+static void printBvParameterizedOp(std::ostream& out, TNode n) throw();
 
 void Smt2Printer::toStream(std::ostream& out, TNode n,
-                           int toDepth, bool types) const {
+                           int toDepth, bool types) const throw() {
   // null
   if(n.getKind() == kind::NULL_EXPR) {
     out << "null";
@@ -247,9 +247,9 @@ void Smt2Printer::toStream(std::ostream& out, TNode n,
     }
   }
   out << ')';
-}/* Smt2Printer::toStream() */
+}/* Smt2Printer::toStream(TNode) */
 
-string smtKindString(Kind k) {
+static string smtKindString(Kind k) throw() {
   switch(k) {
     // builtin theory
   case kind::APPLY: break;
@@ -330,7 +330,7 @@ string smtKindString(Kind k) {
   return kind::kindToString(k);
 }
 
-void printBvParameterizedOp(std::ostream& out, TNode n) {
+static void printBvParameterizedOp(std::ostream& out, TNode n) throw() {
   out << "(_ ";
   switch(n.getKind()) {
   case kind::BITVECTOR_EXTRACT: {
@@ -359,16 +359,16 @@ void printBvParameterizedOp(std::ostream& out, TNode n) {
         << n.getOperator().getConst<BitVectorRotateRight>().rotateRightAmount;
     break;
   default:
-    Unhandled(n.getKind());
+    out << n.getKind();
   }
   out << ")";
 }
 
 template <class T>
-static bool tryToStream(std::ostream& out, const Command* c);
+static bool tryToStream(std::ostream& out, const Command* c) throw();
 
 void Smt2Printer::toStream(std::ostream& out, const Command* c,
-                           int toDepth, bool types) const {
+                           int toDepth, bool types) const throw() {
   expr::ExprSetDepth::Scope sdScope(out, toDepth);
   expr::ExprPrintTypes::Scope ptScope(out, types);
 
@@ -400,23 +400,40 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c,
     return;
   }
 
-  Unhandled("don't know how to print this command as SMT-LIBv2: %s", c->toString().c_str());
+  out << "ERROR: don't know how to print a Command of class: "
+      << typeid(*c).name() << endl;
 
-}/* Smt2Printer::toStream() */
+}/* Smt2Printer::toStream(Command*) */
 
-static void toStream(std::ostream& out, const AssertCommand* c) {
+template <class T>
+static bool tryToStream(std::ostream& out, const CommandStatus* s) throw();
+
+void Smt2Printer::toStream(std::ostream& out, const CommandStatus* s) const throw() {
+
+  if(tryToStream<CommandSuccess>(out, s) ||
+     tryToStream<CommandFailure>(out, s) ||
+     tryToStream<CommandUnsupported>(out, s)) {
+    return;
+  }
+
+  out << "ERROR: don't know how to print a CommandStatus of class: "
+      << typeid(*s).name() << endl;
+
+}/* Smt2Printer::toStream(CommandStatus*) */
+
+static void toStream(std::ostream& out, const AssertCommand* c) throw() {
   out << "(assert " << c->getExpr() << ")";
 }
 
-static void toStream(std::ostream& out, const PushCommand* c) {
+static void toStream(std::ostream& out, const PushCommand* c) throw() {
   out << "(push 1)";
 }
 
-static void toStream(std::ostream& out, const PopCommand* c) {
+static void toStream(std::ostream& out, const PopCommand* c) throw() {
   out << "(pop 1)";
 }
 
-static void toStream(std::ostream& out, const CheckSatCommand* c) {
+static void toStream(std::ostream& out, const CheckSatCommand* c) throw() {
   BoolExpr e = c->getExpr();
   if(!e.isNull()) {
     out << PushCommand() << endl
@@ -428,7 +445,7 @@ static void toStream(std::ostream& out, const CheckSatCommand* c) {
   }
 }
 
-static void toStream(std::ostream& out, const QueryCommand* c) {
+static void toStream(std::ostream& out, const QueryCommand* c) throw() {
   BoolExpr e = c->getExpr();
   if(!e.isNull()) {
     out << PushCommand() << endl
@@ -440,11 +457,11 @@ static void toStream(std::ostream& out, const QueryCommand* c) {
   }
 }
 
-static void toStream(std::ostream& out, const QuitCommand* c) {
+static void toStream(std::ostream& out, const QuitCommand* c) throw() {
   out << "(exit)";
 }
 
-static void toStream(std::ostream& out, const CommandSequence* c) {
+static void toStream(std::ostream& out, const CommandSequence* c) throw() {
   for(CommandSequence::const_iterator i = c->begin();
       i != c->end();
       ++i) {
@@ -452,7 +469,7 @@ static void toStream(std::ostream& out, const CommandSequence* c) {
   }
 }
 
-static void toStream(std::ostream& out, const DeclareFunctionCommand* c) {
+static void toStream(std::ostream& out, const DeclareFunctionCommand* c) throw() {
   Type type = c->getType();
   out << "(declare-fun " << c->getSymbol() << " (";
   if(type.isFunction()) {
@@ -469,7 +486,7 @@ static void toStream(std::ostream& out, const DeclareFunctionCommand* c) {
   out << ") " << type << ")";
 }
 
-static void toStream(std::ostream& out, const DefineFunctionCommand* c) {
+static void toStream(std::ostream& out, const DefineFunctionCommand* c) throw() {
   Expr func = c->getFunction();
   const vector<Expr>& formals = c->getFormals();
   Expr formula = c->getFormula();
@@ -487,11 +504,11 @@ static void toStream(std::ostream& out, const DefineFunctionCommand* c) {
   out << ") " << FunctionType(func.getType()).getRangeType() << " " << formula << ")";
 }
 
-static void toStream(std::ostream& out, const DeclareTypeCommand* c) {
+static void toStream(std::ostream& out, const DeclareTypeCommand* c) throw() {
   out << "(declare-sort " << c->getSymbol() << " " << c->getArity() << ")";
 }
 
-static void toStream(std::ostream& out, const DefineTypeCommand* c) {
+static void toStream(std::ostream& out, const DefineTypeCommand* c) throw() {
   const vector<Type>& params = c->getParameters();
   out << "(define-sort " << c->getSymbol() << " (";
   if(params.size() > 0) {
@@ -502,55 +519,57 @@ static void toStream(std::ostream& out, const DefineTypeCommand* c) {
   out << ") " << c->getType() << ")";
 }
 
-static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) {
+static void toStream(std::ostream& out, const DefineNamedFunctionCommand* c) throw() {
   out << "DefineNamedFunction( ";
   toStream(out, static_cast<const DefineFunctionCommand*>(c));
   out << " )";
-  Unhandled("define named function command");
+
+  out << "ERROR: don't know how to output define-named-function command" << endl;
 }
 
-static void toStream(std::ostream& out, const SimplifyCommand* c) {
+static void toStream(std::ostream& out, const SimplifyCommand* c) throw() {
   out << "Simplify( << " << c->getTerm() << " >> )";
-  Unhandled("simplify command");
+
+  out << "ERROR: don't know how to output simplify command" << endl;
 }
 
-static void toStream(std::ostream& out, const GetValueCommand* c) {
+static void toStream(std::ostream& out, const GetValueCommand* c) throw() {
   out << "(get-value " << c->getTerm() << ")";
 }
 
-static void toStream(std::ostream& out, const GetAssignmentCommand* c) {
+static void toStream(std::ostream& out, const GetAssignmentCommand* c) throw() {
   out << "(get-assignment)";
 }
 
-static void toStream(std::ostream& out, const GetAssertionsCommand* c) {
+static void toStream(std::ostream& out, const GetAssertionsCommand* c) throw() {
   out << "(get-assertions)";
 }
 
-static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) {
+static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) throw() {
   out << "(set-info :status " << c->getStatus() << ")";
 }
 
-static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) {
+static void toStream(std::ostream& out, const SetBenchmarkLogicCommand* c) throw() {
   out << "(set-logic " << c->getLogic() << ")";
 }
 
-static void toStream(std::ostream& out, const SetInfoCommand* c) {
+static void toStream(std::ostream& out, const SetInfoCommand* c) throw() {
   out << "(set-info " << c->getFlag() << " " << c->getSExpr() << ")";
 }
 
-static void toStream(std::ostream& out, const GetInfoCommand* c) {
+static void toStream(std::ostream& out, const GetInfoCommand* c) throw() {
   out << "(get-info " << c->getFlag() << ")";
 }
 
-static void toStream(std::ostream& out, const SetOptionCommand* c) {
+static void toStream(std::ostream& out, const SetOptionCommand* c) throw() {
   out << "(set-option " << c->getFlag() << " " << c->getSExpr() << ")";
 }
 
-static void toStream(std::ostream& out, const GetOptionCommand* c) {
+static void toStream(std::ostream& out, const GetOptionCommand* c) throw() {
   out << "(get-option " << c->getFlag() << ")";
 }
 
-static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) {
+static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) throw() {
   const vector<DatatypeType>& datatypes = c->getDatatypes();
   out << "DatatypeDeclarationCommand([";
   for(vector<DatatypeType>::const_iterator i = datatypes.begin(),
@@ -560,18 +579,19 @@ static void toStream(std::ostream& out, const DatatypeDeclarationCommand* c) {
     out << *i << ";" << endl;
   }
   out << "])";
-  Unhandled("datatype declaration command");
+
+  out << "ERROR: don't know how to output datatype declaration command" << endl;
 }
 
-static void toStream(std::ostream& out, const CommentCommand* c) {
+static void toStream(std::ostream& out, const CommentCommand* c) throw() {
   out << "(set-info :notes \"" << c->getComment() << "\")";
 }
 
-static void toStream(std::ostream& out, const EmptyCommand* c) {
+static void toStream(std::ostream& out, const EmptyCommand* c) throw() {
 }
 
 template <class T>
-static bool tryToStream(std::ostream& out, const Command* c) {
+static bool tryToStream(std::ostream& out, const Command* c) throw() {
   if(typeid(*c) == typeid(T)) {
     toStream(out, dynamic_cast<const T*>(c));
     return true;
@@ -579,6 +599,35 @@ static bool tryToStream(std::ostream& out, const Command* c) {
   return false;
 }
 
+static void toStream(std::ostream& out, const CommandSuccess* s) throw() {
+  if(Command::printsuccess::getPrintSuccess(out)) {
+    out << "success" << endl;
+  }
+}
+
+static void toStream(std::ostream& out, const CommandUnsupported* s) throw() {
+  out << "unsupported" << endl;
+}
+
+static void toStream(std::ostream& out, const CommandFailure* s) throw() {
+  string message = s->getMessage();
+  // escape all double-quotes
+  size_t pos;
+  while((pos = message.find('"')) != string::npos) {
+    message = message.replace(pos, 1, "\\\"");
+  }
+  out << "(error \"" << message << "\")" << endl;
+}
+
+template <class T>
+static bool tryToStream(std::ostream& out, const CommandStatus* s) throw() {
+  if(typeid(*s) == typeid(T)) {
+    toStream(out, dynamic_cast<const T*>(s));
+    return true;
+  }
+  return false;
+}
+
 }/* CVC4::printer::smt2 namespace */
 }/* CVC4::printer namespace */
 }/* CVC4 namespace */
diff --git a/src/printer/smt2/smt2_printer.h b/src/printer/smt2/smt2_printer.h
index 2086370ae..a48104e45 100644
--- a/src/printer/smt2/smt2_printer.h
+++ b/src/printer/smt2/smt2_printer.h
@@ -31,8 +31,9 @@ namespace smt2 {
 
 class Smt2Printer : public CVC4::Printer {
 public:
-  void toStream(std::ostream& out, TNode n, int toDepth, bool types) const;
-  void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const;
+  void toStream(std::ostream& out, TNode n, int toDepth, bool types) const throw();
+  void toStream(std::ostream& out, const Command* c, int toDepth, bool types) const throw();
+  void toStream(std::ostream& out, const CommandStatus* s) const throw();
 };/* class Smt2Printer */
 
 }/* CVC4::printer::smt2 namespace */
diff --git a/src/util/cardinality.cpp b/src/util/cardinality.cpp
index b8a79cd9e..8aba4ad41 100644
--- a/src/util/cardinality.cpp
+++ b/src/util/cardinality.cpp
@@ -24,9 +24,9 @@ const Integer Cardinality::s_unknownCard(0);
 const Integer Cardinality::s_intCard(-1);
 const Integer Cardinality::s_realCard(-2);
 
-const Cardinality Cardinality::INTEGERS(Cardinality::Beth(0));
-const Cardinality Cardinality::REALS(Cardinality::Beth(1));
-const Cardinality Cardinality::UNKNOWN((Cardinality::Unknown()));
+const Cardinality Cardinality::INTEGERS(CardinalityBeth(0));
+const Cardinality Cardinality::REALS(CardinalityBeth(1));
+const Cardinality Cardinality::UNKNOWN((CardinalityUnknown()));
 
 Cardinality& Cardinality::operator+=(const Cardinality& c) throw() {
   if(isUnknown()) {
@@ -127,7 +127,7 @@ std::string Cardinality::toString() const throw() {
 }
 
 
-std::ostream& operator<<(std::ostream& out, Cardinality::Beth b) throw() {
+std::ostream& operator<<(std::ostream& out, CardinalityBeth b) throw() {
   out << "beth[" << b.getNumber() << ']';
 
   return out;
@@ -140,7 +140,7 @@ std::ostream& operator<<(std::ostream& out, const Cardinality& c) throw() {
   } else if(c.isFinite()) {
     out << c.getFiniteCardinality();
   } else {
-    out << Cardinality::Beth(c.getBethNumber());
+    out << CardinalityBeth(c.getBethNumber());
   }
 
   return out;
diff --git a/src/util/cardinality.h b/src/util/cardinality.h
index e08f09bb6..057bb0b0c 100644
--- a/src/util/cardinality.h
+++ b/src/util/cardinality.h
@@ -31,6 +31,35 @@
 namespace CVC4 {
 
 /**
+ * Representation for a Beth number, used only to construct
+ * Cardinality objects.
+ */
+class CVC4_PUBLIC CardinalityBeth {
+  Integer d_index;
+
+public:
+  CardinalityBeth(const Integer& beth) : d_index(beth) {
+    CheckArgument(beth >= 0, beth,
+                  "Beth index must be a nonnegative integer, not %s.",
+                  beth.toString().c_str());
+  }
+
+  const Integer& getNumber() const throw() {
+    return d_index;
+  }
+
+};/* class CardinalityBeth */
+
+/**
+ * Representation for an unknown cardinality.
+ */
+class CVC4_PUBLIC CardinalityUnknown {
+public:
+  CardinalityUnknown() throw() {}
+  ~CardinalityUnknown() throw() {}
+};/* class CardinalityUnknown */
+
+/**
  * A simple representation of a cardinality.  We store an
  * arbitrary-precision integer for finite cardinalities, and we
  * distinguish infinite cardinalities represented as Beth numbers.
@@ -65,34 +94,6 @@ public:
   static const Cardinality UNKNOWN;
 
   /**
-   * Representation for a Beth number, used only to construct
-   * Cardinality objects.
-   */
-  class CVC4_PUBLIC Beth {
-    Integer d_index;
-
-  public:
-    Beth(const Integer& beth) : d_index(beth) {
-      CheckArgument(beth >= 0, beth,
-                    "Beth index must be a nonnegative integer, not %s.",
-                    beth.toString().c_str());
-    }
-
-    const Integer& getNumber() const throw() {
-      return d_index;
-    }
-  };/* class Cardinality::Beth */
-
-  /**
-   * Representation for an unknown cardinality.
-   */
-  class CVC4_PUBLIC Unknown {
-  public:
-    Unknown() throw() {}
-    ~Unknown() throw() {}
-  };/* class Cardinality::Unknown */
-
-  /**
    * Construct a finite cardinality equal to the integer argument.
    * The argument must be nonnegative.  If we change this to an
    * "unsigned" argument to enforce the restriction, we mask some
@@ -120,14 +121,14 @@ public:
   /**
    * Construct an infinite cardinality equal to the given Beth number.
    */
-  Cardinality(Beth beth) : d_card(-beth.getNumber() - 1) {
+  Cardinality(CardinalityBeth beth) : d_card(-beth.getNumber() - 1) {
     Assert(!isFinite());
   }
 
   /**
    * Construct an unknown cardinality.
    */
-  Cardinality(Unknown) : d_card(0) {
+  Cardinality(CardinalityUnknown) : d_card(0) {
   }
 
   /** Returns true iff this cardinality is unknown. */
@@ -256,7 +257,7 @@ public:
 
 
 /** Print an element of the InfiniteCardinality enumeration. */
-std::ostream& operator<<(std::ostream& out, Cardinality::Beth b)
+std::ostream& operator<<(std::ostream& out, CardinalityBeth b)
   throw() CVC4_PUBLIC;
 
 
diff --git a/src/util/cardinality.i b/src/util/cardinality.i
index 4e1382f87..c88037cfe 100644
--- a/src/util/cardinality.i
+++ b/src/util/cardinality.i
@@ -2,7 +2,7 @@
 #include "util/cardinality.h"
 %}
 
-%feature("valuewrapper") CVC4::Cardinality::Beth;
+%feature("valuewrapper") CVC4::CardinalityBeth;
 
 %rename(plusAssign) CVC4::Cardinality::operator+=(const Cardinality&);
 %rename(timesAssign) CVC4::Cardinality::operator*=(const Cardinality&);
@@ -18,36 +18,6 @@
 %rename(greaterEqual) CVC4::Cardinality::operator>=(const Cardinality&) const;
 
 %ignore CVC4::operator<<(std::ostream&, const Cardinality&);
-%ignore CVC4::operator<<(std::ostream&, Cardinality::Beth);
-
-namespace CVC4 {
-  class Beth {
-    Integer d_index;
-
-  public:
-    Beth(const Integer& beth) : d_index(beth) {
-      CheckArgument(beth >= 0, beth,
-                    "Beth index must be a nonnegative integer, not %s.",
-                    beth.toString().c_str());
-    }
-
-    const Integer& getNumber() const throw() {
-      return d_index;
-    }
-  };/* class Cardinality::Beth */
-
-  class Unknown {
-  public:
-    Unknown() throw() {}
-    ~Unknown() throw() {}
-  };/* class Cardinality::Unknown */
-}
+%ignore CVC4::operator<<(std::ostream&, CardinalityBeth);
 
 %include "util/cardinality.h"
-
-%{
-namespace CVC4 {
-  typedef CVC4::Cardinality::Beth Beth;
-  typedef CVC4::Cardinality::Unknown Unknown;
-}
-%}
diff --git a/src/util/exception.h b/src/util/exception.h
index 43a0354ca..fe01eba36 100644
--- a/src/util/exception.h
+++ b/src/util/exception.h
@@ -24,25 +24,29 @@
 #include <iostream>
 #include <string>
 #include <sstream>
+#include <exception>
 
 namespace CVC4 {
 
-class CVC4_PUBLIC Exception {
+class CVC4_PUBLIC Exception : public std::exception {
 protected:
   std::string d_msg;
 
 public:
   // Constructors
-  Exception() : d_msg("Unknown exception") {}
-  Exception(const std::string& msg) : d_msg(msg) {}
-  Exception(const char* msg) : d_msg(msg) {}
+  Exception() throw() : d_msg("Unknown exception") {}
+  Exception(const std::string& msg) throw() : d_msg(msg) {}
+  Exception(const char* msg) throw() : d_msg(msg) {}
 
   // Destructor
   virtual ~Exception() throw() {}
 
   // NON-VIRTUAL METHOD for setting and printing the error message
-  void setMessage(const std::string& msg) { d_msg = msg; }
-  std::string getMessage() const { return d_msg; }
+  void setMessage(const std::string& msg) throw() { d_msg = msg; }
+  std::string getMessage() const throw() { return d_msg; }
+
+  // overridden from base class std::exception
+  virtual const char* what() const throw() { return d_msg.c_str(); }
 
   /**
    * Get this exception as a string.  Note that
@@ -56,7 +60,7 @@ public:
    * toString(), there is no stream, so the parameters are default
    * and you'll get exprs and types printed using the AST language.
    */
-  std::string toString() const {
+  std::string toString() const throw() {
     std::stringstream ss;
     toStream(ss);
     return ss.str();
@@ -67,12 +71,12 @@ public:
    * a derived class, it's recommended that this method print the
    * type of exception before the actual message.
    */
-  virtual void toStream(std::ostream& os) const { os << d_msg; }
+  virtual void toStream(std::ostream& os) const throw() { os << d_msg; }
 
 };/* class Exception */
 
-inline std::ostream& operator<<(std::ostream& os, const Exception& e) CVC4_PUBLIC;
-inline std::ostream& operator<<(std::ostream& os, const Exception& e) {
+inline std::ostream& operator<<(std::ostream& os, const Exception& e) throw() CVC4_PUBLIC;
+inline std::ostream& operator<<(std::ostream& os, const Exception& e) throw() {
   e.toStream(os);
   return os;
 }
diff --git a/src/util/exception.i b/src/util/exception.i
index 52ff28922..ab6284633 100644
--- a/src/util/exception.i
+++ b/src/util/exception.i
@@ -2,7 +2,7 @@
 #include "util/exception.h"
 %}
 
-%ignore CVC4::operator<<(std::ostream&, const Exception&);
-%ignore CVC4::Exception::Exception(const char*);
+%ignore CVC4::operator<<(std::ostream&, const Exception&) throw();
+%ignore CVC4::Exception::Exception(const char*) throw();
 
 %include "util/exception.h"
diff --git a/src/util/options.cpp b/src/util/options.cpp
index 94ddf082f..842bd84b2 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -27,6 +27,7 @@
 #include <getopt.h>
 
 #include "expr/expr.h"
+#include "expr/command.h"
 #include "util/configuration.h"
 #include "util/exception.h"
 #include "util/language.h"
@@ -118,6 +119,8 @@ Most commonly-used CVC4 options:\n\
    --no-interactive       force non-interactive mode\n\
    --produce-models | -m  support the get-value command\n\
    --produce-assignments  support the get-assignment command\n\
+   --print-success        print the \"success\" output required of SMT-LIBv2\n\
+   --smtlib2              SMT-LIBv2 conformance mode (implies other options)\n\
    --proof                turn on proof generation\n\
    --incremental | -i     enable incremental solving\n\
    --tlimit=MS            enable time limiting (give milliseconds)\n\
@@ -306,6 +309,8 @@ enum OptionValue {
   INTERACTIVE,
   NO_INTERACTIVE,
   PRODUCE_ASSIGNMENTS,
+  PRINT_SUCCESS,
+  SMTLIB2,
   PROOF,
   NO_TYPE_CHECKING,
   LAZY_TYPE_CHECKING,
@@ -384,6 +389,8 @@ static struct option cmdlineOptions[] = {
   { "no-interactive", no_argument   , NULL, NO_INTERACTIVE },
   { "produce-models", no_argument   , NULL, 'm' },
   { "produce-assignments", no_argument, NULL, PRODUCE_ASSIGNMENTS },
+  { "print-success", no_argument, NULL, PRINT_SUCCESS },
+  { "smtlib2", no_argument, NULL, SMTLIB2 },
   { "proof", no_argument, NULL, PROOF },
   { "no-type-checking", no_argument , NULL, NO_TYPE_CHECKING },
   { "lazy-type-checking", no_argument, NULL, LAZY_TYPE_CHECKING },
@@ -597,14 +604,12 @@ throw(OptionException) {
       break;
 
     case PRINT_EXPR_TYPES:
-      {
-        Debug.getStream() << Expr::printtypes(true);
-        Trace.getStream() << Expr::printtypes(true);
-        Notice.getStream() << Expr::printtypes(true);
-        Chat.getStream() << Expr::printtypes(true);
-        Message.getStream() << Expr::printtypes(true);
-        Warning.getStream() << Expr::printtypes(true);
-      }
+      Debug.getStream() << Expr::printtypes(true);
+      Trace.getStream() << Expr::printtypes(true);
+      Notice.getStream() << Expr::printtypes(true);
+      Chat.getStream() << Expr::printtypes(true);
+      Message.getStream() << Expr::printtypes(true);
+      Warning.getStream() << Expr::printtypes(true);
       break;
 
     case LAZY_DEFINITION_EXPANSION:
@@ -648,7 +653,27 @@ throw(OptionException) {
     case PRODUCE_ASSIGNMENTS:
       produceAssignments = true;
       break;
-      
+
+    case SMTLIB2: // smtlib v2 compliance mode
+      inputLanguage = language::input::LANG_SMTLIB_V2;
+      outputLanguage = language::output::LANG_SMTLIB_V2;
+      strictParsing = true;
+      // make sure entire expressions are printed on all the non-debug, non-trace streams
+      Notice.getStream() << Expr::setdepth(-1);
+      Chat.getStream() << Expr::setdepth(-1);
+      Message.getStream() << Expr::setdepth(-1);
+      Warning.getStream() << Expr::setdepth(-1);
+      /* intentionally fall through */
+
+    case PRINT_SUCCESS:
+      Debug.getStream() << Command::printsuccess(true);
+      Trace.getStream() << Command::printsuccess(true);
+      Notice.getStream() << Command::printsuccess(true);
+      Chat.getStream() << Command::printsuccess(true);
+      Message.getStream() << Command::printsuccess(true);
+      Warning.getStream() << Command::printsuccess(true);
+      break;
+
     case PROOF:
 #ifdef CVC4_PROOF
       proof = true;
diff --git a/src/util/stats.h b/src/util/stats.h
index e955a7d28..719bbaab6 100644
--- a/src/util/stats.h
+++ b/src/util/stats.h
@@ -30,6 +30,7 @@
 #include <set>
 #include <ctime>
 #include <vector>
+#include <stdint.h>
 
 #include "util/Assert.h"
 
@@ -390,7 +391,6 @@ public:
 
 };/* class WrappedStat<T> */
 
-
 /**
  * A backed integer-valued (64-bit signed) statistic.
  * This doesn't functionally differ from its base class BackedStat<int64_t>,
@@ -655,7 +655,7 @@ class CVC4_PUBLIC CodeTimer;
  * arbitrarily, like a stopwatch; the value of the statistic at the
  * end is the accumulated time over all (start,stop) pairs.
  */
-class CVC4_PUBLIC TimerStat : public BackedStat< timespec > {
+class CVC4_PUBLIC TimerStat : public BackedStat<timespec> {
 
   // strange: timespec isn't placed in 'std' namespace ?!
   /** The last start time of this timer */
diff --git a/src/util/stats.i b/src/util/stats.i
index 5d3b81d4d..6f1ef5367 100644
--- a/src/util/stats.i
+++ b/src/util/stats.i
@@ -2,6 +2,14 @@
 #include "util/stats.h"
 %}
 
+namespace CVC4 {
+  template <class T> class CVC4_PUBLIC BackedStat;
+
+  %template(int64_t_BackedStat) BackedStat<int64_t>;
+  %template(double_BackedStat) BackedStat<double>;
+  %template(timespec_BackedStat) BackedStat<timespec>;
+}/* CVC4 namespace */
+
 %ignore CVC4::operator<<(std::ostream&, const timespec&);
 
 %rename(increment) CVC4::IntStat::operator++();
@@ -19,3 +27,4 @@
 %rename(greaterEqual) CVC4::operator>=(const timespec&, const timespec&);
 
 %include "util/stats.h"
+