diff options
| author | Morgan Deters <mdeters@gmail.com> | 2011-11-16 00:48:42 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2011-11-16 00:48:42 +0000 |
| commit | d514291efafeef479b819af3f905f339c85086fb (patch) | |
| tree | 88f22153a7fa157e0d02c996aaabed387ab5c56b /src | |
| parent | 78af7dfd469b43c17c3ad582a094068484955037 (diff) | |
* Applying Andy's fix for datatypes bug #286; thanks for the quick work, Andy!
* Also some better configure script wording
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 08b142fe3..6b067c681 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -854,7 +854,8 @@ void TheoryDatatypes::merge(TNode a, TNode b) { } void TheoryDatatypes::addTermToLabels( Node t ) { - if( t.getKind() == VARIABLE || t.getKind() == APPLY_SELECTOR ) { + if( ( t.getKind() == VARIABLE || t.getKind() == APPLY_SELECTOR ) && + t.getType().isDatatype() ) { Node tmp = find( t ); if( tmp == t ) { //add to labels |