diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-05-30 15:41:20 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-05-30 16:36:43 -0400 |
| commit | 7088a6ffa1fd470dc677a589014a467480f9e2b5 (patch) | |
| tree | 3f45951a4b290f7ad00d7b3e6edc2fb2bbab0508 /test/system | |
| parent | 47ad6ac144a2e23d971fffd982951e93d93e88ad (diff) | |
Update submission make rules.
Diffstat (limited to 'test/system')
| -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; } |