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
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
