Hi, I found that the version from SV-Comp 26 classifies this program as terminating:
int high = 5;
int low = -5;
int high_or_low(int x) {
if (x >= 0)
return high;
else
return low;
}
int safe_mul(int x, int y) {
if (y < -4 || y > 4)
return 0;
else
return x * y;
}
int some_division(int dividend, int divisor) {
if (dividend == low)
return 0;
else
return -1 / divisor;
}
int main() {
int x = 1;
int one = 1;
while (safe_mul(one, high_or_low(x)) > 0 && one >= 0) {
x--;
if (1)
some_division(some_division(-1, one), -1);
}
while (1)
;
}
This should be a non-terminating program, the first loop body should never be executed as the LHS of the conjunction is false for the initial values. I could also achieve the same result using the web interface.
Basic Info
- Version: 00d4337
- Java version: openjdk 21.0.10 2026-01-20
- Command:
"/home/UAutomizer-linux/Ultimate.py" "--spec" "termination.prp" "--file" test.c "--full-output" "--architecture" "64bit"
Hi, I found that the version from SV-Comp 26 classifies this program as terminating:
This should be a non-terminating program, the first loop body should never be executed as the LHS of the conjunction is false for the initial values. I could also achieve the same result using the web interface.
Basic Info
"/home/UAutomizer-linux/Ultimate.py" "--spec" "termination.prp" "--file" test.c "--full-output" "--architecture" "64bit"