diff options
| -rw-r--r-- | src/expr/node_manager.h | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index 5e27962da..b5ac9e973 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -1384,15 +1384,18 @@ NodeClass NodeManager::mkConstInternal(const T& val) { nvStack.d_rc = 0; nvStack.d_nchildren = 1; +#if defined(__GNUC__) && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ >= 6)) #pragma GCC diagnostic push #pragma GCC diagnostic ignored "-Warray-bounds" +#endif nvStack.d_children[0] = const_cast<expr::NodeValue*>(reinterpret_cast<const expr::NodeValue*>(&val)); expr::NodeValue* nv = poolLookup(&nvStack); +#if defined(__GNUC__) && (__GNUC__ > 4 || (__GNUC__ == 4 && __GNUC_MINOR__ >= 6)) #pragma GCC diagnostic pop - +#endif if(nv != NULL) { return NodeClass(nv); |