X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=c01122191d0e712750b382f87b9c0edbfecf9aa2;hb=8497408d26002ec1a9d7cfd42458f92f2cdd9864;hp=d0dc027150bc629a1df5a839d7c45c9ce1c4d5ee;hpb=381e2769f94f7e41c1c90d3ab633a37136fa24b0;p=model-checker.git

diff --git a/model.cc b/model.cc
index d0dc027..c011221 100644
--- a/model.cc
+++ b/model.cc
@@ -188,6 +188,7 @@ bool ModelChecker::next_execution()
 	DBG();
 
 	num_executions++;
+
 	if (isfinalfeasible()) {
 		printf("Earliest divergence point since last feasible execution:\n");
 		if (earliest_diverge)
@@ -199,6 +200,9 @@ bool ModelChecker::next_execution()
 		num_feasible_executions++;
 	}
 
+	DEBUG("Number of acquires waiting on pending release sequences: %lu\n",
+			pending_acq_rel_seq->size());
+
 	if (isfinalfeasible() || DBG_ENABLED())
 		print_summary();
 
@@ -1477,6 +1481,7 @@ bool ModelChecker::resolve_promises(ModelAction *write)
 			//Make sure the promise's value matches the write's value
 			ASSERT(promise->get_value() == write->get_value());
 
+			delete(promise);
 			promises->erase(promises->begin() + promise_index);
 			resolved = true;
 		} else