diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-12-06 01:26:44 +0100 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-12-06 01:26:53 +0100 |
| commit | 5e2eef449c11b0be6b25942bccf7b0712ebe2d20 (patch) | |
| tree | 11cbfff8392ae0bc498c1d8da96d45862e8911f6 /src | |
| parent | f8c5e78d97eb7ddc3a29392c9ca18c627279fa2b (diff) | |
Fix dt.size care graph.
Diffstat (limited to 'src')
| -rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index a70343702..5436ab632 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -1096,7 +1096,7 @@ void TheoryDatatypes::computeCareGraph(){ for( unsigned j=i+1; j<functionTerms; j++ ){ TNode f2 = r==0 ? d_consTerms[j] : d_selTerms[j]; Trace("dt-cg-debug") << "dt-cg: " << f1 << " and " << f2 << " " << (f1.getOperator()==f2.getOperator()) << " " << areEqual( f1, f2 ) << std::endl; - if( f1.getOperator()==f2.getOperator() && !areEqual( f1, f2 ) ){ + if( f1.getOperator()==f2.getOperator() && ( f1.getKind()!=DT_SIZE || f1[0].getType()==f2[0].getType() ) && !areEqual( f1, f2 ) ){ Trace("dt-cg") << "Check " << f1 << " and " << f2 << std::endl; bool somePairIsDisequal = false; currentPairs.clear(); |