Incorrect Büchi program while using LTLAutomizerCInline toolchain

[jjoojjoo123]

I've tried some C programs with LTL property using LTLAutomizerC.xml and LTLAutomizerCInline.xml with jungvisualization plugin. However, the resulting Büchi program is not correctly generated while using LTLAutomizerCInline.xml toolchain, i.e. with Boogie procedureinliner plugin. The never claim automaton states do not appear in any states of the resulting Büchi program, so the LTL property is always satisfied whatever the input program and the property are. This issue is also mentioned in the update of #508. Thanks.

[danieldietsch]

You are right, Ill look into it, but it might take some time because of deadlines ,)

Is this time-critical for you?

[jjoojjoo123]

Probably yes. We want to do something with concurrent C program and LTL simultaneously, which requires the correct Büchi program product. In addition, the product generator seems not to recognize the thread related edges of RCFG. Will this take a lot of work ? Thank you so much.

[Langenfeld]

The problem is, that the product generator ignores everything, that is of the ULTIMATE.start or .init functions. The inliner seems to set these functions for all the statements, that are inlined, thus they are ignored.

The good news is, that we fixed the several errors in the non-inlined ltl checking, so that might solve the problem, just try #566.

[danieldietsch]

Adding support for multi-threaded programs is hard for numerous reasons. It wont be done quickly, but possibly this year.