merge upstream/master

1 files changed, 4 insertions, 0 deletions

diff --git a/decoder/cdec.cc b/decoder/cdec.cc
index c671af57..cc3fcff1 100644
--- a/decoder/cdec.cc
+++ b/decoder/cdec.cc
@@ -4,6 +4,8 @@
 #include "decoder.h"
 #include "ff_register.h"
 #include "verbose.h"
+#include "timing_stats.h"
+#include "util/usage.hh"
 
 using namespace std;
 
@@ -27,6 +29,7 @@ int main(int argc, char** argv) {
     if (buf.empty()) continue;
     decoder.Decode(buf);
   }
+  Timer::Summarize();
 #ifdef CP_TIME
     cerr << "Time required for Cube Pruning execution: "
     << CpTime::Get()
@@ -38,6 +41,7 @@ int main(int argc, char** argv) {
       cout << FD::Convert(i) << endl;
     }
   }
+  util::PrintUsage(std::cerr);
   return 0;
 }