[klee-dev] klee crash question

[Vijay Ganesh]

On Tue, Dec 18, 2012 at 5:35 PM, Stefan Bucur <stefan.bucur at gmail.com> wrote:
> Hi,
>
> In my experience, the crash happens because of a stack overflow in the STP
> solver, when converting a very large symbolic array into its bitvector
> representation (i.e., "bitblasting"). My workaround was to allow for an
> unlimited stack size -- you can run "ulimit -s unlimited" before executing
> Klee.

I was going to suggest the same thing. This is not an STP specific
problem, i.e., other solvers also have the same issue with such huge
arrays.

> However, even if Klee no longer crashes, such huge constraints are likely
> quite expensive, and the solver may get stuck in one of them (unless it
> times out...). A quick way to diagnose the problem is to find in the
> assembly.ll file generated by Klee the line of code where the large object
> was allocated, and see if you can manually tweak the source code to reduce
> its size. Klee provides this line in the warning message that you
> copy-pasted here.

I concur with this as well.

-Vijay Ganesh
U of Waterloo, Canada.