[klee-dev] KLEE fork failed

[Dan Liew]

On 27 March 2018 at 08:45, Sicco Verwer <s.e.verwer at tudelft.nl> wrote:
>
> Dear all,
>
> I am trying to run KLEE in my class on concolic execution. Some student get the following message after which KLEE quits, and I cannot seem to find the cause, or solution. Does anyone know?

Just to be explicitly clear. KLEE does not use concolic execution.
KLEE implements classical symbolic execution where by it stores every
path (and related state) in memory at the same time.
This gives KLEE a global view of feasible paths in the programs but
this approach can quickly lead to memory exhaustion.

The issues you're seeing points at memory exhaustion which is one of
the limitations of classical symbolic execution. Concolic execution
side steps this by not storing the execution state of every path it
discovers.

You could try using the Z3 solver instead of STP if you want to avoid
forking which might reduce some of the memory overhead.