Makefile: use -rdyanmic only for linking

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 134e457eb44468e02c4d9879e89e1c25a1679c2a..f8aa4f0a4fd49b6eb487539c9fece2d15146e2a0 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1815,6 +1815,7 @@ void ModelChecker::compute_promises(ModelAction *curr)
                                act->is_read() &&
                                !act->could_synchronize_with(curr) &&
                                !act->same_thread(curr) &&
+                               act->get_location() == curr->get_location() &&
                                promise->get_value() == curr->get_value()) {
                        curr->get_node()->set_promise(i);
                }
@@ -1993,6 +1994,7 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
        if (!initialized) {
                /** @todo Need a more informative way of reporting errors. */
                printf("ERROR: may read from uninitialized atomic\n");
+               set_assert();
        }
 
        if (DBG_ENABLED() || !initialized) {
@@ -2002,8 +2004,6 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
                curr->get_node()->print_may_read_from();
                printf("End printing may_read_from\n");
        }
-
-       ASSERT(initialized);
 }
 
 bool ModelChecker::sleep_can_read_from(ModelAction * curr, const ModelAction *write) {