diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/theory.cpp | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 859356341..5d2128c54 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -214,9 +214,12 @@ TheoryId Theory::theoryOf(options::TheoryOfMode mode, TNode node) TNode r = node[1]; TypeNode ltype = l.getType(); TypeNode rtype = r.getType(); - if (ltype != rtype) + // If the types are different, we must assign based on type due + // to handling subtypes (limited to arithmetic). Also, if we are + // a Boolean equality, we must assign THEORY_BOOL. + if (ltype != rtype || ltype.isBoolean()) { - tid = Theory::theoryOf(l.getType()); + tid = Theory::theoryOf(ltype); } else { |