Skip to content
Snippets Groups Projects
  • Regis Blanc's avatar
    ef3642c6
    unrolling solver correclty interrupts its solver · ef3642c6
    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.
    ef3642c6
    History
    unrolling solver correclty interrupts its solver
    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.
SMTLIBSolver.scala 922 B