Fix error in Windows build
authorAndres Noetzli <noetzli@stanford.edu>
Tue, 16 May 2017 18:08:30 +0000 (11:08 -0700)
committerAndres Noetzli <noetzli@stanford.edu>
Tue, 16 May 2017 18:08:30 +0000 (11:08 -0700)
The Windows build was missing the `print_statistics()` function, this commit
moves the function out of the `#ifndef __WIN32__` guard.

src/main/util.cpp

index 9dc5049a92de5a9230ea0d91307e953822284756..72f431b0d8df07e78715b2817d5dd44ce74b5034 100644 (file)
@@ -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");