Chalice: Applied patch #6192

Patches the translation of "assert" statements, so that the meaning of "old" is preserved when the temporary copy of the heap is made for the exhale.

1 files changed, 1 insertions, 1 deletions

diff --git a/Chalice/src/Translator.scala b/Chalice/src/Translator.scala
index 72dbf9e4..6b85ed8a 100644
--- a/Chalice/src/Translator.scala
+++ b/Chalice/src/Translator.scala
@@ -301,7 +301,7 @@ class Translator {
         val tmpHeap = Boogie.NewBVar(HeapName, theap, true);

         val tmpMask = Boogie.NewBVar(MaskName, tmask, true); 

         val tmpCredits = Boogie.NewBVar(CreditsName, tcredits, true); 

-        val tmpTranslator = new ExpressionTranslator(List(tmpHeap._1.id, tmpMask._1.id, tmpCredits._1.id), currentClass);

+        val tmpTranslator = new ExpressionTranslator(List(tmpHeap._1.id, tmpMask._1.id, tmpCredits._1.id), List(etran.ChooseEtran(true).Heap, etran.ChooseEtran(true).Mask, etran.ChooseEtran(true).Credits), currentClass);        

         Comment("assert") ::

         // exhale e in a copy of the heap/mask/credits

         BLocal(tmpHeap._1) :: (tmpHeap._2 := VarExpr(HeapName)) ::