diff options
Diffstat (limited to 'src/expr/node_builder.h')
| -rw-r--r-- | src/expr/node_builder.h | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 45ac02f10..b0fdd0657 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -687,10 +687,11 @@ private: expr::NodeValue* constructNV() const; #ifdef CVC4_DEBUG - void maybeCheckType(const TNode n) const - throw(TypeCheckingExceptionPrivate, AssertionException); + // Throws a TypeCheckingExceptionPrivate on a failure. + void maybeCheckType(const TNode n) const; #else /* CVC4_DEBUG */ - inline void maybeCheckType(const TNode n) const throw() { } + // Do nothing if not in debug mode. + inline void maybeCheckType(const TNode n) const {} #endif /* CVC4_DEBUG */ public: @@ -1320,7 +1321,7 @@ void NodeBuilder<nchild_thresh>::internalCopy(const NodeBuilder<N>& nb) { #ifdef CVC4_DEBUG template <unsigned nchild_thresh> inline void NodeBuilder<nchild_thresh>::maybeCheckType(const TNode n) const - throw(TypeCheckingExceptionPrivate, AssertionException) { +{ /* force an immediate type check, if early type checking is enabled and the current node isn't a variable or constant */ if( d_nm->getOptions()[options::earlyTypeChecking] ) { |