Optimize / maximize incorrect return value

[Thomasb81]

Hello
work.py.zip

Starting from version 4.8.9.0 the attached python script is not able to return the correct maximum value of my problem:

Here the execution trace of my script with the last working (4.8.8.0) and the last release (4.8.13.0) not working

$python3 work.py 
Z3 4.8.8.0
problem is stat: sat
maximum for PARAM1 : 19
maximum for PARAM3 : 8
maximum for PARAM2 : 4
maximum for PARAM5 : 32
maximum for PARAM4 : 32

$ python3 work.py 
Z3 4.8.13.0
problem is stat: sat
maximum for PARAM1 : 19
maximum for PARAM3 : 8
maximum for PARAM2 : 4
maximum for PARAM5 : 0
maximum for PARAM4 : 0

Depending of Z3 revision and/or the order the script fill opt.maximize in each variable the result of which variable having maximum value find at zero can change.

Is that a bug or an expected behavioral change ?

Thanks
Thomas

[Thomasb81]

In case a smt testcase is required:
test.exepected.out.zip
test.smt2.zip

Thomas

[NikolajBjorner]

The buggy code path is unfortunately hacky and I have repeatedly gotten it wrong for multi-objective case.
In lieu of a rewrite, I hope the fix addresses the bug properly.

[Thomasb81]

Unfortunately I can't comment on code quality there.
Is there any interest to add the testcase to https://github.com/Z3Prover/z3test, should I contribute ?

Thanks
Thomas

[NikolajBjorner]

The code quality is my fault, of course.
Another issue is that the code isn't well tested; and it is also something I would desire to have prepared better. The test matrix is somewhat large because it integrates different optimization solvers in the multi-objective case. Their results are combined.
If you can add test cases it will be highly appreciated and help everybody.