Change internal representative selection for finite domains that do not involve uninterpreted sorts, including bounded integer quantification.

1 files changed, 2 insertions, 0 deletions

diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index 98cd175fd..5e4b6828e 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -744,12 +744,14 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No
   for( unsigned i=0; i<c.getNumChildren(); i++ ){
     if( c[i].getType().isInteger() ){
       if( fm->isInterval(c[i]) ){
+        Trace("fmc-exh-debug") << "...set " << i << " based on interval." << std::endl;
         for( unsigned b=0; b<2; b++ ){
           if( !fm->isStar(c[i][b]) ){
             riter.d_bounds[b][i] = c[i][b];
           }
         }
       }else if( !fm->isStar(c[i]) ){
+        Trace("fmc-exh-debug") << "...set " << i << " based on point." << std::endl;
         riter.d_bounds[0][i] = c[i];
         riter.d_bounds[1][i] = QuantArith::offset( c[i], 1 );
       }