Update OptiMathSAT from 1.7.1 to 1.7.2 or 1.7.3

[kfriedberger]

There is a new version of OptiMathSAT, which does not bring anything new, except internal improvements. Normally, such an update would not be worth an issue. However, there is a regression and it should to be documented:

Problem

The JUnit test OptimizationTest#testSwitchingObjectives hangs with an unexpected high runtime (no result after 10min). The expected runtime is less than a second.

Steps for simpler reproduction

When reporting the regression to the developer team of OptiMathSAT, they gave useful hints how to extract traces for the API interaction. Setting a few options allows to dump either SMTLIB2 of even C code directly for using OptiMathSAT:

• debug.api_call_trace_filename=mathsat_trace.smt (or .c) sets the filename.
• debug.api_call_trace_dump_config=true adds some header into the file and provides the used options.
• debug.api_call_trace=NUMBER with:
  • 1: dump SMTLIB2 with global declarations (uses temporary symbols via declare-fun)
  • 2: dump C code
  • 3: dump SMTLIB2 with scoped declarations (uses let statements))

Those settings can be given to our (Opti)MathSAT bindings via the option solver.mathsat5.furtherOptions. The dump with number 3 provides an SMTLIB2 file (mathsat_trace_3.txt) that seems to directly cause the problem on commandline: bin/optimathsat -optimization=true mathsat_trace_3.txt

We reported this and now wait for the developers to provide a fixed version of OptiMathSAT.

[kfriedberger]

The same problem still appears with OptiMathSAT 1.7.3.