Add options for symmetry breaking in uf+ss totality axiom approach, option for using clique lemmas instead of splitting on demand, option for simplifying models in fmf-fmc, minor fixes for rewrite engine

1 files changed, 7 insertions, 0 deletions

diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index 99e28714f..f2cb22b85 100644
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -295,11 +295,18 @@ void RepSetIterator::increment2( int counter ){
     d_index.clear();
   }else{
     d_index[counter]++;
+    bool emptyDomain = false;
     for( int i=(int)d_index.size()-1; i>counter; i-- ){
       if (!resetIndex(i)){
         break;
+      }else if( domainSize(i)<=0 ){
+        emptyDomain = true;
       }
     }
+    if( emptyDomain ){
+      Trace("rsi-debug") << "This is an empty domain, increment again." << std::endl;
+      increment();
+    }
   }
 }