X-Git-Url: http://demsky.eecs.uci.edu/git/?a=blobdiff_plain;f=model.cc;h=1ecc48e395ffbe0a13b00b5dbeba02985de33ec2;hb=72524dae1144e6fe437c8317f8f718e534ccfe0f;hp=9e611fae96367283e33d7b927224eb259b52a27e;hpb=b1de3c01aaea4141cd01410ef739a00f2987b567;p=model-checker.git

diff --git a/model.cc b/model.cc
index 9e611fa..1ecc48e 100644
--- a/model.cc
+++ b/model.cc
@@ -1372,8 +1372,6 @@ void ModelChecker::print_infeasibility(const char *prefix) const
 {
 	char buf[100];
 	char *ptr = buf;
-	if (mo_graph->checkForRMWViolation())
-		ptr += sprintf(ptr, "[RMW atomicity]");
 	if (mo_graph->checkForCycles())
 		ptr += sprintf(ptr, "[mo cycle]");
 	if (priv->failed_promise)
@@ -1407,8 +1405,7 @@ bool ModelChecker::is_feasible_prefix_ignore_relseq() const
  */
 bool ModelChecker::is_infeasible() const
 {
-	return mo_graph->checkForRMWViolation() ||
-		mo_graph->checkForCycles() ||
+	return mo_graph->checkForCycles() ||
 		priv->failed_promise ||
 		priv->too_many_reads ||
 		priv->bad_synchronization ||