model: use get_write_value()

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index aba71772fde8638892165bf9775df78be30f2819..4fca7aadc48cd09b5c9a2d3490e54872796d0daf 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -874,7 +874,7 @@ bool ModelChecker::process_read(ModelAction *curr)
                        }
 
                        updated = r_modification_order(curr, rf);
-                       value = rf->get_value();
+                       value = rf->get_write_value();
                        read_from(curr, rf);
                        mo_graph->commitChanges();
                        mo_check_promises(curr, true);
@@ -882,7 +882,8 @@ bool ModelChecker::process_read(ModelAction *curr)
                }
                case READ_FROM_PROMISE: {
                        Promise *promise = curr->get_node()->get_read_from_promise();
-                       promise->add_reader(curr);
+                       if (promise->add_reader(curr))
+                               priv->failed_promise = true;
                        value = promise->get_value();
                        curr->set_read_from_promise(promise);
                        mo_graph->startChanges();