diff --git a/Source/Concurrency/LinearRewriter.cs b/Source/Concurrency/LinearRewriter.cs
index daaac2881..da6fbd404 100644
--- a/Source/Concurrency/LinearRewriter.cs
+++ b/Source/Concurrency/LinearRewriter.cs
@@ -59,6 +59,8 @@ public List<Cmd> RewriteCallCmd(CallCmd callCmd)
     switch (Monomorphizer.GetOriginalDecl(callCmd.Proc).Name)
     {
       case "One_New":
+      case "One_To_Fractions":
+      case "Fractions_To_One":
       case "Cell_Pack":
       case "Cell_Unpack":
       case "Set_MakeEmpty":
diff --git a/Source/Core/CivlAttributes.cs b/Source/Core/CivlAttributes.cs
index e8d629042..972486e7e 100644
--- a/Source/Core/CivlAttributes.cs
+++ b/Source/Core/CivlAttributes.cs
@@ -180,7 +180,7 @@ public static class CivlPrimitives
   {
     public static HashSet<string> LinearPrimitives = new()
     {
-      "One_New",
+      "One_New", "One_To_Fractions", "Fractions_To_One",
       "Cell_Pack", "Cell_Unpack",
       "Map_MakeEmpty", "Map_Split", "Map_Get", "Map_Put", "Map_Assume",
       "Set_MakeEmpty", "Set_Split", "Set_Get", "Set_Put", "One_Split", "One_Get", "One_Put"
diff --git a/Source/Core/base.bpl b/Source/Core/base.bpl
index cd0b90dd2..b56c989ff 100644
--- a/Source/Core/base.bpl
+++ b/Source/Core/base.bpl
@@ -278,7 +278,8 @@ function {:inline} Map_Swap<T,U>(a: Map T U, t1: T, t2: T): Map T U
   (var u1, u2 := Map_At(a, t1), Map_At(a, t2); Map_Update(Map_Update(a, t1, u2), t2, u1))
 }
 
-function {:inline} Map_WellFormed<T,U>(a: Map T U): bool {
+function {:inline} Map_WellFormed<T,U>(a: Map T U): bool
+{
   a->val == MapIte(a->dom->val, a->val, MapConst(Default()))
 }
 
@@ -295,6 +296,19 @@ function {:inline} One_Collector<T>(a: One T): [T]bool
   MapOne(a->val)
 }
 
+datatype Fraction<T, K> { Fraction(val: T, id: K, ids: [K]bool) }
+
+pure procedure {:inline 1} One_To_Fractions<T,K>({:linear_in} one_t: One T, ids: [K]bool) returns ({:linear} pieces: Set (Fraction T K))
+{
+  pieces := Set((lambda piece: Fraction T K :: piece->val == one_t->val && ids[piece->id] && piece->ids == ids));
+}
+
+pure procedure {:inline 1} Fractions_To_One<T,K>({:linear_out} one_t: One T, ids: [K]bool, {:linear_in} pieces: Set (Fraction T K))
+{
+  assert (forall piece: Fraction T K:: Set_Contains(pieces, piece) ==> piece->val == one_t->val && piece->ids == ids);
+  assert pieces == Set((lambda piece: Fraction T K :: piece->val == one_t->val && ids[piece->id] && piece->ids == ids));
+}
+
 /// singleton map
 datatype Cell<T,U> { Cell(key: T, val: U) }
 
diff --git a/Test/civl/samples/treiber-stack.bpl b/Test/civl/samples/treiber-stack.bpl
index b62105120..bffba4cf5 100644
--- a/Test/civl/samples/treiber-stack.bpl
+++ b/Test/civl/samples/treiber-stack.bpl
@@ -1,8 +1,12 @@
 // RUN: %parallel-boogie -lib:base -lib:node "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
+datatype LocPiece { Left(), Right() }
+const AllLocPieces: [LocPiece]bool;
+axiom AllLocPieces == MapConst(false)[Left() := true][Right() := true];
+
 type TreiberNode _;
-type LocTreiberNode T = Loc (TreiberNode T);
+type LocTreiberNode T = Fraction (Loc (TreiberNode T)) LocPiece;
 type StackElem T = Node (LocTreiberNode T) T;
 type StackMap T = Map (LocTreiberNode T) (StackElem T);
 datatype Treiber<T> { Treiber(top: Option (LocTreiberNode T), {:linear} stack: StackMap T) }
@@ -12,6 +16,47 @@ type X; // module type parameter
 var {:layer 4, 5} Stack: Map (Loc (Treiber X)) (Vec X);
 var {:layer 0, 4} {:linear} ts: Map (Loc (Treiber X)) (Treiber X);
 
+/// Yield invariants
+
+function {:inline} Domain(ts: Map (Loc (Treiber X)) (Treiber X), loc_t: Loc (Treiber X)): Set (LocTreiberNode X) {
+  ts->val[loc_t]->stack->dom
+}
+
+yield invariant {:layer 1} Yield();
+
+yield invariant {:layer 2} TopInStack(loc_t: Loc (Treiber X));
+invariant Map_Contains(ts, loc_t);
+invariant (var loc_n := Map_At(ts, loc_t)->top; loc_n is None || Set_Contains(Domain(ts, loc_t), loc_n->t));
+invariant (forall loc_n: LocTreiberNode X :: Set_Contains(Domain(ts, loc_t), loc_n) ==> 
+              (var loc_n' := Map_At(Map_At(ts, loc_t)->stack, loc_n)->next; loc_n' is None || Set_Contains(Domain(ts, loc_t), loc_n'->t)));
+
+yield invariant {:layer 2} LocInStack(loc_t: Loc (Treiber X), loc_n: Option (LocTreiberNode X));
+invariant Map_Contains(ts, loc_t);
+invariant loc_n is None || Set_Contains(Domain(ts, loc_t), loc_n->t);
+
+yield invariant {:layer 4} ReachInStack(loc_t: Loc (Treiber X));
+invariant Map_Contains(ts, loc_t);
+invariant (var t := ts->val[loc_t]; Between(t->stack->val, t->top, t->top, None()));
+invariant (var t := ts->val[loc_t]; IsSubset(BetweenSet(t->stack->val, t->top, None()), Domain(ts, loc_t)->val));
+invariant (var loc_n := Map_At(ts, loc_t)->top; loc_n is None || Set_Contains(Domain(ts, loc_t), loc_n->t));
+invariant (forall {:pool "A"} loc_n: LocTreiberNode X :: {:add_to_pool "A", loc_n} Set_Contains(Domain(ts, loc_t), loc_n) ==>
+              loc_n == Fraction(loc_n->val, Left(), AllLocPieces) &&
+              (var loc_n' := Map_At(Map_At(ts, loc_t)->stack, loc_n)->next; loc_n' is None || Set_Contains(Domain(ts, loc_t), loc_n'->t)));
+invariant Map_At(Stack, loc_t) == Abs(Map_At(ts, loc_t));
+
+yield invariant {:layer 4} StackDom();
+invariant Stack->dom == ts->dom;
+
+yield invariant {:layer 4} PushLocInStack(
+  loc_t: Loc (Treiber X), node: StackElem X, new_loc_n: LocTreiberNode X, {:linear} right_loc_piece: One (LocTreiberNode X));
+invariant Map_Contains(ts, loc_t);
+invariant Set_Contains(Domain(ts, loc_t), new_loc_n);
+invariant right_loc_piece->val == Fraction(new_loc_n->val, Right(), AllLocPieces);
+invariant new_loc_n == Fraction(new_loc_n->val, Left(), AllLocPieces);
+invariant (var t := ts->val[loc_t]; Map_At(t->stack, new_loc_n) == node && !BetweenSet(t->stack->val, t->top, None())[new_loc_n]);
+
+/// Layered implementation
+
 atomic action {:layer 5} AtomicAlloc() returns (loc_t: Loc (Treiber X))
 modifies Stack;
 {
@@ -24,7 +69,7 @@ modifies Stack;
 }
 yield procedure {:layer 4} Alloc() returns (loc_t: Loc (Treiber X))
 refines AtomicAlloc;
-preserves call YieldInvDom#4();
+preserves call StackDom();
 {
   var top: Option (LocTreiberNode X);
   var {:linear} stack: StackMap X;
@@ -38,7 +83,7 @@ preserves call YieldInvDom#4();
   call one_loc_t := One_New();
   call cell_t := Cell_Pack(one_loc_t, treiber);
   loc_t := one_loc_t->val;
-  call AllocTreiber(cell_t);
+  call AllocTreiber#0(cell_t);
   call {:layer 4} Stack := Copy(Map_Update(Stack, loc_t, Vec_Empty()));
   call {:layer 4} AbsLemma(treiber);
 }
@@ -46,22 +91,30 @@ preserves call YieldInvDom#4();
 atomic action {:layer 5} AtomicPush(loc_t: Loc (Treiber X), x: X) returns (success: bool)
 modifies Stack;
 {
-  if (success) {
+  if (*) {
     Stack := Map_Update(Stack, loc_t, Vec_Append(Map_At(Stack, loc_t), x));
+    success := true;
+  } else {
+    success := false;
   }
 }
 yield procedure {:layer 4} Push(loc_t: Loc (Treiber X), x: X) returns (success: bool)
 refines AtomicPush;
-preserves call YieldInv#2(loc_t);
-preserves call YieldInv#4(loc_t);
-preserves call YieldInvDom#4();
+preserves call TopInStack(loc_t);
+preserves call ReachInStack(loc_t);
+preserves call StackDom();
 {
+  var loc_n: Option (LocTreiberNode X);
+  var new_loc_n: LocTreiberNode X;
+  var {:linear} right_loc_piece: One (LocTreiberNode X);
   var {:layer 4} old_treiber: Treiber X;
 
   call {:layer 4} old_treiber := Copy(ts->val[loc_t]);
-  call success := PushIntermediate(loc_t, x);
+  call loc_n, new_loc_n, right_loc_piece := AllocNode#3(loc_t, x);
+  call {:layer 4} FrameLemma(old_treiber, ts->val[loc_t]);
+  par ReachInStack(loc_t) | StackDom() | PushLocInStack(loc_t, Node(loc_n, x), new_loc_n, right_loc_piece);
+  call success := WriteTopOfStack#0(loc_t, loc_n, Some(new_loc_n));
   if (success) {
-    call {:layer 4} FrameLemma(old_treiber, ts->val[loc_t]->stack);
     call {:layer 4} Stack := Copy(Map_Update(Stack, loc_t, Vec_Append(Map_At(Stack, loc_t), x)));
     assert {:layer 4} ts->val[loc_t]->top != None();
     call {:layer 4} AbsLemma(ts->val[loc_t]);
@@ -73,19 +126,21 @@ modifies Stack;
 {
   var stack: Vec X;
 
-  if (success) {
+  if (*) {
     stack := Map_At(Stack, loc_t);
     assume Vec_Len(stack) > 0;
     x := Vec_Nth(stack, Vec_Len(stack) - 1);
     Stack := Map_Update(Stack, loc_t, Vec_Remove(stack));
+    success := true;
+  } else {
+    success := false;
   }
 }
 yield procedure {:layer 4} Pop(loc_t: Loc (Treiber X)) returns (success: bool, x: X)
 refines AtomicPop;
-preserves call YieldInv#2(loc_t);
-preserves call YieldInv#3(loc_t);
-preserves call YieldInv#4(loc_t);
-preserves call YieldInvDom#4();
+preserves call TopInStack(loc_t);
+preserves call ReachInStack(loc_t);
+preserves call StackDom();
 {
   call {:layer 4} AbsLemma(ts->val[loc_t]);
   call success, x := PopIntermediate(loc_t);
@@ -95,6 +150,56 @@ preserves call YieldInvDom#4();
   }
 }
 
+atomic action {:layer 4} AtomicAllocNode#3(loc_t: Loc (Treiber X), x: X)
+  returns (loc_n: Option (LocTreiberNode X), new_loc_n: LocTreiberNode X, {:linear} right_loc_piece: One (LocTreiberNode X))
+modifies ts;
+{
+  var {:linear} one_loc_t: One (Loc (Treiber X));
+  var {:linear} treiber: Treiber X;
+  var top: Option (LocTreiberNode X);
+  var {:linear} stack: StackMap X;
+  var {:linear} one_loc_n: One (Loc (TreiberNode X));
+  var {:linear} cell_n: Cell (LocTreiberNode X) (StackElem X);
+  var {:linear} cell_t: Cell (Loc (Treiber X)) (Treiber X);
+  var {:linear} loc_pieces: Set (Fraction (Loc (TreiberNode X)) LocPiece);
+  var {:linear} left_loc_piece: One (Fraction (Loc (TreiberNode X)) LocPiece);
+  
+  call cell_t := Map_Get(ts, loc_t);
+  call one_loc_t, treiber := Cell_Unpack(cell_t);
+  Treiber(top, stack) := treiber;
+  assume loc_n is None || Map_Contains(stack, loc_n->t);
+  call one_loc_n := One_New();
+  call loc_pieces := One_To_Fractions(one_loc_n, AllLocPieces);
+  call left_loc_piece := One_Get(loc_pieces, Fraction(one_loc_n->val, Left(), AllLocPieces));
+  new_loc_n := left_loc_piece->val;
+  call right_loc_piece := One_Get(loc_pieces, Fraction(one_loc_n->val, Right(), AllLocPieces));
+  call cell_n := Cell_Pack(left_loc_piece, Node(loc_n, x));
+  call Map_Put(stack, cell_n);
+  treiber := Treiber(top, stack);
+  call cell_t := Cell_Pack(one_loc_t, treiber);
+  call Map_Put(ts, cell_t);
+}
+yield procedure {:layer 3} AllocNode#3(loc_t: Loc (Treiber X), x: X)
+  returns (loc_n: Option (LocTreiberNode X), new_loc_n: LocTreiberNode X, {:linear} right_loc_piece: One (LocTreiberNode X))
+preserves call TopInStack(loc_t);
+ensures call LocInStack(loc_t, Some(new_loc_n));
+refines AtomicAllocNode#3;
+{
+  var {:linear} one_loc_n: One (Loc (TreiberNode X));
+  var {:linear} cell_n: Cell (LocTreiberNode X) (StackElem X);
+  var {:linear} loc_pieces: Set (Fraction (Loc (TreiberNode X)) LocPiece);
+  var {:linear} left_loc_piece: One (Fraction (Loc (TreiberNode X)) LocPiece);
+
+  call loc_n := ReadTopOfStack#2(loc_t);
+  call one_loc_n := One_New();
+  call loc_pieces := One_To_Fractions(one_loc_n, AllLocPieces);
+  call left_loc_piece := One_Get(loc_pieces, Fraction(one_loc_n->val, Left(), AllLocPieces));
+  new_loc_n := left_loc_piece->val;
+  call right_loc_piece := One_Get(loc_pieces, Fraction(one_loc_n->val, Right(), AllLocPieces));
+  call cell_n := Cell_Pack(left_loc_piece, Node(loc_n, x));
+  call AllocNode#0(loc_t, cell_n);
+}
+
 atomic action {:layer 4} AtomicPopIntermediate(loc_t: Loc (Treiber X)) returns (success: bool, x: X)
 modifies ts;
 {
@@ -105,7 +210,7 @@ modifies ts;
   var {:linear} stack: StackMap X;
   var {:linear} cell_t: Cell (Loc (Treiber X)) (Treiber X);
 
-  assume Map_Contains(ts, loc_t);
+  assert Map_Contains(ts, loc_t);
   if (success) {
     call cell_t := Map_Get(ts, loc_t);
     call one_loc_t, treiber := Cell_Unpack(cell_t);
@@ -120,135 +225,48 @@ modifies ts;
 }
 yield procedure {:layer 3} PopIntermediate(loc_t: Loc (Treiber X)) returns (success: bool, x: X)
 refines AtomicPopIntermediate;
-preserves call YieldInv#2(loc_t);
-preserves call YieldInv#3(loc_t);
+preserves call TopInStack(loc_t);
 {
   var loc_n, new_loc_n: Option (LocTreiberNode X);
   var node: StackElem X;
 
   success := false;
-  call loc_n := ReadTopOfStack#Pop(loc_t);
+  call loc_n := ReadTopOfStack#2(loc_t);
   if (loc_n == None()) {
     return;
   }
-  call node := LoadNode(loc_t, loc_n->t);
+  par LocInStack(loc_t, loc_n) | TopInStack(loc_t);
+  call node := LoadNode#0(loc_t, loc_n->t);
+  call Yield();
   Node(new_loc_n, x) := node;
-  call success := WriteTopOfStack#Pop(loc_t, loc_n, new_loc_n);
-}
-
-atomic action {:layer 3, 4} AtomicPushIntermediate(loc_t: Loc (Treiber X), x: X) returns (success: bool)
-modifies ts;
-{
-  var {:linear} one_loc_t: One (Loc (Treiber X));
-  var {:linear} treiber: Treiber X;
-  var top: Option (LocTreiberNode X);
-  var {:linear} stack: StackMap X;
-  var {:linear} one_loc_n: One (LocTreiberNode X);
-  var {:linear} cell_n: Cell (LocTreiberNode X) (StackElem X);
-  var {:linear} cell_t: Cell (Loc (Treiber X)) (Treiber X);
-
-  success := false;
-  if (*) {
-    success := true;
-    call cell_t := Map_Get(ts, loc_t);
-    call one_loc_t, treiber := Cell_Unpack(cell_t);
-    Treiber(top, stack) := treiber;
-    call one_loc_n := One_New();
-    call cell_n := Cell_Pack(one_loc_n, Node(top, x));
-    call Map_Put(stack, cell_n);
-    treiber := Treiber(Some(one_loc_n->val), stack);
-    call cell_t := Cell_Pack(one_loc_t, treiber);
-    call Map_Put(ts, cell_t);
-  }
+  call success := WriteTopOfStack#0(loc_t, loc_n, new_loc_n);
 }
-yield procedure {:layer 2} PushIntermediate(loc_t: Loc (Treiber X), x: X) returns (success: bool)
-refines AtomicPushIntermediate;
-preserves call YieldInv#2(loc_t);
-{
-  var loc_n: Option (LocTreiberNode X);
-  var new_loc_n: LocTreiberNode X;
-  var {:linear} one_loc_n: One (LocTreiberNode X);
-  var {:linear} cell_n: Cell (LocTreiberNode X) (StackElem X);
 
-  call loc_n := ReadTopOfStack#Push(loc_t);
-  call one_loc_n := One_New();
-  new_loc_n := one_loc_n->val;
-  call cell_n := Cell_Pack(one_loc_n, Node(loc_n, x));
-  call success := WriteTopOfStack(loc_t, loc_n, Some(new_loc_n));
-  if (success) {
-    call AllocNode(loc_t, cell_n);
-  }
-}
-
-right action {:layer 3} AtomicReadTopOfStack#Pop(loc_t: Loc (Treiber X)) returns (loc_n: Option (LocTreiberNode X))
+right action {:layer 3} AtomicReadTopOfStack#2(loc_t: Loc (Treiber X)) returns (loc_n: Option (LocTreiberNode X))
 {
   assert Map_Contains(ts, loc_t);
   assume loc_n is None || Set_Contains(Domain(ts, loc_t), loc_n->t);
 }
-yield procedure {:layer 2} ReadTopOfStack#Pop(loc_t: Loc (Treiber X)) returns (loc_n: Option (LocTreiberNode X))
-refines AtomicReadTopOfStack#Pop;
-preserves call YieldInv#2(loc_t);
+yield procedure {:layer 2} ReadTopOfStack#2(loc_t: Loc (Treiber X)) returns (loc_n: Option (LocTreiberNode X))
+preserves call TopInStack(loc_t);
+ensures call LocInStack(loc_t, loc_n);
+refines AtomicReadTopOfStack#2;
 {
-  call loc_n := ReadTopOfStack(loc_t);
+  call loc_n := ReadTopOfStack#0(loc_t);
 }
 
-right action {:layer 2} AtomicReadTopOfStack#Push(loc_t: Loc (Treiber X)) returns (loc_n: Option (LocTreiberNode X))
-{
-  assert Map_Contains(ts, loc_t);
-}
-yield procedure {:layer 1} ReadTopOfStack#Push(loc_t: Loc (Treiber X)) returns (loc_n: Option (LocTreiberNode X))
-refines AtomicReadTopOfStack#Push;
-{
-  call loc_n := ReadTopOfStack(loc_t);
-}
-
-right action {:layer 3} AtomicLoadNode(loc_t: Loc (Treiber X), loc_n: LocTreiberNode X) returns (node: StackElem X)
-modifies ts;
+right action {:layer 2,3} AtomicLoadNode#1(loc_t: Loc (Treiber X), loc_n: LocTreiberNode X) returns (node: StackElem X)
 {
   assert Map_Contains(ts, loc_t);
   assert Map_Contains(Map_At(ts, loc_t)->stack, loc_n);
   node := Map_At(Map_At(ts, loc_t)->stack, loc_n);
 }
-yield procedure {:layer 2} LoadNode(loc_t: Loc (Treiber X), loc_n: LocTreiberNode X) returns (node: StackElem X)
-refines AtomicLoadNode;
-preserves call YieldInv#2(loc_t);
-{
-  call node := LoadNode#0(loc_t, loc_n);
-}
-
-atomic action {:layer 3} AtomicWriteTopOfStack#Pop(
-  loc_t: Loc (Treiber X), old_loc_n: Option (LocTreiberNode X), new_loc_n: Option (LocTreiberNode X)) returns (r: bool)
-modifies ts;
-{
-  assert new_loc_n is None || Set_Contains(Domain(ts, loc_t), new_loc_n->t);
-  call r := AtomicWriteTopOfStack(loc_t, old_loc_n, new_loc_n);
-}
-yield procedure {:layer 2} WriteTopOfStack#Pop(
-  loc_t: Loc (Treiber X), old_loc_n: Option (LocTreiberNode X), new_loc_n: Option (LocTreiberNode X)) returns (r: bool)
-refines AtomicWriteTopOfStack#Pop;
-preserves call YieldInv#2(loc_t);
-{
-  call r := WriteTopOfStack(loc_t, old_loc_n, new_loc_n);
-}
 
-atomic action {:layer 1, 2} AtomicReadTopOfStack(loc_t: Loc (Treiber X)) returns (loc_n: Option (LocTreiberNode X))
-modifies ts;
-{
-  var {:linear} one_loc_t: One (Loc (Treiber X));
-  var {:linear} treiber: Treiber X;
-  var {:linear} cell_t: Cell (Loc (Treiber X)) (Treiber X);
-
-  call cell_t := Map_Get(ts, loc_t);
-  call one_loc_t, treiber := Cell_Unpack(cell_t);
-  loc_n := treiber->top;
-  call cell_t := Cell_Pack(one_loc_t, treiber);
-  call Map_Put(ts, cell_t);
-}
-yield procedure {:layer 0} ReadTopOfStack(loc_t: Loc (Treiber X)) returns (loc_n: Option (LocTreiberNode X));
-refines AtomicReadTopOfStack;
+/// Primitives
 
-atomic action {:layer 1,2} AtomicLoadNode#0(loc_t: Loc (Treiber X), loc_n: LocTreiberNode X) returns (node: StackElem X)
+atomic action {:layer 1} AtomicLoadNode#0(loc_t: Loc (Treiber X), loc_n: LocTreiberNode X) returns (node: StackElem X)
 modifies ts;
+refines AtomicLoadNode#1;
 {
   var {:linear} one_loc_t: One (Loc (Treiber X));
   var {:linear} treiber: Treiber X;
@@ -261,7 +279,6 @@ modifies ts;
   call cell_t := Map_Get(ts, loc_t);
   call one_loc_t, treiber := Cell_Unpack(cell_t);
   Treiber(top, stack) := treiber;
-  assume Map_Contains(stack, loc_n); // problematic assume
   call cell_n := Map_Get(stack, loc_n);
   call one_loc_n, node := Cell_Unpack(cell_n);
   call cell_n := Cell_Pack(one_loc_n, node);
@@ -273,8 +290,7 @@ modifies ts;
 yield procedure {:layer 0} LoadNode#0(loc_t: Loc (Treiber X), loc_n: LocTreiberNode X) returns (node: StackElem X);
 refines AtomicLoadNode#0;
 
-left action {:layer 1, 2} AtomicAllocNode(
-  loc_t: Loc (Treiber X), {:linear_in} cell_n: Cell (LocTreiberNode X) (StackElem X))
+atomic action {:layer 1,2} AtomicReadTopOfStack#0(loc_t: Loc (Treiber X)) returns (loc_n: Option (LocTreiberNode X))
 modifies ts;
 {
   var {:linear} one_loc_t: One (Loc (Treiber X));
@@ -283,16 +299,15 @@ modifies ts;
 
   call cell_t := Map_Get(ts, loc_t);
   call one_loc_t, treiber := Cell_Unpack(cell_t);
-  call Map_Put(treiber->stack, cell_n);
+  loc_n := treiber->top;
   call cell_t := Cell_Pack(one_loc_t, treiber);
   call Map_Put(ts, cell_t);
 }
-yield procedure {:layer 0} AllocNode(
-  loc_t: Loc (Treiber X), {:linear_in} cell_n: Cell (LocTreiberNode X) (StackElem X));
-refines AtomicAllocNode;
+yield procedure {:layer 0} ReadTopOfStack#0(loc_t: Loc (Treiber X)) returns (loc_n: Option (LocTreiberNode X));
+refines AtomicReadTopOfStack#0;
 
-atomic action {:layer 1, 3} AtomicWriteTopOfStack(
-  loc_t: Loc (Treiber X), old_loc_n: Option (LocTreiberNode X), new_loc_n: Option (LocTreiberNode X)) returns (r: bool)
+atomic action {:layer 1,4} AtomicWriteTopOfStack#0(
+  loc_t: Loc (Treiber X), old_loc_n: Option (LocTreiberNode X), new_loc_n: Option (LocTreiberNode X)) returns (success: bool)
 modifies ts;
 {
   var {:linear} treiber: Treiber X;
@@ -303,53 +318,45 @@ modifies ts;
   call one_loc_t, treiber := Cell_Unpack(cell_t);
   if (old_loc_n == treiber->top) {
     treiber->top := new_loc_n;
-    r := true;
+    success := true;
   } else {
-    r := false;
+    success := false;
   }
   call cell_t := Cell_Pack(one_loc_t, treiber);
   call Map_Put(ts, cell_t);
 }
-yield procedure {:layer 0} WriteTopOfStack(
-  loc_t: Loc (Treiber X), old_loc_n: Option (LocTreiberNode X), new_loc_n: Option (LocTreiberNode X)) returns (r: bool);
-refines AtomicWriteTopOfStack;
+yield procedure {:layer 0} WriteTopOfStack#0(
+  loc_t: Loc (Treiber X), old_loc_n: Option (LocTreiberNode X), new_loc_n: Option (LocTreiberNode X)) returns (success: bool);
+refines AtomicWriteTopOfStack#0;
 
-atomic action {:layer 1, 4} AtomicAllocTreiber({:linear_in} cell_t: Cell (Loc (Treiber X)) (Treiber X))
+atomic action {:layer 1,3} AtomicAllocNode#0(loc_t: Loc (Treiber X), {:linear_in} cell_n: Cell (LocTreiberNode X) (StackElem X))
 modifies ts;
 {
+  var {:linear} one_loc_t: One (Loc (Treiber X));
+  var {:linear} treiber: Treiber X;
+  var {:linear} cell_t: Cell (Loc (Treiber X)) (Treiber X);
+
+  call cell_t := Map_Get(ts, loc_t);
+  call one_loc_t, treiber := Cell_Unpack(cell_t);
+  call Map_Put(treiber->stack, cell_n);
+  call cell_t := Cell_Pack(one_loc_t, treiber);
   call Map_Put(ts, cell_t);
 }
-yield procedure {:layer 0} AllocTreiber({:linear_in} cell_t: Cell (Loc (Treiber X)) (Treiber X));
-refines AtomicAllocTreiber;
+yield procedure {:layer 0} AllocNode#0(loc_t: Loc (Treiber X), {:linear_in} cell_n: Cell (LocTreiberNode X) (StackElem X));
+refines AtomicAllocNode#0;
 
-function {:inline} Domain(ts: Map (Loc (Treiber X)) (Treiber X), loc_t: Loc (Treiber X)): Set (LocTreiberNode X) {
-  ts->val[loc_t]->stack->dom
+atomic action {:layer 1,4} AtomicAllocTreiber#0({:linear_in} cell_t: Cell (Loc (Treiber X)) (Treiber X))
+modifies ts;
+{
+  call Map_Put(ts, cell_t);
 }
+yield procedure {:layer 0} AllocTreiber#0({:linear_in} cell_t: Cell (Loc (Treiber X)) (Treiber X));
+refines AtomicAllocTreiber#0;
 
-yield invariant {:layer 2} YieldInv#2(loc_t: Loc (Treiber X));
-invariant Map_Contains(ts, loc_t);
-invariant (var loc_n := Map_At(ts, loc_t)->top; loc_n is None || Set_Contains(Domain(ts, loc_t), loc_n->t));
-
-yield invariant {:layer 3} YieldInv#3(loc_t: Loc (Treiber X));
-invariant Map_Contains(ts, loc_t);
-invariant (var loc_n := Map_At(ts, loc_t)->top; loc_n is None || Set_Contains(Domain(ts, loc_t), loc_n->t));
-invariant (forall loc_n: LocTreiberNode X ::
-              Set_Contains(Domain(ts, loc_t), loc_n) ==> 
-              (var loc_n' := Map_At(Map_At(ts, loc_t)->stack, loc_n)->next; 
-                    loc_n' is None || Set_Contains(Domain(ts, loc_t), loc_n'->t)));
-
-yield invariant {:layer 4} YieldInv#4(loc_t: Loc (Treiber X));
-invariant Map_Contains(ts, loc_t);
-invariant Map_At(Stack, loc_t) == Abs(Map_At(ts, loc_t));
-invariant (var t := ts->val[loc_t]; Between(t->stack->val, t->top, t->top, None()));
-invariant (var t := ts->val[loc_t]; IsSubset(BetweenSet(t->stack->val, t->top, None()), Domain(ts, loc_t)->val));
-
-yield invariant {:layer 4} YieldInvDom#4();
-invariant Stack->dom == ts->dom;
+/// Proof of abstraction with a manual encoding of termination
 
-// The following is a manual encoding of the termination proof for the abstraction.
+// Abs and AbsDefinition together model the abstraction function
 function Abs(treiber: Treiber X): Vec X;
-
 function {:inline} AbsDefinition(treiber: Treiber X): Vec X {
 if treiber->top == None() then
   Vec_Empty() else
@@ -358,11 +365,17 @@ if treiber->top == None() then
       Vec_Append(Abs(treiber'), n->val)))
 }
 
-pure procedure AbsCompute(treiber: Treiber X) returns (absStack: Vec X)
+pure procedure AbsCompute(treiber: Treiber X, treiber': Treiber X) returns (absStack: Vec X)
+requires treiber->top == treiber'->top;
+requires IsSubset(treiber->stack->dom->val, treiber'->stack->dom->val);
+requires MapIte(treiber->stack->dom->val, treiber->stack->val, MapConst(Default())) ==
+         MapIte(treiber->stack->dom->val, treiber'->stack->val, MapConst(Default()));
 requires Between(treiber->stack->val, treiber->top, treiber->top, None());
 requires IsSubset(BetweenSet(treiber->stack->val, treiber->top, None()), treiber->stack->dom->val);
 ensures absStack == AbsDefinition(treiber);
+ensures absStack == AbsDefinition(treiber');
 free ensures absStack == Abs(treiber);
+free ensures absStack == Abs(treiber');
 {
   var loc_n: Option (LocTreiberNode X);
   var n: StackElem X;
@@ -371,27 +384,36 @@ free ensures absStack == Abs(treiber);
       absStack := Vec_Empty();
   } else {
       loc_n := treiber->top;
-      assert Map_Contains(treiber->stack, loc_n->t); // soundness of framing
+      assert Map_Contains(treiber->stack, loc_n->t);
       n := Map_At(treiber->stack, loc_n->t);
-      assert Between(treiber->stack->val, loc_n, n->next, None()); // soundness of termination (for induction)
-      call absStack := AbsCompute(Treiber(n->next, treiber->stack));
+      // Use well-founded list reachability to prove that recursion will terminate:
+      // treiber@caller->top --> treiber@callee->top --> None()
+      assert Between(treiber->stack->val, loc_n, n->next, None());
+      call absStack := AbsCompute(Treiber(n->next, treiber->stack), Treiber(n->next, treiber'->stack));
       absStack := Vec_Append(absStack, n->val);
   }
 }
 
+/// Useful lemmas obtained by wrapping AbsCompute
+
 pure procedure AbsLemma(treiber: Treiber X)
 requires Between(treiber->stack->val, treiber->top, treiber->top, None());
 requires IsSubset(BetweenSet(treiber->stack->val, treiber->top, None()), treiber->stack->dom->val);
 ensures Abs(treiber) == AbsDefinition(treiber);
 {
   var absStack: Vec X;
-  call absStack := AbsCompute(treiber);
+  call absStack := AbsCompute(treiber, treiber);
 }
 
-pure procedure FrameLemma(treiber: Treiber X, map': StackMap X);
+pure procedure FrameLemma(treiber: Treiber X, treiber': Treiber X)
+requires treiber->top == treiber'->top;
+requires IsSubset(treiber->stack->dom->val, treiber'->stack->dom->val);
+requires MapIte(treiber->stack->dom->val, treiber->stack->val, MapConst(Default())) ==
+         MapIte(treiber->stack->dom->val, treiber'->stack->val, MapConst(Default()));
 requires Between(treiber->stack->val, treiber->top, treiber->top, None());
 requires IsSubset(BetweenSet(treiber->stack->val, treiber->top, None()), treiber->stack->dom->val);
-requires IsSubset(treiber->stack->dom->val, map'->dom->val);
-requires MapIte(treiber->stack->dom->val, treiber->stack->val, MapConst(Default())) == 
-         MapIte(treiber->stack->dom->val, map'->val, MapConst(Default()));
-ensures Abs(treiber) == Abs(Treiber(treiber->top, map'));
+ensures Abs(treiber) == Abs(treiber');
+{
+  var absStack: Vec X;
+  call absStack := AbsCompute(treiber, treiber');
+}
diff --git a/Test/civl/samples/treiber-stack.bpl.expect b/Test/civl/samples/treiber-stack.bpl.expect
index d3c7fab1e..b3847fc1a 100644
--- a/Test/civl/samples/treiber-stack.bpl.expect
+++ b/Test/civl/samples/treiber-stack.bpl.expect
@@ -1,2 +1,2 @@
 
-Boogie program verifier finished with 58 verified, 0 errors
+Boogie program verifier finished with 31 verified, 0 errors