From 98314f3813388c7d74d7452042b0c6707a194e54 Mon Sep 17 00:00:00 2001
From: stefanheule <unknown>
Date: Sat, 25 Feb 2012 03:19:14 -0800
Subject: Chalice: ordering of picking a new version and checking against

---
 Chalice/src/main/scala/Translator.scala | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

diff --git a/Chalice/src/main/scala/Translator.scala b/Chalice/src/main/scala/Translator.scala
index dd5e02e2..f736c65a 100644
--- a/Chalice/src/main/scala/Translator.scala
+++ b/Chalice/src/main/scala/Translator.scala
@@ -2215,6 +2215,15 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F
         // transfer permission to secondary mask if necessary
         (if (transferPermissionToSecMask) InhalePermission(perm, trE, memberName, currentK, sm)
         else Nil) :::
+        // give up secondary permission to locations of the body of the predicate (also recursively)
+        (if (e.isPredicate)
+          (if (isUpdatingSecMask)
+            UpdateSecMask(e.predicate, trE, Heap.select(trE, memberName), perm, currentK, recurseOnPredicatesDepth, previousReceivers)
+          else
+            UpdateSecMask(e.predicate, trE, Heap.select(trE, memberName), perm, currentK)
+          )
+        else Nil) :::
+        // update version number (if necessary)
         (if (e.isPredicate && !isUpdatingSecMask)
           Boogie.If(!CanRead(trE, memberName, m, sm), // if we cannot access the predicate anymore, then its version will be havoced
             (if (!duringUnfold) bassume(Heap.select(trE, memberName) < eh.select(trE, memberName)) :: Nil // assume that the predicate's version grows monotonically
@@ -2227,14 +2236,6 @@ class ExpressionTranslator(val globals: Globals, preGlobals: Globals, val fpi: F
             }),
             Nil) :: Nil
         else Nil) :::
-        // give up secondary permission to locations of the body of the predicate (also recursively)
-        (if (e.isPredicate)
-          (if (isUpdatingSecMask)
-            UpdateSecMask(e.predicate, trE, Heap.select(trE, memberName), perm, currentK, recurseOnPredicatesDepth, previousReceivers)
-          else
-            UpdateSecMask(e.predicate, trE, Heap.select(trE, memberName), perm, currentK)
-          )
-        else Nil) :::
         bassume(AreGoodMasks(m, sm)) ::
         bassume(wf(Heap, m, sm))
       }
-- 
cgit v1.2.3