model: add RMW violation debug print

diff --git a/model.cc b/model.cc
index ea7b657c3f34c03b8839c3e09be7dbcc6a6ae3a7..fd9068586bc6f23f1371327ce0c337e837c15e9f 100644 (file)
--- a/model.cc
+++ b/model.cc
@@ -723,6 +723,9 @@ bool ModelChecker::isfeasibleprefix() {
 
 /** @return whether the current partial trace is feasible. */
 bool ModelChecker::isfeasible() {
 
 /** @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();
 }
 
        return !mo_graph->checkForRMWViolation() && isfeasibleotherthanRMW();
 }