Timeout on a small example program

[blizzard4591]

Dear Developers,

I tested an example program with Ultimate and ran into timeouts where I did not expect them.

The example program is:

extern void __VERIFIER_error();

typedef struct {
  float a[0];
  char i;
} b;
typedef struct {
  b c;
} d;
int e, g, h, a;
d f;
int main() {
  while (1) {
    e = !h && f.c.i;
    for (; a < 10; a++)
      f.c.a[a] = g;
    if (e)
      __VERIFIER_error();
  }
}

I called Ultimate with timeout -k 900s 960s nice -10 ./Ultimate.py --spec reach.prp --file example.c --full-output --architecture 32bit. Even longer timeouts also lead to timeout - but to me, it looks like there is a structural bug here, not a problem with program complexity - or what do you think?

[danieldietsch]

@Heizmann could you inspect this program? It seems to me that this might be due to quantifier elimination.

After the following lines (note the treesize of input 211123411353580 treesize of output 211106231484396) we get a lot of the famous ...QuantifierPusher]: Applying distributivity, recursing on 2 terms lines.

...
[2020-01-30 16:16:16,531 INFO  L377             Elim1Store]: Elim1 did not use preprocessing eliminated variable of array dimension 1, 0 stores, 1 select indices, 1 select index equivalence classes, 0 disjoint index pairs (out of 0 index pairs), introduced 1 new quantified variables, introduced 0 case distinctions, treesize of input 211123411353580 treesize of output 211106231484396
[2020-01-30 16:16:16,656 INFO  L319       QuantifierPusher]: Applying distributivity, recursing on 2 terms

I used ./run-ultimate.sh -tc config/AutomizerReach.xml -s config/svcomp-Reach-32bit-Automizer_Bitvector.epf -i test.c on Ultimate 0.1.25-f69c6ef.

[Heizmann]

@blizzard4591 Thanks for the example. I will have a look in the next days. If the problem is what Daniel mentioned, then I can solve the issue only after I found time to continue my work on the quantifier elimination.