minor fix, and better output for type errors

1 files changed, 4 insertions, 2 deletions

diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index cffc95ab2..f343848d8 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -82,8 +82,10 @@ class EqualityTypeRule {
       if ( lhsType != rhsType ) {
         std::stringstream ss;
         ss << Expr::setlanguage(language::toOutputLanguage(Options::current()->inputLanguage));
-        ss << "Types do not match in equation ";
-        ss << "[" << lhsType << "<>" << rhsType << "]";
+        ss << "Types do not match in equation:" << std::endl;
+        ss << "Equation: " << n << std::endl;
+        ss << "Type 1: " << lhsType << std::endl;
+        ss << "Type 2: " << rhsType << std::endl;
 
         throw TypeCheckingExceptionPrivate(n, ss.str());
       }