diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-12-10 23:17:13 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-12-10 23:26:50 -0500 |
| commit | b337066773212390eedff81aaacffe3f226b6549 (patch) | |
| tree | 1409670b6951ea3c7fe05a07b00628eef971f96c /test/unit/util/stats_black.h | |
| parent | 811202ddd6851e61c71aa4db92a2231986aa99ff (diff) | |
Fix timer statistics to report correct time even on process abort.
Diffstat (limited to 'test/unit/util/stats_black.h')
| -rw-r--r-- | test/unit/util/stats_black.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test/unit/util/stats_black.h b/test/unit/util/stats_black.h index 3e3f6b942..1367a62c1 100644 --- a/test/unit/util/stats_black.h +++ b/test/unit/util/stats_black.h @@ -94,7 +94,7 @@ public: sTimer.start(); timespec zero = { 0, 0 }; - TS_ASSERT_EQUALS(zero, sTimer.getData()); + //TS_ASSERT_EQUALS(zero, sTimer.getData()); sTimer.stop(); TS_ASSERT_LESS_THAN(zero, sTimer.getData()); #endif /* CVC4_STATISTICS_ON */ |