Fix to bug 251 (non-spurious warnings in builds) by shifting metakind array by 1...

diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index 515b7978c900682e8ea0a7a93e695921e46cbec5..5f9aa6619ba381182a39cc6c229df4d74dbd0771 100644 (file)
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -114,6 +114,7 @@ typedef ::CVC4::kind::metakind::MetaKind_t MetaKind;
  */
 static inline MetaKind metaKindOf(Kind k) {
   static const MetaKind metaKinds[] = {
+    metakind::INVALID, /* UNDEFINED_KIND */
     metakind::INVALID, /* NULL_EXPR */
 ${metakind_kinds}
     metakind::INVALID /* LAST_KIND */
@@ -121,7 +122,10 @@ ${metakind_kinds}
 
   Assert(k >= kind::NULL_EXPR && k < kind::LAST_KIND);
 
-  return metaKinds[k];
+  // We've asserted that k >= NULL_EXPR (which is 0), but we still
+  // handle the UNDEFINED_KIND (-1) case.  If we don't, the compiler
+  // emits warnings for non-assertion builds, since the check isn't done.
+  return metaKinds[k + 1];
 }/* metaKindOf(k) */
 
 /**