worklist version

[repair.git] / Repair / RepairCompiler / MCC / link.model

diff --git a/Repair/RepairCompiler/MCC/link.model b/Repair/RepairCompiler/MCC/link.model
index b8451212aa47831fab193b954ae90ab6552e3035..855104cb07fdc9149cac1e43aecad3b5e9a73c72 100755 (executable)
--- a/Repair/RepairCompiler/MCC/link.model
+++ b/Repair/RepairCompiler/MCC/link.model
@@ -1,5 +1,7 @@
-[], true => head in Nodes;
+[], literal(true) => head in Nodes;
 [forall node in Nodes], !node.next=literal(0) => node.next in Nodes;
-[forall node in Nodes], true => <node, node.next> in nextnodes;
+[forall node in Nodes], !node.next=literal(0) => <node, node.next> in nextnodes;
+[forall node in Nodes], !node.prev=literal(0) => node.prev in Nodes;
+[forall node in Nodes], !node.prev=literal(0) => <node, node.prev> in prevnodes;