From: Brian Norris <banorris@uci.edu>
Date: Thu, 27 Sep 2012 17:53:37 +0000 (-0700)
Subject: model: add RMW violation debug print
X-Git-Tag: pldi2013~148
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=a3f3df022fdfd22dd6a8e877610b4b82281926fd;p=model-checker.git

model: add RMW violation debug print
---

diff --git a/model.cc b/model.cc
index ea7b657..fd90685 100644
--- a/model.cc
+++ b/model.cc
@@ -723,6 +723,9 @@ bool ModelChecker::isfeasibleprefix() {
 
 /** @return whether the current partial trace is feasible. */
 bool ModelChecker::isfeasible() {
+	if (DBG_ENABLED() && mo_graph->checkForRMWViolation())
+		DEBUG("Infeasible: RMW violation\n");
+
 	return !mo_graph->checkForRMWViolation() && isfeasibleotherthanRMW();
 }