如何在Z3 Python中避免位向量表达式简化生成单项式？

我有如下表达式：

a = z3.BitVec('a', 32)
b = z3.BitVec('b', 32)

e = a - b < z3.BitVecVal(0, 32)

使用z3.simplify后返回：

Not(0 <= a + 4294967295*b)

尝试了som=False等选项但没有效果，请问该如何阻止这种单项式形式的重写？

• 改用prove验证等价性：若只是需要确认表达式逻辑，直接调用z3.prove(e == Not(0 <= a - b))，此方式不会强制重写表达式结构，能保留原始减法形式。
• 自定义保守简化策略：通过z3.Tactic组合仅做基础操作的简化规则，跳过算术重写步骤。示例代码：

from z3 import *

a = BitVec('a', 32)
b = BitVec('b', 32)
e = a - b < BitVecVal(0, 32)

# 仅执行基础简化、值传播、无约束变量消除，避免减法转乘法
tactic = Then('simplify', 'propagate-values', 'elim-uncnstr')
print(tactic.apply(e))

• 自行封装表达式打印逻辑：z3的简化规则优先服务于求解效率，若需保留人类可读的结构，建议手动解析原始表达式并输出，比如直接格式化输出a - b < 0这类形式，不依赖simplify的输出结果。

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