From 8d3aca31964a314b4c84679d6ec0a223bcc30dda Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 27 May 2014 00:06:42 -0400 Subject: [PATCH] Improved type-checking for tuple and record selects. --- src/theory/datatypes/theory_datatypes_type_rules.h | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h index d08b511dd..09d43b3bc 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.h +++ b/src/theory/datatypes/theory_datatypes_type_rules.h @@ -282,6 +282,9 @@ struct TupleTypeRule { struct TupleSelectTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { Assert(n.getKind() == kind::TUPLE_SELECT); + if(n.getOperator().getKind() != kind::TUPLE_SELECT_OP) { + throw TypeCheckingExceptionPrivate(n, "Tuple-select expression requires TupleSelect operator"); + } const TupleSelect& ts = n.getOperator().getConst(); TypeNode tupleType = n[0].getType(check); if(!tupleType.isTuple()) { @@ -422,6 +425,9 @@ struct RecordSelectTypeRule { inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { Assert(n.getKind() == kind::RECORD_SELECT); NodeManagerScope nms(nodeManager); + if(n.getOperator().getKind() != kind::RECORD_SELECT_OP) { + throw TypeCheckingExceptionPrivate(n, "Tuple-select expression requires TupleSelect operator"); + } const RecordSelect& rs = n.getOperator().getConst(); TypeNode recordType = n[0].getType(check); if(!recordType.isRecord()) { -- 2.30.2