isolate1:
var x : t
action foo = {
...
call bar
invariant ...
if (x = ...) ....
}
action baz = {
x := ...
isolate2:
action bar = {
call baz