parser and core support for SMT-LIBv2 commands get-info, set-option, get-option, get-assertions, get-value, define-sort, define-fun, and declare-sort with arity > 0; SmtEngine doesn't yet support most of these, but will shortly...

1 files changed, 4 insertions, 0 deletions

diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 54e20667f..83d5dc47f 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -42,6 +42,10 @@ const int ExprPrintTypes::s_iosIndex = std::ios_base::xalloc();
 
 }/* CVC4::expr namespace */
 
+std::ostream& operator<<(std::ostream& out, const TypeCheckingException& e) {
+  return out << e.getMessage() << ": " << e.getExpression();
+}
+
 std::ostream& operator<<(std::ostream& out, const Expr& e) {
   e.toStream(out);
   return out;