Minor fix for explanations for co-datatypes. Bug fix for explanations in FMF for quantifiers over arrays.

3 files changed, 11 insertions, 2 deletions

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 544589306..65d307a34 100644
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -570,7 +570,12 @@ void TheoryDatatypes::explain(TNode literal, std::vector<TNode>& assumptions){
   TNode atom = polarity ? literal : literal[0];
   if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) {
     explainEquality( atom[0], atom[1], polarity, assumptions );
+  } else if( atom.getKind() == kind::AND && polarity ){
+    for( unsigned i=0; i<atom.getNumChildren(); i++ ){
+      explain( atom[i], assumptions );
+    }
   } else {
+    Assert( atom.getKind()!=kind::AND );
     explainPredicate( atom, polarity, assumptions );
   }
 }
@@ -670,7 +675,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){
             for( unsigned i=0; i<deq_cand.size(); i++ ){
               if( d_equalityEngine.areDisequal( deq_cand[i].first, deq_cand[i].second, true ) ){
                 conf = true;
-                Node eq = NodeManager::currentNM()->mkNode( deq_cand[i].first.getType().isBoolean() ? kind::IFF : kind::EQUAL, 
+                Node eq = NodeManager::currentNM()->mkNode( deq_cand[i].first.getType().isBoolean() ? kind::IFF : kind::EQUAL,
                                                             deq_cand[i].first, deq_cand[i].second );
                 exp.push_back( eq.negate() );
               }
@@ -1488,6 +1493,7 @@ void TheoryDatatypes::checkCycles() {
   }
   //process codatatypes
   if( cod_eqc.size()>1 ){
+    Trace("dt-cod-debug") << "Process " << cod_eqc.size() << " co-datatypes" << std::endl;
     std::vector< std::vector< Node > > part_out;
     std::vector< TNode > exp;
     std::map< Node, Node > cn;
@@ -1496,7 +1502,9 @@ void TheoryDatatypes::checkCycles() {
       cn[cod_eqc[i]] = cod_eqc[i];
     }
     separateBisimilar( cod_eqc, part_out, exp, cn, dni, 0, false );
+    Trace("dt-cod-debug") << "Done separate bisimilar." << std::endl;
     if( !part_out.empty() ){
+      Trace("dt-cod-debug") << "Process partition size " << part_out.size() << std::endl;
       for( unsigned i=0; i<part_out.size(); i++ ){
         std::vector< Node > part;
         part.push_back( part_out[i][0] );
diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp
index d5ed5589b..c21859e87 100644
--- a/src/theory/quantifiers/full_model_check.cpp
+++ b/src/theory/quantifiers/full_model_check.cpp
@@ -871,7 +871,7 @@ void FullModelChecker::doCheck(FirstOrderModelFmc * fm, Node f, Def & d, Node n
       Trace("fmc-debug") << "Can't process base array " << r << std::endl;
       //can't process this array
       d.reset();
-      d.addEntry(fm, defC, Node::null());
+      d.addEntry(fm, mkCondDefault(fm, f), Node::null());
     }
   }
   else if( n.getNumChildren()==0 ){
diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp
index 954272549..5a9b92fa0 100644
--- a/src/theory/rep_set.cpp
+++ b/src/theory/rep_set.cpp
@@ -38,6 +38,7 @@ int RepSet::getNumRepresentatives( TypeNode tn ) const{
 }
 
 void RepSet::add( TypeNode tn, Node n ){
+  Assert( n.getType()==tn );
   d_tmap[ n ] = (int)d_type_reps[tn].size();
   Trace("rsi-debug") << "Add rep #" << d_type_reps[tn].size() << " for " << tn << " : " << n << std::endl;
   d_type_reps[tn].push_back( n );