The semantics of old expression in Boogie

Nov 1, 2013 at 2:35 PM
Hi,
Suppose $Heap is a global variable, storing a global heap, and other variables are local.
I have the following code segment:
   $PreThreadHeap0 := $Heap;
    // ----- call statement ----- C:\Docs\Examples\cell.dfy(191,6)
    assert i#11 != null;
    assume true;
    l##42 := 2;
    call _module.Interval.setLeft(i#11, l##42);
    assume {:captureState "C:\Docs\Examples\cell.dfy(191,6)"} true;
    assert old($Heap) == $PreThreadHeap0;
I think the state(or heap) is updated by "call _module.Interval.setLeft(i#11, l##42);", then I can use an old expression to get the old state(or heap). However the assertion "old($Heap) == $PreThreadHeap0" failed.

I appreciate explanations.

Thanks
Yuyan