Answer unknown when uf-ss=no-minimal is combined with cardinality constraints from user input, add regressions. (#1060)

6 files changed, 254 insertions, 201 deletions

diff --git a/src/theory/theory_model.cpp b/src/theory/theory_model.cpp
index 75bc40af7..840bbd027 100644
--- a/src/theory/theory_model.cpp
+++ b/src/theory/theory_model.cpp
@@ -137,8 +137,7 @@ Node TheoryModel::getModelValue(TNode n, bool hasBoundVars, bool useDontCares) c
     return (*it).second;
   }
   Node ret = n;
-  if(n.getKind() == kind::EXISTS || n.getKind() == kind::FORALL || n.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT ||
-     ( n.getKind() == kind::CARDINALITY_CONSTRAINT && options::ufssMode()!=theory::uf::UF_SS_FULL ) ) {
+  if(n.getKind() == kind::EXISTS || n.getKind() == kind::FORALL || n.getKind() == kind::COMBINED_CARDINALITY_CONSTRAINT ) {
     // We should have terms, thanks to TheoryQuantifiers::collectModelInfo().
     // However, if the Decision Engine stops us early, there might be a
     // quantifier that isn't assigned.  In conjunction with miniscoping, this
diff --git a/src/theory/uf/theory_uf_strong_solver.cpp b/src/theory/uf/theory_uf_strong_solver.cpp
index 77459715f..e7efba325 100644
--- a/src/theory/uf/theory_uf_strong_solver.cpp
+++ b/src/theory/uf/theory_uf_strong_solver.cpp
@@ -697,6 +697,7 @@ bool SortModel::areDisequal( Node a, Node b ) {
 
 /** check */
 void SortModel::check( Theory::Effort level, OutputChannel* out ){
+  Assert( options::ufssMode()==UF_SS_FULL );
   if( level>=Theory::EFFORT_STANDARD && d_hasCard && !d_conflict ){
     Debug("uf-ss") << "StrongSolverTheoryUF: Check " << level << " " << d_type << std::endl;
     if( level==Theory::EFFORT_FULL ){
@@ -723,11 +724,9 @@ void SortModel::check( Theory::Effort level, OutputChannel* out ){
           if( d_regions[i]->valid() ){
             std::vector< Node > clique;
             if( d_regions[i]->check( level, d_cardinality, clique ) ){
-              if( options::ufssMode()==UF_SS_FULL ){
-                //add clique lemma
-                addCliqueLemma( clique, out );
-                return;
-              }
+              //add clique lemma
+              addCliqueLemma( clique, out );
+              return;
             }else{
               Trace("uf-ss-debug") << "No clique in Region #" << i << std::endl;
             }
@@ -797,10 +796,8 @@ void SortModel::check( Theory::Effort level, OutputChannel* out ){
                   int fcr = forceCombineRegion( i, false );
                   Debug("fmf-full-check") << "Combined regions " << i << " " << fcr << std::endl;
                   Trace("uf-ss-debug") << "Combined regions " << i << " " << fcr << std::endl;
-                  if( options::ufssMode()==UF_SS_FULL || fcr!=-1 ){
-                    recheck = true;
-                    break;
-                  }
+                  recheck = true;
+                  break;
                 }
               }
             }
@@ -1045,10 +1042,8 @@ void SortModel::checkRegion( int ri, bool checkCombine ){
     //now check if region is in conflict
     std::vector< Node > clique;
     if( d_regions[ri]->check( Theory::EFFORT_STANDARD, d_cardinality, clique ) ){
-      if( options::ufssMode()==UF_SS_FULL ){
-        //explain clique
-        addCliqueLemma( clique, &d_thss->getOutputChannel() );
-      }
+      //explain clique
+      addCliqueLemma( clique, &d_thss->getOutputChannel() );
     }
   }
 }
@@ -1228,24 +1223,6 @@ int SortModel::addSplit( Region* r, OutputChannel* out ){
       }
     }
     Assert( s!=Node::null() );
-  }else{
-    if( options::ufssMode()!=UF_SS_FULL ){
-      // Since candidate clique is not reported, we may need to find
-      // splits manually.
-      for ( Region::iterator it = r->begin(); it != r->end(); ++it ){
-        if ( it->second->valid() ){
-          for ( Region::iterator it2 = r->begin(); it2 != r->end(); ++it2 ){
-            if ( it->second!=it2->second && it2->second->valid() ){
-              if( !r->isDisequal( it->first, it2->first, 1 ) ){
-                Node it_node = it->first;
-                Node it2_node = it2->first;
-                s = it_node.eqNode(it2_node);
-              }
-            }
-          }
-        }
-      }
-    }
   }
   if (!s.isNull() ){
     //add lemma to output channel
@@ -1811,112 +1788,120 @@ void StrongSolverTheoryUF::assertNode( Node n, bool isDecision ){
 #endif
   bool polarity = n.getKind() != kind::NOT;
   TNode lit = polarity ? n : n[0];
-  if( lit.getKind()==CARDINALITY_CONSTRAINT ){
-    TypeNode tn = lit[0].getType();
-    Assert( tn.isSort() );
-    Assert( d_rep_model[tn] );
-    int nCard = lit[1].getConst<Rational>().getNumerator().getSignedInt();
-    Node ct = d_rep_model[tn]->getCardinalityTerm();
-    Trace("uf-ss-debug") << "...check cardinality terms : " << lit[0] << " " << ct << std::endl;
-    if( lit[0]==ct ){
-      if( options::ufssFairnessMonotone() ){
-        Trace("uf-ss-com-card-debug") << "...set master/slave" << std::endl;
-        if( tn!=d_tn_mono_master ){
-          std::map< TypeNode, bool >::iterator it = d_tn_mono_slave.find( tn );
-          if( it==d_tn_mono_slave.end() ){
-            bool isMonotonic;
-            if( d_th->getQuantifiersEngine() ){
-              isMonotonic = getSortInference()->isMonotonic( tn );
-            }else{
-              //if ground, everything is monotonic
-              isMonotonic = true;
-            }
-            if( isMonotonic ){
-              if( d_tn_mono_master.isNull() ){
-                Trace("uf-ss-com-card-debug") << "uf-ss-fair-monotone: Set master : " << tn << std::endl;
-                d_tn_mono_master = tn;
+  if( options::ufssMode()==UF_SS_FULL ){
+    if( lit.getKind()==CARDINALITY_CONSTRAINT ){
+      TypeNode tn = lit[0].getType();
+      Assert( tn.isSort() );
+      Assert( d_rep_model[tn] );
+      int nCard = lit[1].getConst<Rational>().getNumerator().getSignedInt();
+      Node ct = d_rep_model[tn]->getCardinalityTerm();
+      Trace("uf-ss-debug") << "...check cardinality terms : " << lit[0] << " " << ct << std::endl;
+      if( lit[0]==ct ){
+        if( options::ufssFairnessMonotone() ){
+          Trace("uf-ss-com-card-debug") << "...set master/slave" << std::endl;
+          if( tn!=d_tn_mono_master ){
+            std::map< TypeNode, bool >::iterator it = d_tn_mono_slave.find( tn );
+            if( it==d_tn_mono_slave.end() ){
+              bool isMonotonic;
+              if( d_th->getQuantifiersEngine() ){
+                isMonotonic = getSortInference()->isMonotonic( tn );
               }else{
-                Trace("uf-ss-com-card-debug") << "uf-ss-fair-monotone: Set slave : " << tn << std::endl;
-                d_tn_mono_slave[tn] = true;
+                //if ground, everything is monotonic
+                isMonotonic = true;
+              }
+              if( isMonotonic ){
+                if( d_tn_mono_master.isNull() ){
+                  Trace("uf-ss-com-card-debug") << "uf-ss-fair-monotone: Set master : " << tn << std::endl;
+                  d_tn_mono_master = tn;
+                }else{
+                  Trace("uf-ss-com-card-debug") << "uf-ss-fair-monotone: Set slave : " << tn << std::endl;
+                  d_tn_mono_slave[tn] = true;
+                }
+              }else{
+                Trace("uf-ss-com-card-debug") << "uf-ss-fair-monotone: Set non-monotonic : " << tn << std::endl;
+                d_tn_mono_slave[tn] = false;
               }
-            }else{
-              Trace("uf-ss-com-card-debug") << "uf-ss-fair-monotone: Set non-monotonic : " << tn << std::endl;
-              d_tn_mono_slave[tn] = false;
             }
           }
-        }
-        //set the minimum positive cardinality for master if necessary
-        if( polarity && tn==d_tn_mono_master ){
-          Trace("uf-ss-com-card-debug") << "...set min positive cardinality" << std::endl;
-          if( d_min_pos_tn_master_card.get()==-1 || nCard<d_min_pos_tn_master_card.get() ){
-            d_min_pos_tn_master_card.set( nCard );
+          //set the minimum positive cardinality for master if necessary
+          if( polarity && tn==d_tn_mono_master ){
+            Trace("uf-ss-com-card-debug") << "...set min positive cardinality" << std::endl;
+            if( d_min_pos_tn_master_card.get()==-1 || nCard<d_min_pos_tn_master_card.get() ){
+              d_min_pos_tn_master_card.set( nCard );
+            }
           }
         }
-      }
-      Trace("uf-ss-com-card-debug") << "...assert cardinality" << std::endl;
-      d_rep_model[tn]->assertCardinality( d_out, nCard, polarity );
-      //check if combined cardinality is violated
-      checkCombinedCardinality();
-    }else{
-      //otherwise, make equal via lemma
-      if( d_card_assertions_eqv_lemma.find( lit )==d_card_assertions_eqv_lemma.end() ){
-        Node eqv_lit = NodeManager::currentNM()->mkNode( CARDINALITY_CONSTRAINT, ct, lit[1] );
-        eqv_lit = lit.eqNode( eqv_lit );
-        Trace("uf-ss-lemma") << "*** Cardinality equiv lemma : " << eqv_lit << std::endl;
-        getOutputChannel().lemma( eqv_lit );
-        d_card_assertions_eqv_lemma[lit] = true;
-      }
-    }
-  }else if( lit.getKind()==COMBINED_CARDINALITY_CONSTRAINT ){
-    d_com_card_assertions[lit] = polarity;
-    if( polarity ){
-      //safe to assume int here
-      int nCard = lit[0].getConst<Rational>().getNumerator().getSignedInt();
-      if( d_min_pos_com_card.get()==-1 || nCard<d_min_pos_com_card.get() ){
-        d_min_pos_com_card.set( nCard );
+        Trace("uf-ss-com-card-debug") << "...assert cardinality" << std::endl;
+        d_rep_model[tn]->assertCardinality( d_out, nCard, polarity );
+        //check if combined cardinality is violated
         checkCombinedCardinality();
+      }else{
+        //otherwise, make equal via lemma
+        if( d_card_assertions_eqv_lemma.find( lit )==d_card_assertions_eqv_lemma.end() ){
+          Node eqv_lit = NodeManager::currentNM()->mkNode( CARDINALITY_CONSTRAINT, ct, lit[1] );
+          eqv_lit = lit.eqNode( eqv_lit );
+          Trace("uf-ss-lemma") << "*** Cardinality equiv lemma : " << eqv_lit << std::endl;
+          getOutputChannel().lemma( eqv_lit );
+          d_card_assertions_eqv_lemma[lit] = true;
+        }
       }
-    }else{
-      bool needsCard = true;
-      if( d_min_pos_com_card.get()==-1 ){
-        //check if all current combined cardinality constraints are asserted negatively
-        for( std::map< int, Node >::iterator it = d_com_card_literal.begin(); it != d_com_card_literal.end(); ++it ){
-          if( d_com_card_assertions.find( it->second )==d_com_card_assertions.end() ){
-            Trace("uf-ss-com-card-debug") << "Does not need combined cardinality : non-assertion : " << it->first << std::endl;
-            needsCard = false;
-            break;
-          }else{
-            Assert( !d_com_card_assertions[it->second] );
-          }
+    }else if( lit.getKind()==COMBINED_CARDINALITY_CONSTRAINT ){
+      d_com_card_assertions[lit] = polarity;
+      if( polarity ){
+        //safe to assume int here
+        int nCard = lit[0].getConst<Rational>().getNumerator().getSignedInt();
+        if( d_min_pos_com_card.get()==-1 || nCard<d_min_pos_com_card.get() ){
+          d_min_pos_com_card.set( nCard );
+          checkCombinedCardinality();
         }
       }else{
-        Trace("uf-ss-com-card-debug") << "Does not need combined cardinality : positive assertion : " << d_min_pos_com_card.get() << std::endl;
-        needsCard = false;
-      }
-      if( needsCard ){
-        allocateCombinedCardinality();
+        bool needsCard = true;
+        if( d_min_pos_com_card.get()==-1 ){
+          //check if all current combined cardinality constraints are asserted negatively
+          for( std::map< int, Node >::iterator it = d_com_card_literal.begin(); it != d_com_card_literal.end(); ++it ){
+            if( d_com_card_assertions.find( it->second )==d_com_card_assertions.end() ){
+              Trace("uf-ss-com-card-debug") << "Does not need combined cardinality : non-assertion : " << it->first << std::endl;
+              needsCard = false;
+              break;
+            }else{
+              Assert( !d_com_card_assertions[it->second] );
+            }
+          }
+        }else{
+          Trace("uf-ss-com-card-debug") << "Does not need combined cardinality : positive assertion : " << d_min_pos_com_card.get() << std::endl;
+          needsCard = false;
+        }
+        if( needsCard ){
+          allocateCombinedCardinality();
+        }
       }
-    }
-  }else{
-    if( Trace.isOn("uf-ss-warn") ){
-      ////FIXME: this is too strict: theory propagations are showing up as isDecision=true, but
-      ////       a theory propagation is not a decision.
-      if( isDecision ){
-        for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
-          if( !it->second->hasCardinalityAsserted() ){
-            Trace("uf-ss-warn") << "WARNING: Assert " << n << " as a decision before cardinality for " << it->first << "." << std::endl;
-            //Message() << "Error: constraint asserted before cardinality for " << it->first << std::endl;
-            //Unimplemented();
+    }else{
+      if( Trace.isOn("uf-ss-warn") ){
+        ////FIXME: this is too strict: theory propagations are showing up as isDecision=true, but
+        ////       a theory propagation is not a decision.
+        if( isDecision ){
+          for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
+            if( !it->second->hasCardinalityAsserted() ){
+              Trace("uf-ss-warn") << "WARNING: Assert " << n << " as a decision before cardinality for " << it->first << "." << std::endl;
+              //Message() << "Error: constraint asserted before cardinality for " << it->first << std::endl;
+              //Unimplemented();
+            }
           }
         }
       }
-    }
-    if( lit.getKind()!=EQUAL ){
-      //it is a predicate
-      if( options::ufssDiseqPropagation() ){
-        d_deq_prop->assertPredicate(lit, polarity);
+      if( lit.getKind()!=EQUAL ){
+        //it is a predicate
+        if( options::ufssDiseqPropagation() ){
+          d_deq_prop->assertPredicate(lit, polarity);
+        }
       }
     }
+  }else{
+    if( lit.getKind()==CARDINALITY_CONSTRAINT || lit.getKind()==COMBINED_CARDINALITY_CONSTRAINT ){
+      // cardinality constraint from user input, set incomplete   
+      Trace("uf-ss") << "Literal " << lit << " not handled when uf ss mode is not FULL, set incomplete." << std::endl;
+      d_out->setIncomplete();
+    }
   }
   Trace("uf-ss") << "Assert: done " << n << " " << isDecision << std::endl;
 }
@@ -1943,20 +1928,57 @@ bool StrongSolverTheoryUF::areDisequal( Node a, Node b ) {
 /** check */
 void StrongSolverTheoryUF::check( Theory::Effort level ){
   if( !d_conflict ){
-    Trace("uf-ss-solver") << "StrongSolverTheoryUF: check " << level << std::endl;
-    if( level==Theory::EFFORT_FULL && Debug.isOn( "uf-ss-debug" ) ){
-      debugPrint( "uf-ss-debug" );
-    }
-    for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
-      it->second->check( level, d_out );
-      if( it->second->isConflict() ){
-        d_conflict = true;
-        break;
+    if( options::ufssMode()==UF_SS_FULL ){
+      Trace("uf-ss-solver") << "StrongSolverTheoryUF: check " << level << std::endl;
+      if( level==Theory::EFFORT_FULL && Debug.isOn( "uf-ss-debug" ) ){
+        debugPrint( "uf-ss-debug" );
+      }
+      for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
+        it->second->check( level, d_out );
+        if( it->second->isConflict() ){
+          d_conflict = true;
+          break;
+        }
       }
-    }
-    //check symmetry breaker
-    if( !d_conflict && options::ufssSymBreak() ){
-      d_sym_break->check( level );
+      //check symmetry breaker
+      if( !d_conflict && options::ufssSymBreak() ){
+        d_sym_break->check( level );
+      }
+    }else if( options::ufssMode()==UF_SS_NO_MINIMAL ){
+      if( level==Theory::EFFORT_FULL ){
+        // split on an equality between two equivalence classes (at most one per type)
+        std::map< TypeNode, std::vector< Node > > eqc_list;
+        std::map< TypeNode, bool > type_proc;
+        eq::EqClassesIterator eqcs_i(d_th->getEqualityEngine());
+        while( !eqcs_i.isFinished() ){
+          Node a = *eqcs_i;
+          TypeNode tn = a.getType();
+          if( tn.isSort() ){
+            if( type_proc.find( tn )==type_proc.end() ){
+              std::map< TypeNode, std::vector< Node > >::iterator itel = eqc_list.find( tn );
+              if( itel!=eqc_list.end() ){
+                for( unsigned j=0; j<itel->second.size(); j++ ){
+                  Node b = itel->second[j];
+                  if( !d_th->getEqualityEngine()->areDisequal( a, b, false ) ){
+                    Node eq = Rewriter::rewrite( a.eqNode( b ) );
+                    Node lem = NodeManager::currentNM()->mkNode( kind::OR, eq, eq.negate() );
+                    Trace("uf-ss-lemma") << "*** Split (no-minimal) : " << lem << std::endl;
+                    d_out->lemma( lem );
+                    d_out->requirePhase( eq, true );
+                    type_proc[tn] = true;
+                    break;
+                  }
+                }
+              }
+              eqc_list[tn].push_back( a );
+            }
+          }
+          ++eqcs_i;
+        }
+      }
+    }else{
+      // unhandled uf ss mode
+      Assert( false );
     }
     Trace("uf-ss-solver") << "Done StrongSolverTheoryUF: check " << level << std::endl;
   }
@@ -1970,39 +1992,34 @@ void StrongSolverTheoryUF::presolve() {
   }
 }
 
-/** propagate */
-void StrongSolverTheoryUF::propagate( Theory::Effort level ){
-  //for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
-  //  it->second->propagate( level, d_out );
-  //}
-}
-
 /** get next decision request */
 Node StrongSolverTheoryUF::getNextDecisionRequest( unsigned& priority ){
   //request the combined cardinality as a decision literal, if not already asserted
-  if( options::ufssFairness() ){
-    int comCard = 0;
-    Node com_lit;
-    do {
-      if( comCard<d_aloc_com_card.get() ){
-        com_lit = d_com_card_literal.find( comCard )!=d_com_card_literal.end() ? d_com_card_literal[comCard] : Node::null();
-        if( !com_lit.isNull() && d_com_card_assertions.find( com_lit )==d_com_card_assertions.end() ){
-          Trace("uf-ss-dec") << "Decide on combined cardinality : " << com_lit << std::endl;
-          priority = 1;
-          return com_lit;
+  if( options::ufssMode()==UF_SS_FULL ){
+    if( options::ufssFairness() ){
+      int comCard = 0;
+      Node com_lit;
+      do {
+        if( comCard<d_aloc_com_card.get() ){
+          com_lit = d_com_card_literal.find( comCard )!=d_com_card_literal.end() ? d_com_card_literal[comCard] : Node::null();
+          if( !com_lit.isNull() && d_com_card_assertions.find( com_lit )==d_com_card_assertions.end() ){
+            Trace("uf-ss-dec") << "Decide on combined cardinality : " << com_lit << std::endl;
+            priority = 1;
+            return com_lit;
+          }
+          comCard++;
+        }else{
+          com_lit = Node::null();
         }
-        comCard++;
-      }else{
-        com_lit = Node::null();
+      }while( !com_lit.isNull() );
+    }
+    //otherwise, check each individual sort
+    for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
+      Node n = it->second->getNextDecisionRequest();
+      if( !n.isNull() ){
+        priority = 1;
+        return n;
       }
-    }while( !com_lit.isNull() );
-  }
-  //otherwise, check each individual sort
-  for( std::map< TypeNode, SortModel* >::iterator it = d_rep_model.begin(); it != d_rep_model.end(); ++it ){
-    Node n = it->second->getNextDecisionRequest();
-    if( !n.isNull() ){
-      priority = 1;
-      return n;
     }
   }
   Trace("uf-ss-dec") << "...no UF SS decisions." << std::endl;
@@ -2010,42 +2027,44 @@ Node StrongSolverTheoryUF::getNextDecisionRequest( unsigned& priority ){
 }
 
 void StrongSolverTheoryUF::preRegisterTerm( TNode n ){
-  //initialize combined cardinality
-  initializeCombinedCardinality();
-
-  Trace("uf-ss-register") << "Preregister " << n << "." << std::endl;
-  //shouldn't have to preregister this type (it may be that there are no quantifiers over tn)
-  TypeNode tn = n.getType();
-  std::map< TypeNode, SortModel* >::iterator it = d_rep_model.find( tn );
-  if( it==d_rep_model.end() ){
-    SortModel* rm = NULL;
-    if( tn.isSort() ){
-      Trace("uf-ss-register") << "Create sort model " << tn << "." << std::endl;
-      rm  = new SortModel( n, d_th->getSatContext(), d_th->getUserContext(), this );
-      //getOutputChannel().lemma( n.eqNode( rm->getCardinalityTerm() ) );
-    }else{
-      /*
-      if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){
-        Debug("uf-ss-na") << "Error: Cannot perform finite model finding on arithmetic quantifier";
-        Debug("uf-ss-na") << " (" << f << ")";
-        Debug("uf-ss-na") << std::endl;
-        Unimplemented("Cannot perform finite model finding on arithmetic quantifier");
-      }else if( tn.isDatatype() ){
-        Debug("uf-ss-na") << "Error: Cannot perform finite model finding on datatype quantifier";
-        Debug("uf-ss-na") << " (" << f << ")";
-        Debug("uf-ss-na") << std::endl;
-        Unimplemented("Cannot perform finite model finding on datatype quantifier");
+  if( options::ufssMode()==UF_SS_FULL ){
+    //initialize combined cardinality
+    initializeCombinedCardinality();
+
+    Trace("uf-ss-register") << "Preregister " << n << "." << std::endl;
+    //shouldn't have to preregister this type (it may be that there are no quantifiers over tn)
+    TypeNode tn = n.getType();
+    std::map< TypeNode, SortModel* >::iterator it = d_rep_model.find( tn );
+    if( it==d_rep_model.end() ){
+      SortModel* rm = NULL;
+      if( tn.isSort() ){
+        Trace("uf-ss-register") << "Create sort model " << tn << "." << std::endl;
+        rm  = new SortModel( n, d_th->getSatContext(), d_th->getUserContext(), this );
+        //getOutputChannel().lemma( n.eqNode( rm->getCardinalityTerm() ) );
+      }else{
+        /*
+        if( tn==NodeManager::currentNM()->integerType() || tn==NodeManager::currentNM()->realType() ){
+          Debug("uf-ss-na") << "Error: Cannot perform finite model finding on arithmetic quantifier";
+          Debug("uf-ss-na") << " (" << f << ")";
+          Debug("uf-ss-na") << std::endl;
+          Unimplemented("Cannot perform finite model finding on arithmetic quantifier");
+        }else if( tn.isDatatype() ){
+          Debug("uf-ss-na") << "Error: Cannot perform finite model finding on datatype quantifier";
+          Debug("uf-ss-na") << " (" << f << ")";
+          Debug("uf-ss-na") << std::endl;
+          Unimplemented("Cannot perform finite model finding on datatype quantifier");
+        }
+        */
       }
-      */
-    }
-    if( rm ){
-      rm->initialize( d_out );
-      d_rep_model[tn] = rm;
-      //d_rep_model_init[tn] = true;
+      if( rm ){
+        rm->initialize( d_out );
+        d_rep_model[tn] = rm;
+        //d_rep_model_init[tn] = true;
+      }
+    }else{
+      //ensure sort model is initialized
+      it->second->initialize( d_out );
     }
-  }else{
-    //ensure sort model is initialized
-    it->second->initialize( d_out );
   }
 }
 
@@ -2139,6 +2158,7 @@ bool StrongSolverTheoryUF::debugModel( TheoryModel* m ){
 
 /** initialize */
 void StrongSolverTheoryUF::initializeCombinedCardinality() {
+  Assert( options::ufssMode()==UF_SS_FULL );
   if( options::ufssFairness() ){
     if( d_aloc_com_card.get()==0 ){
       Trace("uf-ss-com-card-debug") << "Initialize combined cardinality" << std::endl;
@@ -2149,6 +2169,7 @@ void StrongSolverTheoryUF::initializeCombinedCardinality() {
 
 /** check */
 void StrongSolverTheoryUF::checkCombinedCardinality() {
+  Assert( options::ufssMode()==UF_SS_FULL );
   if( options::ufssFairness() ){
     Trace("uf-ss-com-card-debug") << "Check combined cardinality, get maximum negative cardinalities..." << std::endl;
     int totalCombinedCard = 0;
@@ -2231,6 +2252,7 @@ void StrongSolverTheoryUF::checkCombinedCardinality() {
 }
 
 void StrongSolverTheoryUF::allocateCombinedCardinality() {
+  Assert( options::ufssMode()==UF_SS_FULL );
   Trace("uf-ss-com-card") << "Allocate combined cardinality (" << d_aloc_com_card.get() << ")" << std::endl;
   //make node
   Node lem = NodeManager::currentNM()->mkNode( COMBINED_CARDINALITY_CONSTRAINT,
diff --git a/src/theory/uf/theory_uf_strong_solver.h b/src/theory/uf/theory_uf_strong_solver.h
index b477a7eb5..a7239dba5 100644
--- a/src/theory/uf/theory_uf_strong_solver.h
+++ b/src/theory/uf/theory_uf_strong_solver.h
@@ -396,8 +396,6 @@ public:
   void check( Theory::Effort level );
   /** presolve */
   void presolve();
-  /** propagate */
-  void propagate( Theory::Effort level );
   /** get next decision request */
   Node getNextDecisionRequest( unsigned& priority );
   /** preregister a term */
diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am
index b02443989..4f81d79aa 100644
--- a/test/regress/regress0/fmf/Makefile.am
+++ b/test/regress/regress0/fmf/Makefile.am
@@ -74,7 +74,9 @@ TESTS =	\
 	bug-041417-set-options.cvc \
 	alg202+1.smt2 \
 	fmf-fun-no-elim-ext-arith.smt2 \
-	fmf-fun-no-elim-ext-arith2.smt2
+	fmf-fun-no-elim-ext-arith2.smt2 \
+	cruanes-no-minimal-unk.smt2 \
+	no-minimal-sat.smt2
 
 EXTRA_DIST = $(TESTS)
 
diff --git a/test/regress/regress0/fmf/cruanes-no-minimal-unk.smt2 b/test/regress/regress0/fmf/cruanes-no-minimal-unk.smt2
new file mode 100644
index 000000000..f38a3ce41
--- /dev/null
+++ b/test/regress/regress0/fmf/cruanes-no-minimal-unk.smt2
@@ -0,0 +1,13 @@
+; COMMAND-LINE: --finite-model-find --uf-ss=no-minimal
+; EXPECT: unknown
+(set-logic UFC)
+; generated by Nunchaku
+(declare-sort i_ 0)
+(declare-fun __nun_card_witness_0_ () i_)
+(assert (fmf.card __nun_card_witness_0_ 2))
+(declare-fun i2_ () i_)
+(declare-fun i1_ () i_)
+(declare-fun i3_ () i_)
+(assert (and (not (= i2_ i3_)) (not (= i1_ i2_)) (not (= i1_ i3_))))
+(check-sat)
+
diff --git a/test/regress/regress0/fmf/no-minimal-sat.smt2 b/test/regress/regress0/fmf/no-minimal-sat.smt2
new file mode 100644
index 000000000..dfb7899ce
--- /dev/null
+++ b/test/regress/regress0/fmf/no-minimal-sat.smt2
@@ -0,0 +1,19 @@
+; COMMAND-LINE: --finite-model-find --uf-ss=no-minimal
+; EXPECT: sat
+(set-logic UF)
+(set-info :status sat)
+; generated by Nunchaku
+(declare-sort i_ 0)
+(declare-fun i2_ () i_)
+(declare-fun i1_ () i_)
+(declare-fun i3_ () i_)
+(assert (and (not (= i2_ i3_)) (not (= i1_ i2_)) (not (= i1_ i3_))))
+(declare-fun i4_ () i_)
+(declare-fun i5_ () i_)
+(declare-fun i6_ () i_)
+(assert (distinct i4_ i5_ i6_))
+(declare-fun P (i_) Bool)
+(declare-fun f (i_) i_)
+(assert (forall ((x i_)) (P (f x))))
+(check-sat)
+