diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-09-23 14:03:49 +0200 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-09-23 14:03:57 +0200 |
commit | 2064e455674aab26e3632da31998bda8b3fff5f9 (patch) | |
tree | 524988e058f1fd4c3e79ed5ea73b3f805c6dd42a /src/util | |
parent | 49747c4574eec3cfa192ffb6e6a2451b949e8b3e (diff) |
Do not throw error when codatatype is not well-founded. Add option for disabling codatatype reasoning. Minor cleanup.
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/datatype.cpp | 8 |
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; } |