Avoid instantiating with array constants.

diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 020a2e552fbe2432eef5feccb838304efc185b7f..a2d68f7c90c080c56c1710882ded4e039304d68d 100644 (file)
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -1100,6 +1100,8 @@ Node EqualityQueryQuantifiersEngine::getInternalRepresentative( Node a, Node f,
             r = getRepresentative( r );
           }else{
             if( r.getType().isSort() ){
+              //TODO : this can happen in rare cases
+              // say x:(Array Int U), select( x, 0 ), x assigned (const @u1).
               Trace("internal-rep-warn") << "No representative for UF constant." << std::endl;
             }
           }

diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index 4ab8df72f3792b120c3ab17ceb682b0ac8f97ec0..70b7d31f4c6d612b0064a5d3651a48f0211fda3f 100644 (file)
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -48,10 +48,13 @@ int RepSet::getNumRepresentatives( TypeNode tn ) const{
 }
 
 void RepSet::add( TypeNode tn, Node n ){
-  Trace("rsi-debug") << "Add rep #" << d_type_reps[tn].size() << " for " << tn << " : " << n << std::endl;
-  Assert( n.getType().isSubtypeOf( tn ) );
-  d_tmap[ n ] = (int)d_type_reps[tn].size();
-  d_type_reps[tn].push_back( n );
+  //for now, do not add array constants FIXME
+  if( !tn.isArray() || !n.isConst() ){
+    Trace("rsi-debug") << "Add rep #" << d_type_reps[tn].size() << " for " << tn << " : " << n << std::endl;
+    Assert( n.getType().isSubtypeOf( tn ) );
+    d_tmap[ n ] = (int)d_type_reps[tn].size();
+    d_type_reps[tn].push_back( n );
+  }
 }
 
 int RepSet::getIndexFor( Node n ) const {
@@ -179,8 +182,8 @@ bool RepSetIterator::initialize(){
           d_incomplete = true;
         }
       }
-    //enumerate if the sort is reasonably small, the upper bound of 1000 is chosen arbitrarily for now
-    }else if( tn.getCardinality().isFinite() && !tn.getCardinality().isLargeFinite() &&
+    //enumerate if the sort is reasonably small, not an Array, the upper bound of 1000 is chosen arbitrarily for now
+    }else if( !tn.isArray() && tn.getCardinality().isFinite() && !tn.getCardinality().isLargeFinite() &&
               tn.getCardinality().getFiniteCardinality().toUnsignedInt()<=1000 ){
       d_rep_set->complete( tn );
     }else{