3 files changed, 5 insertions, 4 deletions
diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp
index 4d2467f84..5f43fb24f 100644
--- a/src/expr/datatype.cpp
+++ b/src/expr/datatype.cpp
@@ -42,7 +42,6 @@ Datatype::~Datatype()
   ExprManagerScope ems(*d_em);
   d_internal.reset();
   d_constructors.clear();
-  delete d_record;
 }
 
 Datatype::Datatype(ExprManager* em, std::string name, bool isCo)
@@ -207,7 +206,7 @@ void Datatype::resolve(const std::map<std::string, DatatypeType>& resolutions,
     for( unsigned i=0; i<(*this)[0].getNumArgs(); i++ ){
       fields.push_back( std::pair<std::string, Type>( (*this)[0][i].getName(), (*this)[0][i].getRangeType() ) );
     }
-    d_record = new Record(fields);
+    d_record.reset(new Record(fields));
   }
 }
 
@@ -911,7 +910,7 @@ bool Datatype::isTuple() const
 
 bool Datatype::isRecord() const { return d_isRecord; }
 
-Record* Datatype::getRecord() const { return d_record; }
+Record* Datatype::getRecord() const { return d_record.get(); }
 bool Datatype::operator!=(const Datatype& other) const
 {
   return !(*this == other);
diff --git a/src/expr/datatype.h b/src/expr/datatype.h
index 1ae59f00c..f9edb998f 100644
--- a/src/expr/datatype.h
+++ b/src/expr/datatype.h
@@ -899,7 +899,7 @@ class CVC4_PUBLIC Datatype {
   /** self type */
   Type d_self;
   /** the data of the record for this datatype (if applicable) */
-  Record* d_record;
+  std::shared_ptr<Record> d_record;
   /** whether the datatype is a record */
   bool d_isRecord;
   /** the constructors of this datatype */
diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h
index e53b989f0..bf992d2d5 100644
--- a/test/unit/api/solver_black.h
+++ b/test/unit/api/solver_black.h
@@ -247,6 +247,8 @@ void SolverBlack::testMkRecordSort()
   std::vector<std::pair<std::string, Sort>> empty;
   TS_ASSERT_THROWS_NOTHING(d_solver->mkRecordSort(fields));
   TS_ASSERT_THROWS_NOTHING(d_solver->mkRecordSort(empty));
+  Sort recSort = d_solver->mkRecordSort(fields);
+  TS_ASSERT_THROWS_NOTHING(recSort.getDatatype());
 }
 
 void SolverBlack::testMkSetSort()