From 7032ab2fd448f8533c7aabc399d11473e22bfdc1 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 9 Dec 2014 18:48:55 -0500 Subject: [PATCH] Better error description (related to bug 605). --- src/theory/datatypes/theory_datatypes_type_rules.h | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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()) { -- 2.30.2