diff options
Diffstat (limited to 'src/expr/expr_manager_template.h')
| -rw-r--r-- | src/expr/expr_manager_template.h | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index a9cdfc587..bce1c8940 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -83,8 +83,8 @@ private: friend class NodeManager; // undefined, private copy constructor and assignment op (disallow copy) - ExprManager(const ExprManager&) CVC4_UNDEFINED; - ExprManager& operator=(const ExprManager&) CVC4_UNDEFINED; + ExprManager(const ExprManager&) = delete; + ExprManager& operator=(const ExprManager&) = delete; std::vector<DatatypeType> d_keep_dtt; std::vector<Datatype> d_keep_dt; |