From 41fb22dfc99a431d471237e48be1acaf01e8cc59 Mon Sep 17 00:00:00 2001
From: Andres Noetzli <noetzli@stanford.edu>
Date: Tue, 16 May 2017 11:08:30 -0700
Subject: 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.
---
 src/main/util.cpp | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'src/main/util.cpp')

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");
-- 
cgit v1.2.3