From: Andres Noetzli <noetzli@stanford.edu>
Date: Tue, 16 May 2017 18:08:30 +0000 (-0700)
Subject: Fix error in Windows build
X-Git-Tag: cvc5-1.0.0~5796^2
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=41fb22dfc99a431d471237e48be1acaf01e8cc59;p=cvc5.git

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.
---

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