[klee-dev] STP solver looping indefinitely
sbkim at stanford.edu
Wed Oct 14 15:01:57 PDT 2009
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.
More information about the klee-dev