On Thu, Mar 17, 2011 at 02:41:46PM +0800, zhaosspirit at sjtu.edu.cn wrote: > Dear all. > I am a beginner of klee. I'm confused that how klee cooperates > with STP, or what is the interface between them. when klee use STP as > a constraint solver, does it have any special files generated as the > input of STP? > I am very appreciate for your answer. Thank you!
Hi Zhao, KLEE links with STP directly and generates queries and extracts counterexamples using its C interface (see the header file in stp/c_interface/c_interface.h), so there are no intermediate files generated. Thanks, -- Peter
