Laurent Voisin - 2013-06-26

Dear Vlad, the layout of your expressions is not retained between the model and the prover. However, within the proving UI, a local pretty-printer is used to render expressions in a readable way. It seems that this tool is missing a kind of expressions you're using heavily.

Could you please provide more details about the structure of the expressions that have this issue (e.g., operators).