diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/main/command_executor.cpp | 21 |
1 files 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 <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__ */ } |