X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=466bf613a905ece97aaba98c506e1bf9234109e7;hb=251c63183adee7dbdceeabce5a706e8281bc2887;hp=e0c3089e4ec1558e072cd3577b22caa3d3a546e1;hpb=63c96bfb56ee71259fcbb4d57a2350424944e28a;p=model-checker.git

diff --git a/model.cc b/model.cc
index e0c3089..466bf61 100644
--- a/model.cc
+++ b/model.cc
@@ -36,8 +36,6 @@ ModelChecker::ModelChecker(struct model_params params) :
 ModelChecker::~ModelChecker()
 {
 	delete node_stack;
-	for (unsigned int i = 0; i < trace_analyses.size(); i++)
-		delete trace_analyses[i];
 	delete scheduler;
 }
 
@@ -256,7 +254,7 @@ void ModelChecker::print_execution(bool printbugs) const
 {
 	print_program_output();
 
-	if (params.verbose) {
+	if (params.verbose >= 2) {
 		model_print("Earliest divergence point since last feasible execution:\n");
 		if (earliest_diverge)
 			earliest_diverge->print();
@@ -485,4 +483,8 @@ void ModelChecker::run()
 
 	model_print("******* Model-checking complete: *******\n");
 	print_stats();
+
+	/* Have the trace analyses dump their output. */
+	for (unsigned int i = 0; i < trace_analyses.size(); i++)
+		trace_analyses[i]->finish();
 }