diff options
Diffstat (limited to 'src/util/stats.h')
| -rw-r--r-- | src/util/stats.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/util/stats.h b/src/util/stats.h index 4dbf31120..a78070de4 100644 --- a/src/util/stats.h +++ b/src/util/stats.h @@ -43,6 +43,8 @@ namespace CVC4 { class CVC4_PUBLIC Stat; +inline std::ostream& operator<<(std::ostream& os, const ::timespec& t); + /** * The main statistics registry. This registry maintains the list of * currently active statistics and is able to "flush" them all. |