[move-prover] Boogie exited with compilation errors when "--trace" is set

When the prover is run against several Move modules in the DPN with the option “—trace”, output.bpl cannot pass compilation. To reproduce the error, using the following command:

`move package -p diem-move/diem-framework/DPN/sources/ prove -t VASP -- —trace`

The output:

Error: [internal] boogie exited with compilation errors:
output.bpl(8284,62): Error: undeclared identifier: a
output.bpl(8290,66): Error: undeclared identifier: a
output.bpl(8427,62): Error: undeclared identifier: a
output.bpl(8433,66): Error: undeclared identifier: a
output.bpl(8450,70): Error: undeclared identifier: parent
output.bpl(8457,73): Error: undeclared identifier: parent
output.bpl(8463,78): Error: undeclared identifier: parent
output.bpl(8592,62): Error: undeclared identifier: a
output.bpl(8598,66): Error: undeclared identifier: a
output.bpl(8615,70): Error: undeclared identifier: parent
output.bpl(8622,73): Error: undeclared identifier: parent
output.bpl(8628,78): Error: undeclared identifier: parent
output.bpl(8950,63): Error: undeclared identifier: a
output.bpl(8956,67): Error: undeclared identifier: a
output.bpl(8973,71): Error: undeclared identifier: parent
....
37 name resolution errors detected in output.bpl

The following code in output.bpl triggers the compilation failure:

// assume Identical($t5, exists(a)) at ./sources/VASP.move:252:37+20
assume {:print "$at(46,10573,10593)"} true;
assume ($t5 == $ResourceExists($1_VASP_ChildVASP_$memory, a));

The Move code at ./sources/VASP.move:252:37+20:
ensures forall a: address : exists(a) == old(exists(a));