added section

# Integer programming example from

# https://de.wikipedia.org/wiki/Lineare_Optimierung

from z3 import *

# Define integer variables.

x1, x2, G = Ints('product1 product2 revenue')

# We use the Optimizer module from Z3.

o = Optimize()

# Add assertions.

o.add(x1 + 2 * x2 <= 170)

o.add(x1 + x2 <= 150)

o.add(3 * x2 <= 180)

o.add(x1 >= 0, x2 >= 0)

o.add(G == 300 * x1 + 500 * x2)

# We want to maximize the total revenue G.

o.maximize(G)

if o.check() == sat:

    print(o.model())

 No newline at end of file