From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Sun, 1 Jun 2014 17:21:05 +0000 (-0400)
Subject: Fix for Windows builds (rlimit doesn't exist on Windows).
X-Git-Tag: cvc5-1.0.0~6867
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=30e1feed2331bb44338363228fe73e82ab7c7c3d;p=cvc5.git

Fix for Windows builds (rlimit doesn't exist on Windows).
---

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 94f9a6100..87836b116 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -21,20 +21,27 @@
 
 #include "smt/options.h"
 
-#include <sys/resource.h>
+#ifndef __WIN32__
+#  include <sys/resource.h>
+#endif /* ! __WIN32__ */
 
 namespace CVC4 {
 namespace main {
 
-//function to set no limit on CPU time.
-//this is used for competitions while a solution (proof or model) is being dumped.
-void setNoLimitCPU(){
+// Function to cancel any (externally-imposed) limit on CPU time.
+// This is used for competitions while a solution (proof or model)
+// is being dumped (so that we don't give "sat" or "unsat" then get
+// interrupted partway through outputting a proof!).
+void setNoLimitCPU() {
+  // Windows doesn't have these things, just ignore
+#ifndef __WIN32__
   struct rlimit rlc;
-  int st = getrlimit(RLIMIT_CPU, &rlc );
-  if( st==0 ){
+  int st = getrlimit(RLIMIT_CPU, &rlc);
+  if(st == 0) {
     rlc.rlim_cur = rlc.rlim_max;
-    setrlimit(RLIMIT_CPU, &rlc );
+    setrlimit(RLIMIT_CPU, &rlc);
   }
+#endif /* ! __WIN32__ */
 }