diff options
Diffstat (limited to 'test/system/statistics.cpp')
| -rw-r--r-- | test/system/statistics.cpp | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/test/system/statistics.cpp b/test/system/statistics.cpp index 1749727f3..8139167a4 100644 --- a/test/system/statistics.cpp +++ b/test/system/statistics.cpp @@ -59,10 +59,12 @@ int main() { different = different || stats.getStatistic((*i).first) != (*i).second; } +#ifdef CVC4_STATISTICS_ON if(!different) { cout << "stats are the same! bailing.." << endl; exit(1); } +#endif /* CVC4_STATISTICS_ON */ return r == Result::VALID ? 0 : 1; } |