diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-04-30 23:55:18 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2010-04-30 23:55:18 +0000 |
commit | cb9a9b98b018106a02b31f2442f347a944d8dda8 (patch) | |
tree | 1669047e13e1224114e9fcea83b212dd6d72836d /src/expr/metakind_template.h | |
parent | 349131957e91150c24a9c69f5e1f04e34494b0c6 (diff) |
Fix for bug 115, mapping was going in the wrong direction.
Diffstat (limited to 'src/expr/metakind_template.h')
-rw-r--r-- | src/expr/metakind_template.h | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index 57bfc51e5..5b0ac150b 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -148,13 +148,11 @@ ${metakind_canbeatomic} * VARIABLE to APPLY_UF. */ static inline Kind operatorKindToKind(Kind k) { - static const Kind kind2kind[] = { - kind::UNDEFINED_KIND, /* NULL_EXPR */ + switch (k) { ${metakind_operatorKinds} - kind::UNDEFINED_KIND /* LAST_KIND */ + default: + return kind::UNDEFINED_KIND; /* LAST_KIND */ }; - - return kind2kind[k]; } }/* CVC4::kind namespace */ |