summaryrefslogtreecommitdiff
path: root/src/theory/uf
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2012-02-20 17:59:33 +0000
committerMorgan Deters <mdeters@gmail.com>2012-02-20 17:59:33 +0000
commit3d2b33d66998261f9369cccc098140f64bc8b417 (patch)
tree9176ad2684415f8fb95f75a5655e8b17dcdf9793 /src/theory/uf
parent92155f5e40ed2cf452dc5e2f618e7be6542293e8 (diff)
portfolio merge
Diffstat (limited to 'src/theory/uf')
-rw-r--r--src/theory/uf/theory_uf_type_rules.h2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/uf/theory_uf_type_rules.h b/src/theory/uf/theory_uf_type_rules.h
index 927a31e01..9b622bc15 100644
--- a/src/theory/uf/theory_uf_type_rules.h
+++ b/src/theory/uf/theory_uf_type_rules.h
@@ -28,7 +28,7 @@ namespace uf {
class UfTypeRule {
public:
inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check)
- throw (TypeCheckingExceptionPrivate) {
+ throw (TypeCheckingExceptionPrivate, AssertionException) {
TNode f = n.getOperator();
TypeNode fType = f.getType(check);
if( !fType.isFunction() ) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback