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
