Inlining introduces syntax that is rejected by the Boogie Preprocessor

[martin-neuhaeusser]

Basic Info

• Version: Ultimate 0.2.2-boogie-steps-59e45e1-m (the LTL extensions should be irrelevant - should be reproducible with dev)
• The example is attached: inlining_syntax_error.zip.
• Not urgent, we stumbled across that issue only during debugging.
• That issue might be simple enough so that I can offer to fix it myself (but most likely only end of October/November).

Description

If we use one tool chain to inline and preprocess the file Obfuscated-erc20-transfer-revert-zero.bpl, everything works as expected:

Ultimate -tc DoBoth.xml -s LTLAutomizer.epf -i Obfuscated-erc20-transfer-revert-zero.bpl

If we inline the example file and print out the result (which is in file Obfuscated-erc20-transfer-revert-zero_inlined.bpl), that Boogie file contains annotations that are rejected by the Boogie Preprocessor.

Ultimate -tc PreprocessOnly.xml -s LTLAutomizer.epf -i Obfuscated-erc20-transfer-revert-zero_inlined.bpl

In essence, the two type synonyms

type Ref = int;
type ContractName = int;

are rewritten during inlining to the following:

type finite Ref = int;
type finite ContractName = int;

I do not really understand why this is happening and doubt that it is correct (int is not finite). In any case, that syntax is rejected if we try to process the inlined Boogie file.
Interestingly, that issue does not occur if we combine inlining and the Boogie processor in a single toolchain.

The exception that is thrown once the Boogie Preprocessor attempts to read the inlined file is:

[2022-09-30 13:08:22,995 INFO  L94    rkbenchWindowAdvisor]: This is Ultimate GUI 0.2.2-boogie-steps-59e45e1-m
[2022-09-30 13:08:26,950 INFO  L75    nceAwareModelManager]: Repository-Root is: /tmp
[2022-09-30 13:08:26,979 INFO  L261   ainManager$Toolchain]: [Toolchain 1]: Applicable parser(s) successfully (re)initialized
[2022-09-30 13:08:30,808 INFO  L130   AnalysisChooseDialog]: Saved custom toolchain to /tmp/lastUltimateToolchain.xml
[2022-09-30 13:08:30,811 INFO  L217   ainManager$Toolchain]: [Toolchain 1]: Toolchain selected.
[2022-09-30 13:08:30,812 INFO  L271        PluginConnector]: Initializing Boogie PL CUP Parser...
[2022-09-30 13:08:30,816 INFO  L275        PluginConnector]: Boogie PL CUP Parser initialized
[2022-09-30 13:08:30,817 INFO  L432   ainManager$Toolchain]: [Toolchain 1]: Parsing single file: /home/marneu/certik/model_checking/freiburg/questions/duplicate_location_names/Obfuscated-erc20-transfer-revert-zero_inlined.bpl
[2022-09-30 13:08:30,817 INFO  L110           BoogieParser]: Parsing: '/home/marneu/certik/model_checking/freiburg/questions/duplicate_location_names/Obfuscated-erc20-transfer-revert-zero_inlined.bpl'
[2022-09-30 13:08:30,829 ERROR L748                 Parser]: /home/marneu/certik/model_checking/freiburg/questions/duplicate_location_names/Obfuscated-erc20-transfer-revert-zero_inlined.bpl:7:16: syntax error
[2022-09-30 13:08:30,831 ERROR L748                 Parser]: /home/marneu/certik/model_checking/freiburg/questions/duplicate_location_names/Obfuscated-erc20-transfer-revert-zero_inlined.bpl:8:25: syntax error