From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Tue, 9 Dec 2014 23:48:55 +0000 (-0500)
Subject: Better error description (related to bug 605).
X-Git-Tag: cvc5-1.0.0~6466
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7032ab2fd448f8533c7aabc399d11473e22bfdc1;p=cvc5.git

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 84be5238d..3044a2bf1 100644
--- 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()) {