Hi Sergey, Although this is only a guess, my guess is that this is because KLEE is worklist-based, where an item in the worklist represents an execution state. The executor (Executor class) has a field searcher, whose runtime type determines the kind of exploration strategy used by KLEE. Executor::run calls searcher->selectState() to get the worklist item (program state) to symbolically execute. In case of depth-first search, the item returned by selectState() is just the last item added into the worklist (see the implementation in DFSSearcher class), other strategy may return different item. The point here, is that KLEE's path exploration may not necessarily use depth-first strategy, so it may not be correct to reuse the solving environment when switching between different worklist items.
Best, Andrew On Sunday, 24 July 2016, 23:17, Sergey Mechtaev <mecht...@gmail.com> wrote: 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 klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev