diff options
Diffstat (limited to 'src/util/cache.h')
| -rw-r--r-- | src/util/cache.h | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/util/cache.h b/src/util/cache.h index 5183c439b..788c89d83 100644 --- a/src/util/cache.h +++ b/src/util/cache.h @@ -39,8 +39,8 @@ class Cache { typename Map::iterator d_result; // disallow copy/assignment - Cache(const Cache&) CVC4_UNUSED; - Cache& operator=(const Cache&) CVC4_UNUSED; + Cache(const Cache&) CVC4_UNDEFINED; + Cache& operator=(const Cache&) CVC4_UNDEFINED; public: |