Frank Schüssele

Compared the latest nightly build [#53](https://jenkins.sopranium.de/job/Ultimate/job/Ultimate%20Nightly/job/PR-591/53/) with the reference build [#302](https://jenkins.sopranium.de/job/Ultimate/job/Ultimate%20Nightly/job/dev/302/) of the reference branch. The following tests failed: * I_programs_regression_c_NutzTransformation02.c S_programs_regression_c_BlockEncodingV2AutomizerC-FP-MaxSaneBE.epf T_programs_regression_c_BlockEncodingV2AutomizerC.xml (de.uni_freiburg.informatik.ultimate.regressiontest.generic.RegressionTestSuite) * I_programs_regression_c_TestIntegerDivision01.c S_programs_regression_c_AutomizerC-BitvectorTranslation.epf T_programs_regression_c_AutomizerC.xml (de.uni_freiburg.informatik.ultimate.regressiontest.generic.RegressionTestSuite) Please...

I think it would be a good idea to merge this, to achieve syntactically more correct witnesses, with 9319baf by just ommiting the function calls (so the title is not...

This is expected. We can model the C-program by using mathematical and unbounded integers (integer translation), but then we loose the bitprecise information. Therefore we cannot handle bitwise precisely in...

This is not the correct setting, use `/instance/de.uni_freiburg.informatik.ultimate.plugins.generator.cacsl2boogietranslator/Use\ bitvectors\ instead\ of\ ints=true` instead.

Oh, yes, this requires to change some other settings as well. I think the best idea is just to load predefined settings (for example `examples/settings/default/automizer/svcomp-Reach-32bit-Automizer_Bitvector.epf`) and adapt them to your...

I just added an optimization to improve the performance of our verification on atomic functions. Most of the atomic function that are supported with this PR require pointers. So if...

If I remember correctly, we currently cannot handle bitvectors in the computation of ranking functions, which is however necessary in `LTLAutomizer` and `BuchiAutomizer`. The implementation of this feature would require...

Needs to be revised (after SV-COMP), because the format for YAML witnesses has changed and we also use a different parser.

What other specifications do you want do add? Ultimate already supports various specifications like overflows and memsafety. Checking them can be enabled in the cacsl2boogietranslator settings. Assertions for those specifications...

What exactly is needed here until we can merge it? There is now a python script that can convert settings (from epf to json). If I understand it correctly to...