From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Sat, 6 Dec 2014 00:26:44 +0000 (+0100)
Subject: Fix dt.size care graph.
X-Git-Tag: cvc5-1.0.0~6471
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5e2eef449c11b0be6b25942bccf7b0712ebe2d20;p=cvc5.git

Fix dt.size care graph.
---

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();