为何使用LIA逻辑的Z3求解器会返回实数结果？

你的代码出现这个现象的核心原因是变量类型与求解器逻辑的匹配问题：

1. 你用SolverFor("LIA")指定了线性整数算术（Linear Integer Arithmetic）逻辑，但同时将变量vB声明为Real类型。
2. Z3的SolverFor主要限制求解器使用的推理算法集合，但不会强制修改你显式声明的变量类型。LIA逻辑针对整数变量的线性约束生效，但一旦变量是实数类型，求解器依然会在实数域内寻找满足约束的解。
3. 5/2（即2.5）是严格介于2和3之间的实数，完全符合你添加的约束条件，所以Z3会返回这个解。

如果想要得到整数域内的解，需要将变量声明为Int类型：

from z3 import *

sol = SolverFor("LIA") 
vB = Int('vB')  # 改为整数类型
sol.add(vB < 3)
sol.add(vB > 2)

print(sol.check())  # 输出unsat，因为没有整数满足2 < vB < 3

内容的提问来源于stack exchange，提问作者catbow