X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=e23e9ec0a990b38e962b249f4d32c666f9885689;hb=92c453e0b51244839270e67528e7a18ba6af82b0;hp=08ea3294b3b963b63ec8d63f3d1a88a39dc7b728;hpb=7616e1626a8bdb735ed4f0b4da56f4816fc9cded;p=model-checker.git

diff --git a/model.cc b/model.cc
index 08ea329..e23e9ec 100644
--- a/model.cc
+++ b/model.cc
@@ -1984,9 +1984,10 @@ bool ModelChecker::take_step() {
 	 *     the 'model_thread')
 	 * (2) pending release sequences
 	 * (3) pending assertions (i.e., data races)
+	 * (4) no pending promises
 	 */
 	if (!pending_rel_seqs->empty() && (!next || next->is_model_thread()) &&
-			!unrealizedraces.empty()) {
+			isfinalfeasible() && !unrealizedraces.empty()) {
 		printf("*** WARNING: release sequence fixup action (%zu pending release seuqences) ***\n",
 				pending_rel_seqs->size());
 		ModelAction *fixup = new ModelAction(MODEL_FIXUP_RELSEQ,