model: correct the "no valid reads" assertion
authorBrian Norris <banorris@uci.edu>
Sat, 23 Feb 2013 00:12:34 +0000 (16:12 -0800)
committerBrian Norris <banorris@uci.edu>
Sat, 23 Feb 2013 00:12:34 +0000 (16:12 -0800)
There are "no valid reads" only if there are no valid prior reads-from
candidates AND no potential values.

model.cc

index 998059e..990f03c 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();
        }