Handle recursive singleton case for codatatypes, add regression. Simplify implementation of datatype utility: fixes well-foundedness check and mkGroundTerm for parametric datatypes.

1 files changed, 9 insertions, 1 deletions

diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index aa91a5a1e..10a729420 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -362,7 +362,15 @@ Parser::mkMutualDatatypeTypes(const std::vector<Datatype>& datatypes) {
     // complained of a bad substitution if anything is left unresolved.
     // Clear out the set.
     d_unresolved.clear();
-
+    
+    //throw exception if any datatype is not well-founded
+    for(unsigned i = 0; i < datatypes.size(); ++i) {
+      const Datatype& dt = types[i].getDatatype();
+      if( !dt.isCodatatype() && !dt.isWellFounded() ){
+        throw ParserException(dt.getName() + " is not well-founded");
+      }
+    }
+    
     return types;
   } catch(IllegalArgumentException& ie) {
     throw ParserException(ie.getMessage());