model: correct the "no valid reads" assertion

There are "no valid reads" only if there are no valid prior reads-from
candidates AND no potential values.

diff --git a/model.cc b/model.cc
index 998059e2451e7e652d2493af3fc6785aad9ba542..990f03c5d9ef38d856c9cec5a46c6e7ad94b6ecd 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -2619,7 +2619,7 @@ void ModelChecker::build_reads_from_past(ModelAction *curr)
                }
        }
        /* We may find no valid may-read-from only if the execution is doomed */
-       if (!curr->get_node()->get_read_from_size()) {
+       if (!curr->get_node()->get_read_from_size() && curr->get_node()->future_value_empty()) {
                priv->no_valid_reads = true;
                set_assert();
        }