-
Regis Blanc authored
Fixes a bug, where UnrollingSolver was interrupted but was not stopping its internal solver, leading to a timeout not being respected if the internal solver was stucked in a complicated check operation. UnrollingSolver now takes a Solver with Interruptible. In order to do that, Leon now relies on a more recent version of scala-smtlib, that provides a feature to kill the solver process in a relatively clean way. Update the SMTLIBSolver code to actually perform the kill operation on the interrupt.
Regis Blanc authoredFixes a bug, where UnrollingSolver was interrupted but was not stopping its internal solver, leading to a timeout not being respected if the internal solver was stucked in a complicated check operation. UnrollingSolver now takes a Solver with Interruptible. In order to do that, Leon now relies on a more recent version of scala-smtlib, that provides a feature to kill the solver process in a relatively clean way. Update the SMTLIBSolver code to actually perform the kill operation on the interrupt.
SMTLIBSolver.scala 922 B