Some questions about BuchiAutomizer

[WHITE000CHOCOLATE]

Excuse me, I encounter some questions while running the BuchiAutomizer module. I found that in this part of the code, a lasso program may contain an if-branch (encoded as a ParallelComposition). But in the definition of lasso program, if-branches are not allowed. What if I want to focus on such lasso programs that contain only statements executed in strict order, such as assignment statements and assume statements, and does not contain if-branches? Or what can be done with these lasso programs? Thank you very much!

[Heizmann]

The problem here is that the large block encoding is enabled. The solution is to disable it.

• If you load your settings from a file you could add the following line /instance/de.uni_freiburg.informatik.ultimate.plugins.generator.rcfgbuilder/Size\ of\ a\ code\ block=SequenceOfStatements
• A (maybe better) alternative would be to our default preference file for the SV-COMP located at trunk/examples/settings/default/automizer/svcomp-Termination-64bit-Automizer_Default.epf
• If you use the GUI you will find the setting at Ultimate Preferences > Tool Plugins > RCFGBuilder > Size of a code block and you should set this to SequenceOfStatements.

[WHITE000CHOCOLATE]

Oh I handle it by loading the default setting file according to the second solution. Thank you so much!!!