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