From ebbaf2d1ff97315fdf97943f122392d1a449e41b Mon Sep 17 00:00:00 2001 From: Brian Norris Date: Fri, 22 Feb 2013 16:12:34 -0800 Subject: [PATCH] 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. --- model.cc | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/model.cc b/model.cc index 998059e2..990f03c5 100644 --- 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(); } -- 2.34.1