GitLab

Vitus Lam reported randpsl.test failing with:

-:17: (F(({{{(p0) | {[*0]}}:{{{(p1)}[*2]}[:*]}[*]:[*2]}[:*0..3]}[]-> (G(F(p1)))) & (G((!(p1)) | ((!(p2)) W (G(!(p0))))))))
Running [P0]: ../ikwiad -R3 -t '(F(({{{(p0) | {[*0]}}:{{{(p1)}[*2]}[:*]}[*]:[*2]}[:*0..3]}[]-> (G(F(p1)))) & (G((!(p1)) | ((!(p2)) W (G(!(p0))))))))' >'lcr-o0-rfpqTF'
Running [P1]: ../ikwiad -x -R3 -t '(F(({{{(p0) | {[*0]}}:{{{(p1)}[*2]}[:*]}[*]:[*2]}[:*0..3]}[]-> (G(F(p1)))) & (G((!(p1)) | ((!(p2)) W (G(!(p0))))))))' >'lcr-o1-TdrzQJ'
Running [N0]: ../ikwiad -R3 -t '(!(F(({{{(p0) | {[*0]}}:{{{(p1)}[*2]}[:*]}[*]:[*2]}[:*0..3]}[]-> (G(F(p1)))) & (G((!(p1)) | ((!(p2)) W (G(!(p0)))))))))' >'lcr-o0-W91t5N'
Running [N1]: ../ikwiad -x -R3 -t '(!(F(({{{(p0) | {[*0]}}:{{{(p1)}[*2]}[:*]}[*]:[*2]}[:*0..3]}[]-> (G(F(p1)))) & (G((!(p1)) | ((!(p2)) W (G(!(p0)))))))))' >'lcr-o1-GEQAIy'
Performing sanity checks and gathering statistics...
terminate called after throwing an instance of 'std::bad_alloc'
  what():  std::bad_alloc
./randpsl.test: line 32:  7714 Broken pipe             ../../bin/randltl -n -1 --tree-size 30 --seed 12 --psl a b c
      7715                       | ../../bin/ltlfilt -r --size-min 12 --unique
      7716 Done                    | ../../bin/ltlfilt -v --ltl -n 50
      7717 Done                    | tee formulas
      7718 Aborted                 (core dumped) | ../../bin/ltlcross '../ikwiad -R3 -t %f >%T' '../ikwiad -x -R3 -t %f >%T' -F - -f '{{(p1)}[*]:{(p3) && {{!(p1)} xor {!(p3)}}}}'

He runs in a 32-bit VM with 4GB of RAM.

This particular formula actually takes a lot of time to run through ltlcross (when it works), so after fixing the memory problem (if possible) we might want to skip this case to speedup the builds.