diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-12-09 18:48:55 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-12-09 18:48:55 -0500 |
| commit | 7032ab2fd448f8533c7aabc399d11473e22bfdc1 (patch) | |
| tree | 77143ae2d4f15c20df8e7dc0e2c11e585f7c7453 | |
| parent | 5361724725d9221fc798a9f3d5fd78de0dd91967 (diff) | |
Better error description (related to bug 605).
| -rw-r--r-- | src/theory/datatypes/theory_datatypes_type_rules.h | 4 |
1 files changed, 3 insertions, 1 deletions
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()) { |