diff options
| author | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-07-27 20:55:10 +0000 |
|---|---|---|
| committer | Christopher L. Conway <christopherleeconway@gmail.com> | 2010-07-27 20:55:10 +0000 |
| commit | 01bd928fa45459114ae4f5effcc8fbcf91bef7e8 (patch) | |
| tree | d29748d3b830c807cc6577e60742045490735df1 /src/theory/theory_engine.cpp | |
| parent | 2564d8730f768a8305325d4b6cc08211d8a3281d (diff) | |
Moving EQ->IFF handling from TheoryEngine to parser/type checker
Diffstat (limited to 'src/theory/theory_engine.cpp')
| -rw-r--r-- | src/theory/theory_engine.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp index bf501ec37..8db81902d 100644 --- a/src/theory/theory_engine.cpp +++ b/src/theory/theory_engine.cpp @@ -165,7 +165,7 @@ Theory* TheoryEngine::theoryOf(TNode n) { return theoryOf(n.getType()); } else if(k == kind::EQUAL) { // equality is special: use LHS - return theoryOf(n[0].getType()); + return theoryOf(n[0]); } else { // use our Kind-to-Theory mapping return d_theoryOfTable[k]; |