model: utilize bad_synchronization flag

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 9d2dbb61ef577c43421f6ab071fe5fc7c9323004..47c6cdb92d442f0b0f460e353e9d25c93cfb6dc7 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1280,8 +1280,10 @@ bool ModelChecker::resolve_release_sequences(void *location, work_queue_t *work_
                complete = release_seq_head(rf, &release_heads);
                for (unsigned int i = 0; i < release_heads.size(); i++) {
                        if (!act->has_synchronized_with(release_heads[i])) {
-                               updated = true;
-                               act->synchronize_with(release_heads[i]);
+                               if (act->synchronize_with(release_heads[i]))
+                                       updated = true;
+                               else
+                                       set_bad_synchronization();
                        }
                }