Missing variable values in counter-examples

[martin-neuhaeusser]

Basic Info

• Ultimate Automizer: Ultimate 0.2.2-boogie-steps-e0412b4-m
• An example *.bpl file, the toolchain and the configuration as well as a dump of stdout with the counter-example are here: counterexample_values.zip.

To reproduce

Ultimate -tc LTLAutomizer.xml -s LTLAutomizer.epf -i Obfuscated-erc20-transferfrom-succeed-normal.bpl

Description

In our configuration, counterexamples produced by Ultimate Automizer do not contain variable values, which makes them hard to understand.

[Heizmann]

I just commited a partial solution to dev that addresses this issue.
2b22b30
If the infinite execution is a fixpoint (state repeated infinitely often) we can now show that values of the stem (infinite execution is lasso shaped and consists of stem + loop).

[martin-neuhaeusser]

@Heizmann Many thanks for the fix!
I ran a couple of examples and it produces variable value annotations also in our setting.
That's really very much appreciated!

For now, we don't have liveness properties in production, so having values for the finite prefix is all we really need at the moment.