Unsound condition transformation

[xlauko]

Refinement does not consider side effects in reaching conditions. Recompilation of following code produces semantically inequivalent results:

#include <stdio.h>

int i;

void fizzbuzz() {
    int save = i;
    if (i % 3 == 0) {
        i = 4;
        printf("fizz");
    }

    if (i % 5 == 0) {
        printf("buzz");
    }

    if ((i % 3 != 0) && (i % 5 != 0)) {
        printf("%d", i);
    }
    i = save;
}

int main() {
    for (i = 1; i < 16; i++) {
        fizzbuzz();
        putchar('\n');
    }
}

[xlauko]

Rellic produces wrong result, not taking into account a possible change of i in between conditions:

unsigned int i = 0U;
unsigned char _str[5] = "fizz\000";
unsigned char _str_1[5] = "buzz\000";
unsigned char _str_2[3] = "%d\000";
void fizzbuzz();
unsigned int printf(unsigned char *arg0, ...);
unsigned int main();
unsigned int putchar(unsigned int arg0);
void fizzbuzz() {
    unsigned int var0;
    unsigned int val1;
    unsigned int val2;
    unsigned int val3;
    var0 = i;
    if (i % 3U == 0U) {
        i = 4U;
        val1 = printf(_str);
    } else {
        if (i % 5U != 0U) {
            val3 = printf(_str_2, i);
        }
    }
    if (i % 5U == 0U) {
        val2 = printf(_str_1);
    }
    i = var0;
    return;
}
unsigned int main() {
    unsigned int val0;
    unsigned int var1;
    var1 = 0U;
    i = 1U;
    while (16U > i)
        {
            fizzbuzz();
            val0 = putchar(10U);
            i = i + 1U;
        }
    if (16U <= i) {
        return var1;
    }
}