search

ultimate-pa / ultimate

The Ultimate program analysis framework.
https://ultimate-pa.org/
198 stars 41 forks source link

Ultimate crashes with OOM for array[8192] #414

Open invd opened 5 years ago

invd commented 5 years ago

When re-testing the code described in #366 with

settings with the newest Ultimate 6392f50fb9ff6daa998daa33f79eb2c3746cdafb, Ultimate subprocesses run into an out of memory condition:

 * Results from de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction:
  - ExceptionOrErrorResult: AssertionError: de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: External (cvc4 --incremental --print-success --lang smt --rewrite-divk)Received EOF on stdin. No stderr output.
    de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction: AssertionError: de.uni_freiburg.informatik.ultimate.logic.SMTLIBException: External (cvc4 --incremental --print-success --lang smt --rewrite-divk)Received EOF on stdin. No stderr output.: de.uni_freiburg.informatik.ultimate.plugins.generator.traceabstraction.singletracecheck.TraceCheck.<init>(TraceCheck.java:239)
RESULT: Ultimate could not prove your program: Toolchain returned no result.

machine dmesg:

java invoked oom-killer [...]
[...]
Out of memory: Kill process 3549 (cvc4) score 685 or sacrifice child
Killed process 3549 (cvc4) total-vm:14672728kB, anon-rss:13832536kB, file-rss:0kB, shmem-rss:0kB
oom_reaper: reaped process 3549 (cvc4), now anon-rss:0kB, file-rss:0kB, shmem-rss:0kB

This happens on the previously described research VM with generous amounts of free RAM.

danieldietsch commented 5 years ago

see #415: probably the same reason, just a different symptom

invd commented 5 years ago

For cf7845638a016090978a13501adca3f0b2bbcea4 and AutomizerReach.xml, Ultimate still runs into an OOM (for the cvc4 subprocess), so this issue is likely unresolved as well.