Updates not related to creation for eliminating Expr-level datatype (#4838)

[cvc5.git] / src / theory / datatypes / theory_datatypes.cpp

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 9b8badc5eb880f963225a1d8ca0a93d278747597..17a43bc04f18a849f73e4083a96f1c5b4acc54cb 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -18,7 +18,6 @@
 #include <map>
 
 #include "base/check.h"
-#include "expr/datatype.h"
 #include "expr/dtype.h"
 #include "expr/kind.h"
 #include "options/datatypes_options.h"
@@ -654,10 +653,11 @@ TrustNode TheoryDatatypes::expandDefinition(Node n)
       }
       else
       {
-        Assert(tn.toType().isRecord());
-        const Record& record = DatatypeType(tn.toType()).getRecord();
-        size = record.getNumFields();
-        updateIndex = record.getIndex(
+        Assert(tn.isRecord());
+        const DTypeConstructor& recCons = dt[0];
+        size = recCons.getNumArgs();
+        // get the index for the name
+        updateIndex = recCons.getSelectorIndexForName(
             n.getOperator().getConst<RecordUpdate>().getField());
       }
       Debug("tuprec") << "expr is " << n << std::endl;