fixed test

Author: shazqadeer

Test/datatypes/node-client.bpl

@@ -3,20 +3,27 @@
 
 type TaggedLocNode V = TaggedLoc (Node V) Unit;
 
-datatype Treiber<V> { Treiber(top: Option (LocNode V), {:linear} nodes: Map (LocNode V) (Node V)) }
+datatype Treiber<V> { Treiber(top: Option (LocNode V), {:linear} nodes: Map (One (LocNode V)) (Node V)) }
 type LocTreiber V = Loc (Treiber V);
 type TaggedLocTreiber V = TaggedLoc (Treiber V) Unit;
 
 type X;
 var ts: Map (LocTreiber X) (Treiber X);
 
+function {:inline} SubsetInv(ts: Map (LocTreiber X) (Treiber X), ref_t: LocTreiber X): bool
+{
+  (var t := Map_At(ts, ref_t);
+    (var m := t->nodes; 
+      (forall x: LocNode X:: BetweenSet(m->val, t->top, None())[x] ==> Set_Contains(m->dom, One(x)))))
+}
+
 procedure YieldInv(ref_t: LocTreiber X)
 requires Map_Contains(ts, ref_t);
 requires (var t := Map_At(ts, ref_t); Between(t->nodes->val, t->top, None(), None()));
-requires (var t := Map_At(ts, ref_t); (var m := t->nodes; IsSubset(BetweenSet(m->val, t->top, None()), m->dom->val)));
+requires SubsetInv(ts, ref_t);
 ensures Map_Contains(ts, ref_t);
 ensures (var t := Map_At(ts, ref_t); Between(t->nodes->val, t->top, None(), None()));
-ensures (var t := Map_At(ts, ref_t); (var m := t->nodes; IsSubset(BetweenSet(m->val, t->top, None()), m->dom->val)));
+ensures SubsetInv(ts, ref_t);
 modifies ts;
 {
   var x: X;
@@ -31,8 +38,8 @@ modifies ts;
   var loc_n_opt: Option (LocNode X);
   assert Map_Contains(ts, loc_t);
   treiber := Map_At(ts, loc_t);
-  assume treiber->top is Some && Map_Contains(treiber->nodes, treiber->top->t);
-  Node(loc_n_opt, x) := Map_At(treiber->nodes, treiber->top->t);
+  assume treiber->top is Some && Map_Contains(treiber->nodes, One(treiber->top->t));
+  Node(loc_n_opt, x) := Map_At(treiber->nodes, One(treiber->top->t));
   treiber->top := loc_n_opt;
   ts := Map_Update(ts, loc_t, treiber);
 }
@@ -44,8 +51,8 @@ modifies ts;
   var loc_n: LocNode X;
   assert Map_Contains(ts, loc_t);
   treiber := Map_At(ts, loc_t);
-  assume !Map_Contains(treiber->nodes, loc_n);
-  treiber->nodes := Map_Update(treiber->nodes, loc_n, Node(treiber->top, x));
+  assume !Map_Contains(treiber->nodes, One(loc_n));
+  treiber->nodes := Map_Update(treiber->nodes, One(loc_n), Node(treiber->top, x));
   treiber->top := Some(loc_n);
   ts := Map_Update(ts, loc_t, treiber);
 }