model: add PendingFutureValue constructor

[model-checker.git] / model.cc

diff --git a/model.cc b/model.cc
index 98df8f316106a5f4cce404f4cada60ee35c5898a..bc17a882c56f38c7bab1a71064f584ca285e6171 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -871,7 +871,7 @@ bool ModelChecker::process_write(ModelAction *curr)
                                        pfv.act->get_node()->add_future_value(pfv.writer->get_value(), pfv.writer->get_seq_number() + params.maxfuturedelay))
                                set_latest_backtrack(pfv.act);
                }
-               futurevalues->resize(0);
+               futurevalues->clear();
        }
 
        mo_graph->commitChanges();
@@ -1773,8 +1773,7 @@ bool ModelChecker::w_modification_order(ModelAction *curr)
                                if (thin_air_constraint_may_allow(curr, act)) {
                                        if (!is_infeasible() ||
                                                        (curr->is_rmw() && act->is_rmw() && curr->get_reads_from() == act->get_reads_from() && !is_infeasible_ignoreRMW())) {
-                                               struct PendingFutureValue pfv = {curr, act};
-                                               futurevalues->push_back(pfv);
+                                               futurevalues->push_back(PendingFutureValue(curr, act));
                                        }
                                }
                        }