Inconsistent results in Hoare triple checker

[martin-neuhaeusser]

Basic Info

• Version: 0.2.2-boogie-steps-59e45e1-m
• The configuration and the input files are hoare_triple_inconsistency.zip.
• Not urgent for us. I am just reporting it so that the issue is not forgotten.

Description

Running a verification on the command line utility (I presume the command line version that is built with default settings does not do expensive assertion checks) proves the LTL formula:

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

Running the same verification in Ultimate Automizer's debug UI (which presumably checks more assertions) results in the following assertion violation:

[2022-09-30 12:54:56,864 INFO  L198             ResultUtil]:   - ExceptionOrErrorResult: AssertionError: HoareTripleChecker results differ between SdHoareTripleChecker (result: INVALID) and MonolithicHoareTripleChecker (result: VALID)
[2022-09-30 12:54:56,864 INFO  L202             ResultUtil]:     de.uni_freiburg.informatik.ultimate.plugins.generator.buchiautomizer: AssertionError: HoareTripleChecker results differ between SdHoareTripleChecker (result: INVALID) and MonolithicHoareTripleChecker (result: VALID): de.uni_freiburg.informatik.ultimate.lib.modelcheckerutils.hoaretriple.ChainingHoareTripleChecker$ReviewedProtectedHtc.createAssertionError(ChainingHoareTripleChecker.java:391)

It seems that there is some inconsistency that is only detected by some internal assertions.

[Heizmann]

Thanks. It seems to me that this is an issue that I am working no with @maul-esel. If this is the case the issue does not affect soundness, but it affects the performance and lets Automizer do unnecessarily many iterations.