diff options
| author | Morgan Deters <mdeters@gmail.com> | 2010-09-13 22:13:36 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2010-09-13 22:13:36 +0000 |
| commit | 5e619ab6d4622403cc427c17f4282900deb940d5 (patch) | |
| tree | 3903755af0f3bbf1f10af34d0511fa5807646574 /src/main/main.h | |
| parent | 67f05d7dd6881c689c6e5385feff32d81ae05fb8 (diff) | |
statistics are now printed on timeout (SIGXCPU) and SIGINT if --stats is given
Diffstat (limited to 'src/main/main.h')
| -rw-r--r-- | src/main/main.h | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/main/main.h b/src/main/main.h index d56684d7d..350578ffa 100644 --- a/src/main/main.h +++ b/src/main/main.h @@ -52,6 +52,12 @@ extern const char *progName; */ extern bool segvNoSpin; +/** + * Keep a copy of the options around globally, so that signal handlers can + * access it. + */ +extern struct Options options; + /** Parse argc/argv and put the result into a CVC4::Options struct. */ int parseOptions(int argc, char** argv, CVC4::Options*) throw(OptionException); |