diff --git a/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.c b/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.c new file mode 100644 index 0000000000..39e3cbce49 --- /dev/null +++ b/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.c @@ -0,0 +1,6 @@ +int main() { + int i = 0; + while (i < 10) + i++; + return 0; +} diff --git a/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t b/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t new file mode 100644 index 0000000000..c46c468642 --- /dev/null +++ b/tests/regression/55-loop-unrolling/11-unrolled-loop-invariant.t @@ -0,0 +1,6 @@ + $ goblint --set lib.activated '[]' --set exp.unrolling-factor 5 --enable ana.int.interval --enable witness.yaml.enabled --set witness.yaml.entry-types '["location_invariant", "loop_invariant"]' 11-unrolled-loop-invariant.c + [Error] YAML witnesses are incompatible with syntactic loop unrolling (https://github.com/goblint/analyzer/pull/1370). + Fatal error: exception Failure("Option error") + [2] + +TODO: Fix loop unrolling with YAML witnesses: https://github.com/goblint/analyzer/pull/1370