model: remove ModelChecker::is_infeasible_ignoreRMW()

We don't make any special exceptions for this condition anymore, so drop
the function.

diff --git a/model.cc b/model.cc
index 4ccdbce2f6700678ce62a684da817c61b4fa8db3..9e611fae96367283e33d7b927224eb259b52a27e 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -1407,21 +1407,11 @@ bool ModelChecker::is_feasible_prefix_ignore_relseq() const
  */
 bool ModelChecker::is_infeasible() const
 {
-       return mo_graph->checkForRMWViolation() || is_infeasible_ignoreRMW();
-}
-
-/**
- * Check If the current partial trace is infeasible, while ignoring
- * infeasibility related to 2 RMW's reading from the same store. It does not
- * check end-of-execution feasibility.
- * @see ModelChecker::is_infeasible
- * @return whether the current partial trace is infeasible, ignoring multiple
- * RMWs reading from the same store.
- * */
-bool ModelChecker::is_infeasible_ignoreRMW() const
-{
-       return mo_graph->checkForCycles() || priv->failed_promise ||
-               priv->too_many_reads || priv->bad_synchronization ||
+       return mo_graph->checkForRMWViolation() ||
+               mo_graph->checkForCycles() ||
+               priv->failed_promise ||
+               priv->too_many_reads ||
+               priv->bad_synchronization ||
                promises_expired();
 }
 

diff --git a/model.h b/model.h
index 960e9e1a9846a8eefd92a7f0ef394eb975adcbca..c76a28972bf4e6f9fac715386a0a69cb1f4956e3 100644 (file)
--- a/model.h
+++ b/model.h
@@ -257,7 +257,6 @@ private:
 
        void print_infeasibility(const char *prefix) const;
        bool is_feasible_prefix_ignore_relseq() const;
-       bool is_infeasible_ignoreRMW() const;
        bool is_infeasible() const;
        bool is_deadlocked() const;
        bool is_complete_execution() const;