Do not throw error when codatatype is not well-founded. Add option for disabling codatatype reasoning. Minor cleanup.

1 files changed, 6 insertions, 2 deletions

diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp
index 9e07c746a..f0704520a 100644
--- a/src/util/datatype.cpp
+++ b/src/util/datatype.cpp
@@ -299,8 +299,12 @@ Expr Datatype::mkGroundTerm( Type t ) const throw(IllegalArgumentException) {
     }
   }
   if( groundTerm.isNull() ){
-    // if we get all the way here, we aren't well-founded
-    CheckArgument(false, *this, "this datatype is not well-founded, cannot construct a ground term!");
+    if( !d_isCo ){
+      // if we get all the way here, we aren't well-founded
+      CheckArgument(false, *this, "this datatype is not well-founded, cannot construct a ground term!");
+    }else{
+      return groundTerm;
+    }
   }else{
     return groundTerm;
   }