[klee-dev] Solving path constraints incrementally

[Sergey Mechtaev]

Hello,

It seems like KLEE does not use SMT solver incrementality when solving path
conditions. Specifically, I refer to the
STPSolverImpl::computeInitialValues that asserts all clauses from the query
and, after solving, removes them using pop. However, since KLEE explicitly
maintains execution states, I expected that it would reuse previous solving
environment in subsequent queries. I didn't manage to find any explanation
of this design choice in the KLEE publications.

Can you please tell me if my understanding is correct? What was the
motivation behind this choice?

Regards,
Sergey Mechtaev
-------------- next part --------------
HTML attachment scrubbed and removed