diff options
| author | Clark Barrett <barrett@cs.stanford.edu> | 2017-05-16 15:10:42 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2017-05-16 15:10:42 -0700 |
| commit | 6316705d252732e1a8abcae1b8b36d77cec8c95d (patch) | |
| tree | 83abf28836588b69cc34dc36e0f70dfbbcabba07 | |
| parent | 3271242a28d7b619152c1fec69c6bd63244b7267 (diff) | |
| parent | 41fb22dfc99a431d471237e48be1acaf01e8cc59 (diff) | |
Merge pull request #160 from 4tXJ7f/fix_win_build
Fix error in Windows build
| -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"); |