From c6a8319b05cf1b156691132b3bec1f56ca6588e0 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Wed, 1 Jun 2011 01:13:21 +0000 Subject: [PATCH] minor fix, and better output for type errors --- src/expr/type_node.cpp | 3 ++- src/theory/builtin/theory_builtin_type_rules.h | 6 ++++-- 2 files changed, 6 insertions(+), 3 deletions(-) diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index 7376b0080..b9047307d 100644 --- 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(); 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 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()); } -- 2.30.2