promise: add 'same_value' helper, force value-checking in CycleGraph

[model-checker.git] / cyclegraph.cc

diff --git a/cyclegraph.cc b/cyclegraph.cc
index 7e111b95a3a4bc43334d7037260fdc85ccbfc9c7..be7885c5c1d66a71837f16f07433a913b8c209c1 100644 (file)
--- a/cyclegraph.cc
+++ b/cyclegraph.cc
@@ -151,7 +151,8 @@ bool CycleGraph::mergeNodes(CycleNode *w_node, CycleNode *p_node,
        ASSERT(p_node->is_promise());
 
        const Promise *promise = p_node->getPromise();
-       if (!promise->is_compatible(w_node->getAction())) {
+       if (!promise->is_compatible(w_node->getAction()) ||
+                       !promise->same_value(w_node->getAction())) {
                hasCycles = true;
                return false;
        }