From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Tue, 28 Aug 2018 00:28:08 +0000 (-0700)
Subject: New C++ API: Fix isDefinedKind() to not be ambigious with respect to … (#2384)
X-Git-Tag: cvc5-1.0.0~4713
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=fa55d0680afab5d319f393bafd3f7ecdf8870b1f;p=cvc5.git

New C++ API: Fix isDefinedKind() to not be ambigious with respect to … (#2384)

…underlying type.
---

diff --git a/src/api/cvc4cppkind.h b/src/api/cvc4cppkind.h
index 65affcad4..f91f934f9 100644
--- a/src/api/cvc4cppkind.h
+++ b/src/api/cvc4cppkind.h
@@ -30,8 +30,13 @@ namespace api {
 
 /**
  * The kind of a CVC4 term.
+ *
+ * Note that the underlying type of Kind must be signed (to enable range
+ * checks for validity). The size of this type depends on the size of
+ * CVC4::Kind (__CVC4__EXPR__NODE_VALUE__NBITS__KIND, currently 10 bits,
+ * see expr/metakind_template.h).
  */
-enum CVC4_PUBLIC Kind
+enum CVC4_PUBLIC Kind : int32_t
 {
   /**
    * Internal kind.