Solver reSSAT starts to compute the upper and lower bounds after catching an interruption signal (e.g., timeout).
However, the underlying model counter might take a long time to derive the bounds.
An internal time limit for the model counter is desired.
Solver reSSAT starts to compute the upper and lower bounds after catching an interruption signal (e.g., timeout). However, the underlying model counter might take a long time to derive the bounds. An internal time limit for the model counter is desired.