[BUG] Wrong solution on evm-super-compilation (only in parallel mode)

[ptal]

I have run benchmarks on the Minizinc competition 2023. After checking the results using mzn-bench, it seems that Choco in parallel mode gives wrong results on two instances:

• BDARUMA_run_code_of_0_block_108_233_1_extended_input
• Kongu_run_code_of_0_block_240_0_input

I ran the experiments with 1, 2, 4, 8, 16, 32, 64, 128 and 256 threads, and the issue occurs only with -p N where N > 1.

Please find attached a .zip with:

• failed.log: the result of mzn-bench
• *.json: the output of the solver in JSON format for all instances. You can copy the .dzn part to try directly in the minizinc editor. I have checked one with ortools in the editor and it returned unsatisfiable confirming a bug.

bug-choco.zip

[cprudhom]

Thank you for the bug reporting. I'm not sure I got what you mean by:

You can copy the .dzn part to try directly in the minizinc editor

And obviously, it takes ages to find a solution on my laptop 🤕

[ptal]

In the .dzn below, I've added the op = ... instruction which was part of the solution given by Choco. There is a model inconsistency detected directly by MinizincIDE when this is added.

Note that I'm not sure it's a bug due to parallelism, perhaps it's just that the single-threaded version of Choco didn't have time to find this particular solution.

evmopt-generic.txt Kongu_run_code_of_0_block_240_0_input.txt