From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Thu, 7 Feb 2013 20:34:23 +0000 (-0500)
Subject: Fix error in tuple type-checking.
X-Git-Tag: cvc5-1.0.0~7391^2~11
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=110376d88d2e317e24f2376de123521fbecc168d;p=cvc5.git

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 ade9ffc26..9b4f24566 100644
--- 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());