use new user-provided witness feature

nyu-acsys · Oct 31, 2024 · 56f2f9d · 56f2f9d
1 parent 9820481
commit 56f2f9d
Showing 1 changed file with 9 additions and 9 deletions.
diff --git a/test/concurrent/treiber_stack/treiber_stack_atomics.rav b/test/concurrent/treiber_stack/treiber_stack_atomics.rav
@@ -50,11 +50,11 @@ module Stack[T: Type] {
 
     {!
       if (res) {
-        assert   
-          (s0 == null ? 
-            cons(x, xs1) == nil : 
-            (cons(x,xs1) != nil && (1.0 > 0.0 && (own(s0, value, cons(x, xs1).head, 1.0) && own(s0, next, top1, 1.0) && list(top1, cons(x, xs1).tail)))));
-        fold list(s0, cons(x, xs1)); 
+        // assert   
+        //   (s0 == null ? 
+        //     cons(x, xs1) == nil : 
+        //     (cons(x,xs1) != nil && (1.0 > 0.0 && (own(s0, value, cons(x, xs1).head, 1.0) && own(s0, next, top1, 1.0) && list(top1, cons(x, xs1).tail)))));
+        fold list(s0, cons(x, xs1))[q := 1.0]; 
         fold stack(s, cons(x, xs1));
         commitAU(phi);
       } else {
@@ -101,11 +101,11 @@ module Stack[T: Type] {
           xs0 == nil : 
           (xs0 != nil && (q > 0.0 && (own(topv, value, xs0.head, q) && own(topv, next, tl0, q) && list(tl0, xs0.tail))));
 
-        assert topv == null ? 
-          xs0 == nil : 
-          (xs0 != nil && (q/2.0 > 0.0 && (own(topv, value, xs0.head, q/2.0) && own(topv, next, tl0, q/2.0) && list(tl0, xs0.tail))));
+        // assert topv == null ? 
+        //   xs0 == nil : 
+        //   (xs0 != nil && (q/2.0 > 0.0 && (own(topv, value, xs0.head, q/2.0) && own(topv, next, tl0, q/2.0) && list(tl0, xs0.tail))));
 
-        fold list(topv, xs0);
+        fold list(topv, xs0)[q := q/2.0];
         fold stack(s, xs0);
         abortAU(phi);
       }