Problems solved by z3-python

[Byxs20]

OS Version: Windows 11
Python Version: Python 3.8.10
Z3 Version: z3-solver 4.12.4.0

from z3 import *

# 创建整数变量 x
x = Int('x')

# 创建条件 x > 12 且 x < 16
condition = And(
x <= 45,
x <= 48,
x <= 49,
x <= 50,
x <= 51,
x <= 52,
x <= 53,
x <= 54,
x <= 55,
x <= 56,
)

# 创建 Z3 Solver
solver = Optimize()

# 向 Solver 添加条件
solver.add(condition)

solver.maximize(x)

# debug
assertions = solver.assertions()
for assertion in assertions:
    print(assertion)

# 检查是否存在解
if solver.check() == sat:
    # 获取解
    model = solver.model()
    solution = model[x].as_long()
    print(f"Solution: {solution}")
else:
    print("No solution")

This will not solve for 45, missing an 'x<=56' can be solved

[Byxs20]

Returned version: pip install z3-solver==4.8.12
Have already solved