diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2017-09-25 16:42:02 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-09-25 16:42:02 -0500 |
| commit | aab07a32ae755d343bec226a746367e35b86098a (patch) | |
| tree | 219fb580c9942ec7cb7182dbef182c3ecb7e06e1 /src/theory | |
| parent | e849f5c87c6a92cc06cfae611ce0cab0851e6905 (diff) | |
Fix bug related to sort inference + subtypes. (#1125)
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/sort_inference.cpp | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/theory/sort_inference.cpp b/src/theory/sort_inference.cpp index 73a50bc7a..b469ac9d0 100644 --- a/src/theory/sort_inference.cpp +++ b/src/theory/sort_inference.cpp @@ -540,7 +540,8 @@ TypeNode SortInference::getTypeForId( int t ){ } Node SortInference::getNewSymbol( Node old, TypeNode tn ){ - if( tn.isNull() || tn==old.getType() ){ + // if no sort was inferred for this node, return original + if( tn.isNull() || tn.isComparableTo( old.getType() ) ){ return old; }else if( old.isConst() ){ //must make constant of type tn |