From 56f2f9debd00828c44cfdd0ab3aa85f8db7488ca Mon Sep 17 00:00:00 2001 From: Thomas Wies Date: Thu, 31 Oct 2024 00:58:53 -0400 Subject: [PATCH] use new user-provided witness feature --- .../treiber_stack/treiber_stack_atomics.rav | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/test/concurrent/treiber_stack/treiber_stack_atomics.rav b/test/concurrent/treiber_stack/treiber_stack_atomics.rav index e300694..ff5d91e 100644 --- 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); }