Bug: Ultimate fails to compute Hoare annotation due to inductivity violation

[bahnwaerter]

When running Ultimate Automizer (0.3.0-dev-8447f03 with OpenJDK 21.0.8) with Java assertions enabled on the input program-3dfs-sb17-program-20.c, the following error occurs in the FloydHoareValidityCheck during the computation of the Hoare annotation to output a YAML verification witness:

Transition L20651 call #t~ret2002.base, #t~ret2002.offset := Cy_GPIO_PortToAddr((if ~pin % 256 % 4294967296 <= 2147483647 then ~pin % 256 % 4294967296 else ~pin % 256 % 4294967296 - 4294967296) / 8 % 256); $Ultimate##0 not inductive
The Plugin de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction has thrown an exception:
java.lang.AssertionError: inductivity violated
	at de.uni_freiburg.informatik.ultimate.lib.proofs.floydhoare.FloydHoareValidityCheck.evaluateInductivityResult(FloydHoareValidityCheck.java:248)
	at de.uni_freiburg.informatik.ultimate.lib.proofs.floydhoare.FloydHoareValidityCheck.checkInductivity(FloydHoareValidityCheck.java:215)
	at de.uni_freiburg.informatik.ultimate.lib.proofs.floydhoare.FloydHoareValidityCheck.checkInductivity(FloydHoareValidityCheck.java:183)
	at de.uni_freiburg.informatik.ultimate.lib.proofs.floydhoare.FloydHoareValidityCheck.performCheck(FloydHoareValidityCheck.java:117)

It looks like there's a bug in the implementation of the program analysis or the computation of the Hoare annotation. It's very unlikely that the error lies in the program. Even if the C translation is faulty, it shouldn't have a major impact on this error, because the analysis takes place on the control flow graph. Therefore, it's of secondary importance here whether the control flow graph correctly represents the C program.

[maul-esel]

Thanks for reporting the bug. You are correct, regardless of the C translation or the program, such an assertion error definitely indicates a bug.

Could you provide the precise settings & toolchain you used, and perhaps the log file? With default settings, I am not able to reproduce the issue (I simply get - CounterExampleResult [Line: -1]: pointer dereference may fail).

[bahnwaerter]

I completely forgot to attach the settings. Thanks for the tip. Here's the toolchain and the settings file for Ultimate. The settings are based on our default SV-COMP settings for ReachSafety verification tasks. Java assertions also need to be enabled. If you're using Eclipse for running or debugging Ultimate, you can add the VM argument -ea to the run configuration. On the command line, you can add it to the -vmargs section in the *.ini launcher configuration file.