model: bugfix - inherit future values from previous loads

[model-checker.git] / nodestack.cc

diff --git a/nodestack.cc b/nodestack.cc
index addf93f67469f1cd7f96a15ffad8ec5551cb1c1b..59e9b5dcad8f9630b2e9dd7ad25a97728ea25458 100644 (file)
--- a/nodestack.cc
+++ b/nodestack.cc
@@ -226,7 +226,7 @@ bool Node::misc_empty() const
  * @param value is the value to backtrack to.
  * @return True if the future value was successully added; false otherwise
  */
-bool Node::add_future_value(struct future_value& fv)
+bool Node::add_future_value(struct future_value fv)
 {
        uint64_t value = fv.value;
        modelclock_t expiration = fv.expiration;
@@ -556,7 +556,11 @@ ModelAction * NodeStack::explore_action(ModelAction *act, enabled_type_t *is_ena
                if (model->params.fairwindow != 0 && head_idx > (int)model->params.fairwindow)
                        prevfairness = node_list[head_idx - model->params.fairwindow];
        }
-       node_list.push_back(new Node(act, head, model->get_num_threads(), prevfairness));
+
+       int next_threads = model->get_num_threads();
+       if (act->get_type() == THREAD_CREATE)
+               next_threads++;
+       node_list.push_back(new Node(act, head, next_threads, prevfairness));
        total_nodes++;
        head_idx++;
        return NULL;