From 30e1feed2331bb44338363228fe73e82ab7c7c3d Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sun, 1 Jun 2014 13:21:05 -0400 Subject: [PATCH] Fix for Windows builds (rlimit doesn't exist on Windows). --- src/main/command_executor.cpp | 21 ++++++++++++++------- 1 file changed, 14 insertions(+), 7 deletions(-) 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 +#ifndef __WIN32__ +# include +#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__ */ } -- 2.30.2