minor fix, and better output for type errors

diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp
index 7376b00802c62df42cb03b4e139e0030fdb054f6..b9047307dc16899a6a8b7e5c18e060a01a58759e 100644 (file)
--- a/src/expr/type_node.cpp
+++ b/src/expr/type_node.cpp
@@ -209,8 +209,9 @@ bool TypeNode::isInstantiatedDatatype() const {
   }
   const Datatype& dt = (*this)[0].getConst<Datatype>();
   unsigned n = dt.getNumParameters();
+  Assert(n < getNumChildren());
   for(unsigned i = 0; i < n; ++i) {
-    if(TypeNode::fromType(dt.getParameter(i)) == (*this)[n + 1]) {
+    if(TypeNode::fromType(dt.getParameter(i)) == (*this)[i + 1]) {
       return false;
     }
   }

diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index cffc95ab2e8c16375e5eb37bc31d0248beb5bc7b..f343848d8373f9a4d079930f84d5c8daa56fcc2c 100644 (file)
--- 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());
       }