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

[rahxephon89]

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<VASP::ChildVASP>(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<ChildVASP>(a) == old(exists<ChildVASP>(a));