Problem unsatisfiable at -O1, solves at -O0 and -O2

[snicolai-blog]

MacOS 14.3.1 SCIP 8.1.0 installed via homebrew MiniZincIDE 2.8.3 using the default SCIP configuration

Using the file: taxes2.mzn.txt

If I open it and switch the solver to SCIP 8.1.0 then run the model at the default -O1, it will report unsatisfiable.

If I then switch the configuration to either -O0 or -O2 for SCIP, it will solve.

I have to quit (without saving the configuration) and restart the IDE to get back to the default configuration.

[a1880]

On my system (Windows 10, MiniZinc 2.8.3), SCIP 7.0.0 yields "UNSATISFIABLE" for -O0 and finds a solution for -O1 and -O2. CPLEX 12.10.0.0 finds solutions for all optimization levels within a couple of seconds. Gecode 6.3.0 does not terminate but runs longer than I was patient enough to wait.

[snicolai-blog]

With MiniZinc 2.8.5 and SCIP 9.0.1, this model now solves at -O0, -O1 and -O2.