[klee-dev] STP solver looping indefinitely
daniel at zuster.org
Wed Oct 14 16:14:37 PDT 2009
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
Otherwise it might be worth sending the query to Vijay, he may have a
On Wed, Oct 14, 2009 at 3:01 PM, Seungbeom Kim <sbkim at stanford.edu> wrote:
> On a particular machine I use (cluestick), the STP solver has been
> timing out frequently, even with a long timeout such as 10 minutes.
> An investigation into this problem reveals that the 'for (;;)' loop
> in MINISAT::Solver::search, located in $KLEE_ROOT/stp/sat/Solver.C,
> loops indefinitely--I observed a count of >300k during >10 minutes.
> This doesn't certainly look normal, does it? A peculiar thing about
> this is that it happens only on that machine, and not the other one
> that I mainly use (bohr). It didn't happen at first, but started to
> happen several months ago.
> Please let me know if you have any idea why this is happening and/or
> how I can fix this.
> Seungbeom Kim
> klee-dev mailing list
> klee-dev at keeda.stanford.edu
More information about the klee-dev