Possible bug: correct optimum but model is inconsistent

[fraleo]

Hello there,

I'm using Z3 (commit 2e6908b) to find the optimal solution to the following formula: formula.txt

After solving, Z3 returns 14 as the optimum, which is correct. However the model returned seems to be inconsistent with the value of the objective function (see: model_z3.txt). The same behaviour can be observed also when using the Python API.

Just to make sure, I ran OptiMathsat on the same formula and obtained a solution where the optimum is indeed 14 and the model agrees with that (see: model_optimathsat.txt).

What could be the reason for this? Any help would be much appreciated :)

Thanks!

[NikolajBjorner]

bug indeed