diff options
author | Tim King <taking@cs.nyu.edu> | 2010-06-18 22:24:59 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-06-18 22:24:59 +0000 |
commit | fd6af9181e763cd9564245114cfa47f3952484db (patch) | |
tree | 0b058ad4e0624f1bf11ed9c65d63a4cfbdbdc66e /src/main | |
parent | 968f250b473d97db537aa7628bf111d15a2db299 (diff) |
Merging the statistics branch into the main trunk. I'll go over how to use this Tuesday during the meeting. You'll need to run autogen and receonfigure after updating.
Diffstat (limited to 'src/main')
-rw-r--r-- | src/main/main.cpp | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/main/main.cpp b/src/main/main.cpp index 7fb0d92c9..5c19a995d 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -35,6 +35,7 @@ #include "util/output.h" #include "util/options.h" #include "util/result.h" +#include "util/stats.h" using namespace std; using namespace CVC4; @@ -85,6 +86,7 @@ int main(int argc, char* argv[]) { } } + int runCvc4(int argc, char* argv[]) { // Initialize the signal handlers @@ -183,6 +185,10 @@ int runCvc4(int argc, char* argv[]) { // Remove the parser delete parser; + if(options.statistics){ + StatisticsRegistry::flushStatistics(cerr); + } + switch(lastResult.asSatisfiabilityResult().isSAT()) { case Result::SAT: |