summaryrefslogtreecommitdiff
path: root/src/expr/expr_template.h
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2010-10-07 22:54:43 +0000
committerMorgan Deters <mdeters@gmail.com>2010-10-07 22:54:43 +0000
commitb63e4a11733051728397f7d4ecb3b205fbd81dab (patch)
tree04dad54f11fd1f7a80c3a8b30bb344ad9786283f /src/expr/expr_template.h
parent557e6c09dcc9068e848796772bc775542f4fc599 (diff)
type checking for define-fun in production builds; related to (and might resolve) bug 212
Diffstat (limited to 'src/expr/expr_template.h')
-rw-r--r--src/expr/expr_template.h2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/expr/expr_template.h b/src/expr/expr_template.h
index bb227f92f..29164ffa5 100644
--- a/src/expr/expr_template.h
+++ b/src/expr/expr_template.h
@@ -60,6 +60,8 @@ namespace expr {
*/
class CVC4_PUBLIC TypeCheckingException : public Exception {
+ friend class SmtEngine;
+
private:
/** The expression responsible for the error */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback