diff options
| author | Andres Noetzli <noetzli@stanford.edu> | 2017-05-16 11:08:30 -0700 |
|---|---|---|
| committer | Andres Noetzli <noetzli@stanford.edu> | 2017-05-16 11:08:30 -0700 |
| commit | 41fb22dfc99a431d471237e48be1acaf01e8cc59 (patch) | |
| tree | 83abf28836588b69cc34dc36e0f70dfbbcabba07 /src/main/util.cpp | |
| parent | 3271242a28d7b619152c1fec69c6bd63244b7267 (diff) | |
Fix error in Windows build
The Windows build was missing the `print_statistics()` function, this commit
moves the function out of the `#ifndef __WIN32__` guard.
Diffstat (limited to 'src/main/util.cpp')
| -rw-r--r-- | src/main/util.cpp | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/src/main/util.cpp b/src/main/util.cpp index 9dc5049a9..72f431b0d 100644 --- a/src/main/util.cpp +++ b/src/main/util.cpp @@ -55,11 +55,6 @@ namespace main { */ bool segvSpin = false; -#ifndef __WIN32__ - -size_t cvc4StackSize; -void* cvc4StackBase; - void print_statistics() { if (pOptions != NULL && pOptions->getStatistics() && pExecutor != NULL) { if (pTotalTime != NULL && pTotalTime->running()) { @@ -69,6 +64,11 @@ void print_statistics() { } } +#ifndef __WIN32__ + +size_t cvc4StackSize; +void* cvc4StackBase; + /** Handler for SIGXCPU, i.e., timeout. */ void timeout_handler(int sig, siginfo_t* info, void*) { safe_print(STDERR_FILENO, "CVC4 interrupted by timeout.\n"); |