diff options
Diffstat (limited to 'src/expr')
| -rw-r--r-- | src/expr/datatype.cpp | 4 | ||||
| -rw-r--r-- | src/expr/datatype.h | 2 |
2 files changed, 3 insertions, 3 deletions
diff --git a/src/expr/datatype.cpp b/src/expr/datatype.cpp index 513cb2170..8b6384dcc 100644 --- a/src/expr/datatype.cpp +++ b/src/expr/datatype.cpp @@ -879,11 +879,11 @@ bool DatatypeConstructor::isSygusIdFunc() const { && d_sygus_op[0][0] == d_sygus_op[1]); } -SygusPrintCallback* DatatypeConstructor::getSygusPrintCallback() const +std::shared_ptr<SygusPrintCallback> DatatypeConstructor::getSygusPrintCallback() const { PrettyCheckArgument( isResolved(), this, "this datatype constructor is not yet resolved"); - return d_sygus_pc.get(); + return d_sygus_pc; } Cardinality DatatypeConstructor::getCardinality( Type t ) const throw(IllegalArgumentException) { diff --git a/src/expr/datatype.h b/src/expr/datatype.h index 85ecfb946..b899b0099 100644 --- a/src/expr/datatype.h +++ b/src/expr/datatype.h @@ -300,7 +300,7 @@ class CVC4_PUBLIC DatatypeConstructor { * to handle defined or let expressions that * appear in user-provided grammars. */ - SygusPrintCallback* getSygusPrintCallback() const; + std::shared_ptr<SygusPrintCallback> getSygusPrintCallback() const; /** * Get the tester name for this Datatype constructor. |