From 1e0f2b1ea7e9cbfd1c7923674c0ed4601263d09a Mon Sep 17 00:00:00 2001
From: Shaz Qadeer <qadeer@microsoft.com>
Date: Tue, 26 Jan 2016 10:11:24 -0800
Subject: another fix

---
 Test/civl/treiber-stack.bpl | 2 --
 1 file changed, 2 deletions(-)

diff --git a/Test/civl/treiber-stack.bpl b/Test/civl/treiber-stack.bpl
index 64e01c99..a184886d 100644
--- a/Test/civl/treiber-stack.bpl
+++ b/Test/civl/treiber-stack.bpl
@@ -80,7 +80,6 @@ ensures {:atomic} |{ A: Stack := Add(Stack, x, TopOfStack); TopOfStack := x; ret
     call t_lmap := Store(t_lmap, x, t);
     call g, t_lmap := TransferToStack(t, x, t_lmap); 
     if (g) {
-      assert {:layer 1} map(Stack)[x] == t;
       break;
     }
     yield; 
@@ -124,7 +123,6 @@ function Subset([int]bool, [int]bool) returns (bool);
 
 function Empty() returns ([int]bool);
 function Singleton(int) returns ([int]bool);
-function Reachable([int,int]bool, int) returns ([int]bool);
 function Union([int]bool, [int]bool) returns ([int]bool);
 
 axiom(forall x:int :: !Empty()[x]);
-- 
cgit v1.2.3