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 <[email protected]> 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 > >
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
