A bug in checking undefined behavior

[mchalupa]

Symbiotic reports false(def-behavior) for this program

int main() {
        int array1[1];
        int count;
        for(count=0;count<1;count++)        {
                array1[count] = 0;
        }
}

The command: symbiotic/bin/symbiotic --sv-comp --prp undefined --save-files --no-slice program.c Symbiotic version: SV-COMP 2022 (the official archive)

[MichalHe]

This program probably triggers the same bug - undefined behavior is reported.

int main() {
    int c = 0;
    int arr[1];
    arr[c] = 42;
    return 0;
}