[klee-dev] Question about CexCache Solver

[Jianxiong Gao]

I have encountered an error recently.



For the CexCache Solver, at line:

https://github.com/klee/klee/blob/a8bf1a78cd20d1c2608faeecc54369d95ceadde7/lib/Solver/CexCachingSolver.cpp#L326



The Assignment of ‘a’ is checked against NULL. However, the
getAssignment function that assigns value to ‘a’ might set ‘a’ to NULL
at line: https://github.com/klee/klee/blob/a8bf1a78cd20d1c2608faeecc54369d95ceadde7/lib/Solver/CexCachingSolver.cpp#L249

when the query is unsatisfiable.



Does that mean the CexCachingSolver::computeValue can be invoked only when
the query is satisfiable?

If not, what does the assertion want to achieve?



Thanks


On Thu, Apr 12, 2018 at 12:28 PM, Jianxiong Gao <gao2 at illinois.edu> wrote:

> I have encountered an error recently.
>
>
>
> For the CexCache Solver, at line:
>
> https://github.com/klee/klee/blob/a8bf1a78cd20d1c2608faeecc54369d95ceadde7/lib/Solver/CexCachingSolver.cpp#L326
>
>
>
> The Assignment of ‘a’ is checked against NULL. However, the getAssignment function that assigns value to ‘a’ might set ‘a’ to NULL at line: https://github.com/klee/klee/blob/a8bf1a78cd20d1c2608faeecc54369d95ceadde7/lib/Solver/CexCachingSolver.cpp#L249
>
> when the query is unsatisfiable.
>
>
>
> Does that mean the CexCachingSolver::computeValue can be invoked only
> when the query is satisfiable?
>
> If not, what does the assertion want to achieve?
>
>
>
> Thanks
>
>
-------------- next part --------------
HTML attachment scrubbed and removed