Better error description (related to bug 605).

diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index 84be5238dd181b47ccde46e4a144d8427dbda6c2..3044a2bf1b468a9a3651fdbb8d0dc50659075c9c 100644 (file)
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -453,7 +453,9 @@ struct RecordTypeRule {
           throw TypeCheckingExceptionPrivate(n, "record description has different length than record literal");
         }
         if(!(*child_it).getType(check).isComparableTo(TypeNode::fromType((*i).second))) {
-          throw TypeCheckingExceptionPrivate(n, "record description types differ from record literal types");
+          std::stringstream ss;
+          ss << "record description types differ from record literal types\nDescription type: " << (*child_it).getType() << "\nLiteral type: " << (*i).second;
+          throw TypeCheckingExceptionPrivate(n, ss.str());
         }
       }
       if(i != rec.end()) {