Solver leaks timer threads accross reuse
The SAT solver uses the java.util.Timer class to stop the solver after a given timeout.
boolean firstTimeGlobal = false;
if (this.timeBasedTimeout) {
if (!global || this.timer == null) {
if (this.timer != null) {
this.timer.cancel();
}
firstTimeGlobal = true;
this.undertimeout = true;
TimerTask stopMe = new TimerTask() {
@Override
public void run() {
Solver.this.undertimeout = false;
}
};
this.timer = new Timer(true);
this.timer.schedule(stopMe, this.timeout);
}
}
When calling several time the method isSatisfiable on a solver, the solver creates for each call a new timer thread, due to the Timer.schedule() method.
This is a big issue because a thread stack is created for each thread, thus quickly the solver is running out of memory in those conditions.