From: Brian Norris <banorris@uci.edu>
Date: Sat, 2 Mar 2013 22:04:08 +0000 (-0800)
Subject: model: refactor process_read logic
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=ed16499d4471e6177a08fb93f33da24465574b63;p=cdsspec-compiler.git

model: refactor process_read logic
---

diff --git a/model.cc b/model.cc
index 9e476a9..63ff363 100644
--- a/model.cc
+++ b/model.cc
@@ -864,21 +864,20 @@ bool ModelChecker::process_read(ModelAction *curr)
 			mo_graph->startChanges();
 
 			ASSERT(!is_infeasible());
-			if (!check_recency(curr, rf))
-				priv->too_many_reads = true;
-			updated = r_modification_order(curr, rf);
-
-			if (is_infeasible() && node->increment_read_from()) {
-				mo_graph->rollbackChanges();
-				priv->too_many_reads = false;
-				continue;
+			if (!check_recency(curr, rf)) {
+				if (node->increment_read_from()) {
+					mo_graph->rollbackChanges();
+					continue;
+				} else {
+					priv->too_many_reads = true;
+				}
 			}
 
+			updated = r_modification_order(curr, rf);
 			value = rf->get_value();
 			read_from(curr, rf);
 			mo_graph->commitChanges();
 			mo_check_promises(curr, true);
-
 			break;
 		}
 		case READ_FROM_PROMISE: {