diff options
Diffstat (limited to 'src/expr/expr_manager_template.h')
| -rw-r--r-- | src/expr/expr_manager_template.h | 8 |
1 files changed, 7 insertions, 1 deletions
diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 92d039bd3..7946a734e 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -74,12 +74,18 @@ private: /** ExprManagerScope reaches in to get the NodeManager */ friend class ExprManagerScope; + // undefined, private copy constructor (disallow copy) + ExprManager(const ExprManager&); + public: /** * Creates an expression manager. + * @param earlyTypeChecking whether to do type checking early (at Expr + * creation time); only used in debug builds---for other builds, type + * checking is never done early. */ - ExprManager(); + explicit ExprManager(bool earlyTypeChecking = true); /** * Destroys the expression manager. No will be deallocated at this point, so |