summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--src/compat/cvc3_compat.cpp4
1 files changed, 1 insertions, 3 deletions
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 8c9992164..18345b3b2 100644
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -1425,9 +1425,7 @@ void ValidityChecker::dataType(const std::vector<std::string>& names,
const CVC4::Datatype& dt = (*i).getDatatype();
// ensure it's well-founded (the check is done here because
// that's how it is in CVC3)
- if(!dt.isWellFounded()) {
- throw TypecheckException(d_em->mkConst(dt), "datatype is not well-founded");
- }
+ CompatCheckArgument(!dt.isWellFounded(), "datatype is not well-founded");
for(CVC4::Datatype::const_iterator j = dt.begin(); j != dt.end(); ++j) {
// For each constructor, register its name and its selectors names.
CompatCheckArgument(
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback