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? Otherwise it might be worth sending the query to Vijay, he may have a better idea. - Daniel On Wed, Oct 14, 2009 at 3:01 PM, Seungbeom Kim <sbkim at stanford.edu> wrote: > Hello, > > 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 > http://keeda.Stanford.EDU/mailman/listinfo/klee-dev >
