[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

-------------- next part --------------
HTML attachment scrubbed and removed