X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=execution.cc;h=47a6ebbff7b76dfbbd7f0ec9898606e4f469d29e;hb=0a99a3c4c1c9aab7be017682b43ddf12d609ff4b;hp=fc2370616388d0c60acf8048fceee307e33ef269;hpb=eb6e8431496fc3dfd7638fbfba4229f7215f6308;p=model-checker.git

diff --git a/execution.cc b/execution.cc
index fc23706..47a6ebb 100644
--- a/execution.cc
+++ b/execution.cc
@@ -58,7 +58,7 @@ struct model_snapshot_members {
 
 /** @brief Constructor */
 ModelExecution::ModelExecution(ModelChecker *m,
-		struct model_params *params,
+		const struct model_params *params,
 		Scheduler *scheduler,
 		NodeStack *node_stack) :
 	model(m),
@@ -380,6 +380,8 @@ ModelAction * ModelExecution::get_last_conflict(ModelAction *act) const
 		action_list_t::reverse_iterator rit;
 		for (rit = list->rbegin(); rit != list->rend(); rit++) {
 			ModelAction *prev = *rit;
+			if (prev == act)
+				continue;
 			if (prev->could_synchronize_with(act)) {
 				ret = prev;
 				break;
@@ -2814,7 +2816,7 @@ void ModelExecution::fixup_release_sequences()
 {
 	while (!pending_rel_seqs.empty() &&
 			is_feasible_prefix_ignore_relseq() &&
-			!unrealizedraces.empty()) {
+			haveUnrealizedRaces()) {
 		model_print("*** WARNING: release sequence fixup action "
 				"(%zu pending release seuqence(s)) ***\n",
 				pending_rel_seqs.size());