fixing a bug with bypassMustBeTrueNode

[satune.git] / src / ASTAnalyses / orderanalysis.cc

diff --git a/src/ASTAnalyses/orderanalysis.cc b/src/ASTAnalyses/orderanalysis.cc
index 196561caa434e0ff74c42d9eb55481084a889fb8..a77a1a8418b086dd143c3e549034dde836d62988 100644 (file)
--- 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);
                }