diff options
| -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"); |