diff options
| -rw-r--r-- | src/api/cvc4cppkind.h | 7 |
1 files changed, 6 insertions, 1 deletions
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. |