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:25:29 -0500 |
| commit | b1dc477acf7eab8e40705ad20f910be91782cd02 (patch) | |
| tree | d95d543c3f65e08971fc816ae63c187f998d382a /test/unit | |
| parent | 027d650400c1e5e6d0b942ccb42783ee7b5e9060 (diff) | |
Fix timer statistics to report correct time even on process abort.
Diffstat (limited to 'test/unit')
| -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 */ |