Non-deterministic optimization result for objective function with division

[Jakob-Bach]

I observed non-deterministic optimization results with an optimization problem that has a division operation in its objective. My original optimization problem was larger (and made more sense), but I cut it down to a minimal example for demonstration purposes here:

• binary decision variables
• each variable is associated with a utility
• objective is average utility of all variables that are set to 1
• only constraint is that at least one variable has to be set to 1

The averaging (division) operation seems to yield non-deterministic results. I implemented the optimization problem in Python, with version 4.8.13 (I had 4.8.12 before, same issue) of Z3, choosing arbitrary values as utilities (the issue also occurs with other values). I solved the same optimization problem 100 times:

import pandas as pd
import z3

utilities = [1.0, 2.0, 3.0]
decision_variables = z3.Bools(' '.join(['x_' + str(i) for i in range(3)]))

k = z3.Sum(*[z3.If(var, 1, 0) for var in decision_variables])  # number of selected variables
utility_term = z3.Sum(*[z3.If(var, val, 0) for var, val in zip(decision_variables, utilities)])
utility_term = utility_term / k  # division here seems to be problematic

results = []
for _ in range(100):
    optimizer = z3.Optimize()
    objective = optimizer.maximize(utility_term)
    optimizer.add(z3.Or(decision_variables))  # one variable needs to be selected, else div by zero
    optimizer.check()
    results.append(str(objective.value()))
print(pd.Series(results).value_counts())  # distribution of results

The output, which is the distribution of the objective value over the 100 repetitions, could look like this:

3     73
oo    27
dtype: int64

(The actual values change from execution to execution.)
As you can see, the optimizer yields the correct result (3) in the majority of cases, but returns infinity in other cases.