diff options
Diffstat (limited to 'src/util/statistics_registry.h')
| -rw-r--r-- | src/util/statistics_registry.h | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h index 44f40d5d3..cf47bdf2e 100644 --- a/src/util/statistics_registry.h +++ b/src/util/statistics_registry.h @@ -81,8 +81,8 @@ #include "cvc4_private_library.h" -#ifndef CVC4__STATISTICS_REGISTRY_H -#define CVC4__STATISTICS_REGISTRY_H +#ifndef CVC5__STATISTICS_REGISTRY_H +#define CVC5__STATISTICS_REGISTRY_H #include <ctime> #include <iomanip> @@ -198,4 +198,4 @@ private: } // namespace cvc5 -#endif /* CVC4__STATISTICS_REGISTRY_H */ +#endif /* CVC5__STATISTICS_REGISTRY_H */ |