From: bdemsky <bdemsky@uci.edu>
Date: Fri, 18 Aug 2017 05:15:15 +0000 (-0700)
Subject: fix logic
X-Git-Url: http://demsky.eecs.uci.edu/git/?a=commitdiff_plain;h=f98cc4deea745afff3628ced7f27070e9489adac;p=satune.git

fix logic
---

diff --git a/src/Encoders/orderencoder.c b/src/Encoders/orderencoder.c
index 5a9dcb9..c8a9b72 100644
--- a/src/Encoders/orderencoder.c
+++ b/src/Encoders/orderencoder.c
@@ -223,12 +223,12 @@ void DFSClearContradictions(OrderGraph *graph, VectorOrderNode *finishNodes, boo
 			deleteIterOrderEdge(iterator);
 		}
 		{
-			//Use source sets to compute mustNeg edges that would introduce cycle if true
+			//Use source sets to compute mustNeg for edges that would introduce cycle if true
 			HSIteratorOrderEdge *iterator = iteratorOrderEdge(node->outEdges);
 			while (hasNextOrderEdge(iterator)) {
 				OrderEdge *edge = nextOrderEdge(iterator);
 				OrderNode *child = edge->sink;
-				if (!edge->mustPos && containsHashSetOrderNode(sources, child)) {
+				if (!edge->mustNeg && containsHashSetOrderNode(sources, child)) {
 					edge->mustNeg = true;
 				}
 			}
@@ -290,10 +290,11 @@ void localMustAnalysisPartial(OrderGraph *graph) {
 				edge->polNeg = false;
 			}
 			OrderEdge *invEdge = getInverseOrderEdge(graph, edge);
-			if (invEdge != NULL && !invEdge->mustPos) {
-				invEdge->polPos = false;
+			if (invEdge != NULL) {
+				if (!invEdge->mustPos)
+					invEdge->polPos = false;
+				invEdge->mustNeg = true;
 			}
-			invEdge->mustNeg = true;
 		}
 		if (edge->mustNeg && !edge->mustPos) {
 			edge->polPos = false;