diff options
| author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-05-05 19:06:07 +0000 |
|---|---|---|
| committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-05-05 19:06:07 +0000 |
| commit | 9a76c8034cadc11b1528be8727f25693f823fb21 (patch) | |
| tree | e6c81952013d82986e4d597a23c018b2abc912da /src/theory/uf | |
| parent | fec2b5751108088ff651ce6eed09bf3aa65f281e (diff) | |
bug fixes for types, old unit tests for types work now
Diffstat (limited to 'src/theory/uf')
| -rw-r--r-- | src/theory/uf/theory_uf_type_rules.h | 2 |
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 8c05591d6..4028c3022 100644 --- a/src/theory/uf/theory_uf_type_rules.h +++ b/src/theory/uf/theory_uf_type_rules.h @@ -22,7 +22,7 @@ namespace uf { class UfTypeRule { public: inline static TypeNode computeType(NodeManager* nodeManager, TNode n) - throw (TypeCheckingException) { + throw (TypeCheckingExceptionPrivate) { TNode f = n.getOperator(); TypeNode fType = f.getType(); if (n.getNumChildren() != fType.getNumChildren() - 1) { |