[klee-dev] Using newer versions of STP
daniel at zuster.org
Tue Jul 13 10:45:10 PDT 2010
Patch looks excellent, please commit!
One question, what does this do:
+ vc_setInterfaceFlags(vc, EXPRDELETE, 0);
It reads like it disable expression freeing, which sounds scary for
memory use. Can you add a comment if it is something subtle?
Would it make sense to push the STP guys to make a stable release,
which we could recommend to users? That would be one step in the
direction of killing off our internal STP copy.
On Fri, Jul 9, 2010 at 8:24 AM, Peter Collingbourne <peter at pcc.me.uk> 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