X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fpapers%2Fuse_case%2Fstats%2Fmkdiff.cc;h=d31bfbfc13d9a8aad9d4ab4bd8db696569e339d0;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=aed015dca81935b86e105cfbddc2fd1f2db3a6a4;hpb=a84be8db90f3f27148074c22d80b21a2dcf58576;p=helm.git

diff --git a/helm/papers/use_case/stats/mkdiff.cc b/helm/papers/use_case/stats/mkdiff.cc
index aed015dca..d31bfbfc1 100644
--- a/helm/papers/use_case/stats/mkdiff.cc
+++ b/helm/papers/use_case/stats/mkdiff.cc
@@ -7,20 +7,23 @@ main(int argc, char* argv[])
 {
 	std::ifstream f(argv[1]);
 
-	int size, nodes, parsing_time;
-	int size1, nodes1, validating_time;
+	int size, nodes, depth, parsing_time;
+	int size1, nodes1, depth1, validating_time;
 
 	while (std::cin >> size) {
 		std::cin >> nodes;
+		std::cin >> depth;
 		std::cin >> parsing_time;
 
 		f >> size1;
 		f >> nodes1;
+		f >> depth1;
 		f >> validating_time;
 
 		assert(size == size1);
 		assert(nodes == nodes1);
-		std::cout << size << " " << nodes << " " << (validating_time - parsing_time) << std::endl;
+		assert(depth == depth1);
+		std::cout << size << " " << nodes << " " << depth << " " << (validating_time - parsing_time) << std::endl;
 	}
 }