Hello, The latest version of STP is a significant improvement over the older version that we are using. For example, it can use a much more efficient SAT solver called CryptoMiniSat.
I think it would be ideal to be able to use an external unmodified installation of STP. That way we can easily integrate new versions of STP as they are developed. I am working with the STP developers to try to get STP into a state where Klee can use it unmodified. I am undecided as to whether we should continue to include our own version of STP with Klee. I imagine this would make things easier for users but OTOH it could encourage divergence from upstream STP making it harder to integrate new versions. The recent changes to Klee to integrate STP into the LLVM build system may make this harder to do, due to certain paths and filenames having changed. I have had success integrating a recent version of STP and having it pass the tests. I am attaching a patch which replaces the in-tree version of STP with an out-of-tree version installed at a path specified at configure time (please note the instructions for applying the patch, supplied inline). If you want to make this work please note that it depends on a patch to STP [1] which has not yet been applied. [1] http://groups.google.com/group/stp-users/t/3eaeac520cbd5978 Thanks, -- Peter -------------- next part -------------- A non-text attachment was scrubbed... Name: 0001-Use-an-external-version-of-STP.patch Type: text/x-diff Size: 0 bytes Desc: not available Url : http://keeda.Stanford.EDU/pipermail/klee-dev/attachments/20100408/bbb6c5cd/attachment.bin
