diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/expr/datatype.cpp | 5 | ||||
-rw-r--r-- | src/expr/datatype.h | 2 |
2 files changed, 3 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 */ |