Minor changes related to codatatypes for 1.5 release.

diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp
index 371f27c95b44483d4a40860268cb045df319461a..e0a4dc7d86ddb3c9403a2b190d399bed66443210 100644 (file)
--- a/src/theory/datatypes/theory_datatypes.cpp
+++ b/src/theory/datatypes/theory_datatypes.cpp
@@ -1414,11 +1414,15 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){
     Node eqc = it->first;
     const Datatype& dt = ((DatatypeType)(eqc.getType()).toType()).getDatatype();
     if( dt.isCodatatype() ){
+      //until models are implemented for codatatypes
+      throw Exception("Models for codatatypes are not supported in this version.");
+      /*
       std::map< Node, Node > vmap;
       std::vector< Node > fv;
       Node v = getCodatatypesValue( it->first, eqc_cons, eqc_mu, vmap, fv );
       Trace("dt-cmi-cdt") << "  EQC(" << it->first << "), constructor is " << it->second << ", value is " << v << ", const = " << v.isConst() << std::endl;
       //m->assertEquality( eqc, v, true );
+      */
     }
   }
 }

diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp
index db0328f4fef8cac82b93233047cef04dcff1f5ba..58f0a265e4577b187a17c92a40978d4267204f2f 100644 (file)
--- a/src/theory/quantifiers/term_database.cpp
+++ b/src/theory/quantifiers/term_database.cpp
@@ -1558,7 +1558,8 @@ void TermDb::registerTrigger( theory::inst::Trigger* tr, Node op ){
 
 bool TermDb::isInductionTerm( Node n ) {
   if( options::dtStcInduction() && datatypes::DatatypesRewriter::isTermDatatype( n ) ){
-    return true;
+    const Datatype& dt = ((DatatypeType)(n.getType()).toType()).getDatatype();
+    return !dt.isCodatatype();
   }
   if( options::intWfInduction() && n.getType().isInteger() ){
     return true;