search

PatrickTrentin88 / fzn2omt

Tools/Scripts to convert MiniZinc/FlatZinc to Optimization Modulo Theories (OMT) for BCLT, OptiMathSAT or Z3 and Satisfiability Modulo Theories (SMT) for CVC4.
8 stars 0 forks source link

Solver keeps running after timeout #12

Open GustavBjordal opened 4 years ago

GustavBjordal commented 4 years ago

This might be hard to reproduce, but I am experiencing an issue where optimathsat keep running after the given time limit.

So after running minizinc --solver optimathsat_int --time-limit 10000 hardToSatisfy.mzn, where hardToSatisfy.mzn is some hard-to-satisfy model, the optimathsat process keeps on running in the background. I am guessing the python script might not send the termination signal to optimathsat?

I am running on ubuntu 16.

PatrickTrentin88 commented 4 years ago

The reason is that there is no such option, neither in OptiMathSAT nor in fzn2omt.

In the case that that you look for a workaround, you may want to use the timeout command in linux with SIGKILL and not SIGINT.

I am keeping this issue open as a reminder to address it.