Fix error in tuple type-checking.

diff --git a/src/theory/datatypes/theory_datatypes_type_rules.h b/src/theory/datatypes/theory_datatypes_type_rules.h
index ade9ffc26cfda91a85b43026bc0457f9ab4b3627..9b4f24566d09fbf45fa4ea6faff507cc57c432f0 100644 (file)
--- a/src/theory/datatypes/theory_datatypes_type_rules.h
+++ b/src/theory/datatypes/theory_datatypes_type_rules.h
@@ -285,7 +285,7 @@ struct TupleSelectTypeRule {
     const TupleSelect& ts = n.getOperator().getConst<TupleSelect>();
     TypeNode tupleType = n[0].getType(check);
     if(!tupleType.isTuple()) {
-      if(!tupleType.hasAttribute(expr::DatatypeRecordAttr())) {
+      if(!tupleType.hasAttribute(expr::DatatypeTupleAttr())) {
         throw TypeCheckingExceptionPrivate(n, "Tuple-select expression formed over non-tuple");
       }
       tupleType = tupleType.getAttribute(expr::DatatypeTupleAttr());
@@ -309,7 +309,7 @@ struct TupleUpdateTypeRule {
     TypeNode newValue = n[1].getType(check);
     if(check) {
       if(!tupleType.isTuple()) {
-        if(!tupleType.hasAttribute(expr::DatatypeRecordAttr())) {
+        if(!tupleType.hasAttribute(expr::DatatypeTupleAttr())) {
           throw TypeCheckingExceptionPrivate(n, "Tuple-update expression formed over non-tuple");
         }
         tupleType = tupleType.getAttribute(expr::DatatypeTupleAttr());