[klee-dev] Using newer versions of STP
c.cadar at imperial.ac.uk
Fri Jul 9 09:36:16 PDT 2010
Thanks, Peter. I think it's a very useful patch: it still allows us to
use the more stable internal STP, as well as more recent versions of
STP, including the svn one.
On 09/07/10 16:24, Peter Collingbourne wrote:
> Hi Daniel,
> Sorry for the slow response.
> On Thu, Apr 08, 2010 at 06:45:58PM -0700, Daniel Dunbar wrote:
>> Um, ignore this question, since you obviously attached a patch for
>> exactly this! :)
>> It would be cool if we could tweak the patch to use the internal STP
>> if --with-stp isn't specified, then we could go ahead and put it in
> I finally got round to doing this -- please see the attached patch.
> I'll commit this if OK.
>>> It should be possible for us to support both options,
>>> initially, which is nice for comparing the performance of them side by
>>> side. Do you have any hard numbers that show that the new STP is
>>> better, or by how much?
> On one particular benchmark, we experienced query runtimes of several
> hours with the old STP, and approx 12 minutes with the new STP (dual
> 2.0GHz machine, using CryptoMiniSat 2). I've attached a copy of the
> problematic query. If you would like a copy of the benchmark itself
> (it has a dependency on another library) I can try to do that.
More information about the klee-dev