From: Hamed <hamed.gorjiara@gmail.com>
Date: Mon, 4 Sep 2017 06:29:12 +0000 (-0700)
Subject: fixing a bug with bypassMustBeTrueNode
X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=9c7f1f613ab7a41fb0755e9aa923f98a07f955d6

fixing a bug with bypassMustBeTrueNode
---

diff --git a/src/ASTAnalyses/orderanalysis.cc b/src/ASTAnalyses/orderanalysis.cc
index 196561c..a77a1a8 100644
--- a/src/ASTAnalyses/orderanalysis.cc
+++ b/src/ASTAnalyses/orderanalysis.cc
@@ -114,11 +114,18 @@ void bypassMustBeTrueNode(CSolver *This, OrderGraph *graph, OrderNode *node) {
 			OrderNode *sinkNode = outEdge->sink;
 			sinkNode->inEdges.remove(outEdge);
 			//Adding new edge to new sink and src nodes ...
+			if(srcNode == sinkNode){
+				This->setUnSAT();
+				delete iterout;
+				delete iterin;
+				return;
+			}
 			OrderEdge *newEdge = graph->getOrderEdgeFromOrderGraph(srcNode, sinkNode);
 			newEdge->mustPos = true;
 			newEdge->polPos = true;
-			if (newEdge->mustNeg)
+			if (newEdge->mustNeg){
 				This->setUnSAT();
+			}
 			srcNode->outEdges.add(newEdge);
 			sinkNode->inEdges.add(newEdge);
 		}