[klee-dev] STP solver looping indefinitely
sbkim at stanford.edu
Thu Oct 15 01:31:27 PDT 2009
Daniel Dunbar wrote:
> Well, it's certainly possible that you are getting a query that is
> hard to solve. It's NP-hard, after all, so it doesn't take much work
> to find queries that will take days to solve.
> That said, if it only happens on one machine maybe something else is
> going on. What versions of gcc do the machines have? Maybe MINISAT is
> being miscompiled?
cluestick has gcc (GCC) 4.3.0 20080428 (Red Hat 4.3.0-8),
bohr has gcc (Debian 4.3.4-5) 4.3.4.
I don't think any of these are outdated enough to be suspected,
but how can I tell if one is causing the proble?
By the way, the Makefile is certainly broken -- running make from
$KLEE_ROOT doesn't recognize any changes in the source files in
$KLEE_ROOT/stp/AST, nor does running make from $KLEE_ROOT/stp.
Either you have to run "make clean" each time, or after changing
any source file you have to do "make" first in $KLEE_ROOT/stp/AST,
then in $KLEE_ROOT/stp, and then in $KLEE_ROOT.
> Otherwise it might be worth sending the query to Vijay, he may have a
> better idea.
I attached a query (printed from KLEE) that I saw more than once that
caused the indefinite loop. How can I feed this into the stand-alone
STP solver ($KLEE_ROOT/stp/bin/stp, I guess)? It seems to expect a
certain grammar that $KLEE_ROOT/stp/bin/stp doesn't accept directly.
And how can I reach Vijay? (Are you on this list? :D)
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
More information about the klee-dev