summaryrefslogtreecommitdiff
path: root/src/expr
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr')
-rw-r--r--src/expr/metakind_template.h6
1 files changed, 5 insertions, 1 deletions
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index 515b7978c..5f9aa6619 100644
--- 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) */
/**
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback