projects
/
satune.git
/ commitdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
| commitdiff |
tree
raw
|
patch
|
inline
| side by side (parent:
2ac885d
)
fixing a bug with bypassMustBeTrueNode
author
Hamed
<hamed.gorjiara@gmail.com>
Mon, 4 Sep 2017 06:29:12 +0000
(23:29 -0700)
committer
Hamed
<hamed.gorjiara@gmail.com>
Mon, 4 Sep 2017 06:29:12 +0000
(23:29 -0700)
src/ASTAnalyses/orderanalysis.cc
patch
|
blob
|
history
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 ...
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;
OrderEdge *newEdge = graph->getOrderEdgeFromOrderGraph(srcNode, sinkNode);
newEdge->mustPos = true;
newEdge->polPos = true;
- if (newEdge->mustNeg)
+ if (newEdge->mustNeg)
{
This->setUnSAT();
This->setUnSAT();
+ }
srcNode->outEdges.add(newEdge);
sinkNode->inEdges.add(newEdge);
}
srcNode->outEdges.add(newEdge);
sinkNode->inEdges.add(newEdge);
}