summaryrefslogtreecommitdiff
path: root/src/main/main.cpp
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2010-09-13 22:13:36 +0000
committerMorgan Deters <mdeters@gmail.com>2010-09-13 22:13:36 +0000
commit5e619ab6d4622403cc427c17f4282900deb940d5 (patch)
tree3903755af0f3bbf1f10af34d0511fa5807646574 /src/main/main.cpp
parent67f05d7dd6881c689c6e5385feff32d81ae05fb8 (diff)
statistics are now printed on timeout (SIGXCPU) and SIGINT if --stats is given
Diffstat (limited to 'src/main/main.cpp')
-rw-r--r--src/main/main.cpp7
1 files changed, 6 insertions, 1 deletions
diff --git a/src/main/main.cpp b/src/main/main.cpp
index 0b962bc9b..235ebb354 100644
--- a/src/main/main.cpp
+++ b/src/main/main.cpp
@@ -43,7 +43,12 @@ using namespace CVC4::parser;
using namespace CVC4::main;
static Result lastResult;
-static struct Options options;
+
+namespace CVC4 {
+ namespace main {
+ struct Options options;
+ }/* CVC4::main namespace */
+}/* CVC4 namespace */
int runCvc4(int argc, char* argv[]);
void doCommand(SmtEngine&, Command*);
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback