From cd500f3653905b029cf019a8709433c90df03fe1 Mon Sep 17 00:00:00 2001
From: qadeer <unknown>
Date: Thu, 23 Jan 2014 10:38:58 -0800
Subject: more cleanup

---
 Test/og/multiset.bpl | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'Test')

diff --git a/Test/og/multiset.bpl b/Test/og/multiset.bpl
index 55c87924..047d25a6 100644
--- a/Test/og/multiset.bpl
+++ b/Test/og/multiset.bpl
@@ -139,6 +139,7 @@ ensures {:right 1}  |{ A: assert tidIn != nil && tidIn != done;
         invariant {:phase 1} tidTmp != nil && tidTmp != done;
         invariant {:phase 1} tidTmp == tidIn;
         invariant {:phase 1} Inv(valid, elt, owner);
+	invariant {:phase 1} 0 <= j;
 	{
                 par Yield1();
 
@@ -319,6 +320,7 @@ ensures {:atomic 2}  |{ A: assert tidIn != nil && tidIn != done;
         invariant {:phase 1} {:phase 2} Inv(valid, elt, owner);
         invariant {:phase 1} {:phase 2} (forall ii:int :: 0 <= ii && ii < j ==> !(old_valid[ii] && old_elt[ii] == x));
 	invariant {:phase 1} {:phase 2} (forall ii:int :: 0 <= ii && ii < max && old_valid[ii] ==> valid[ii] && old_elt[ii] == elt[ii]);
+	invariant {:phase 1} {:phase 2} 0 <= j;
 	{
                 par Yield12() | YieldLookUp(old_valid, old_elt);
 
-- 
cgit v1.2.3