From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Tue, 1 Nov 2016 21:47:24 +0000 (-0500)
Subject: Minor fix to cvc3_compat.
X-Git-Tag: cvc5-1.0.0~6010
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6404d4f5f65eefbcc91c733f04942d6cb817f46a;p=cvc5.git

Minor fix to cvc3_compat.
---

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(