Since the translator must look for aliases in the path condition, it might return an expression that is no longer valid at the program point due to reassignment/modification. The path condition never drops information; the information becomes inaccessible to the verifier except for during translation. This is a tricky problem, because the Translator's functionality needs to operate on aliases in the path condition and it cannot rely on accessibility predicates on the H or OH to indicate whether to translate something in the PC or not (thanks to imprecision). So, the best solution is to start removing information from the path condition where necessary in consume or mark certain information in the path condition as to be ignored by the Translator in the consume function. This is a wide-sweeping change that needs time to be explored for correctness.
Additionally, it appears that non of our current benchmarks experience this issue, because when it happens a shorter (in terms of path dereferences), correct expression is produced along the incorrect one, and so the correct one is always given back instead of the incorrect one by the Translator. In practice the incorrect expression being given back may not happen often, but it definitely can and so this design/implementation change should be addressed.
Since the translator must look for aliases in the path condition, it might return an expression that is no longer valid at the program point due to reassignment/modification. The path condition never drops information; the information becomes inaccessible to the verifier except for during translation. This is a tricky problem, because the Translator's functionality needs to operate on aliases in the path condition and it cannot rely on accessibility predicates on the H or OH to indicate whether to translate something in the PC or not (thanks to imprecision). So, the best solution is to start removing information from the path condition where necessary in consume or mark certain information in the path condition as to be ignored by the Translator in the consume function. This is a wide-sweeping change that needs time to be explored for correctness.
Additionally, it appears that non of our current benchmarks experience this issue, because when it happens a shorter (in terms of path dereferences), correct expression is produced along the incorrect one, and so the correct one is always given back instead of the incorrect one by the Translator. In practice the incorrect expression being given back may not happen often, but it definitely can and so this design/implementation change should be addressed.