Add #nodes console output

diff --git a/base/main.cc b/base/main.cc
index 6e3f0332769084d331e20ce18f1d4d782d5c7856..0b0d4b5fac8c07ba6154d80c3cafc384a75dc0f8 100644 (file)
--- a/base/main.cc
+++ b/base/main.cc
@@ -69,6 +69,7 @@ int main()
 
         std::cerr << "Elapsed is " << p.elapsed() << std::endl;
         std::cerr << "Goal found is " << p.goal_found() << std::endl;
+        std::cerr << "#nodes is " << p.nodes().size() << std::endl;
         std::cerr << "`tlog` size is " << p.tlog().size() << std::endl;
 
         Json::Value jvo; // JSON output